Migrate to `Felix` namespaceHEADhotg

1 files changed, 1037 insertions, 0 deletions

diff --git a/source/Felix/Checking/Foundation.hs b/source/Felix/Checking/Foundation.hs
new file mode 100644
index 0000000..5852901
--- /dev/null
+++ b/source/Felix/Checking/Foundation.hs
@@ -0,0 +1,1037 @@
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | The one compiled monomorphic HOL/HOTG foundation.
+--
+-- Constructing 'CheckedFoundation' requires exact manifest coverage, closed
+-- well-typed schemas, and structural backend classification.  This gate
+-- certifies manifest conformance only; it is not a consistency proof.
+module Felix.Checking.Foundation
+    ( FoundationAxiomTag(..)
+    , KernelRuleTag(..)
+    , KernelRuleSignature(..)
+    , FoundationRuleInput(..)
+    , FoundationBackendClass(..)
+    , FofExclusion(..)
+    , FoundationAxiomInput(..)
+    , FoundationManifestError(..)
+    , FoundationManifestAudit
+    , auditFoundationManifest
+    , compiledFoundationIntrinsicRows
+    , compiledFoundationRuleRows
+    , compiledFoundationAxiomRows
+    , CheckedFoundation
+    , checkedFoundation
+    , foundationAxiomProposition
+    , foundationAxiomFrozen
+    , foundationAxiomBackendClass
+    , foundationRuleSignature
+    , foundationAxiomDependencies
+    , classifyCanonicalFofStructure
+    , classifyFrozenCore
+    ) where
+
+import Base hiding (Empty)
+import Felix.Checking.Core
+
+import Control.Monad (unless)
+import Data.List qualified as List
+import Data.Map.Strict qualified as Map
+import Data.Set qualified as Set
+import Numeric.Natural (Natural)
+
+
+-- | The complete axiom inventory. Ordinary implication, quantifier, equality,
+-- and falsum rules are dedicated kernel operations rather than manifest rows.
+data FoundationAxiomTag
+    = EmptyCharacteristic
+    | PairSetCharacteristic
+    | FamilyUnionCharacteristic
+    | PowerSetCharacteristic
+    | SeparationCharacteristic
+    | ReplacementCharacteristic
+    | SetChooseWitness
+    | SetExtensionality
+    | SetInduction
+    | PropositionalExtensionality
+    | DoubleNegationElim
+    | UnivOfContains
+    | UnivOfTransitive
+    | UnivOfFamilyUnionClosed
+    | UnivOfPowerSetClosed
+    | UnivOfReplacementClosed
+    | UnivOfMinimal
+    deriving stock (Show, Eq, Ord, Enum, Bounded)
+
+-- | The complete guarded-rule inventory.
+data KernelRuleTag
+    = SetLfpBound
+    | SetLfpLeast
+    | SetLfpFixed
+    | SetLfpInduct
+    deriving stock (Show, Eq, Ord, Enum, Bounded)
+
+data KernelRuleSignature = KernelRuleSignature
+    ![CoreType]
+    !Natural
+    deriving stock (Show, Eq)
+
+data FoundationRuleInput = FoundationRuleInput
+    !KernelRuleTag
+    !KernelRuleSignature
+    deriving stock (Show, Eq)
+
+data FofExclusion
+    = HigherOrderBinder !CoreType
+    | HigherOrderEquality !CoreType
+    | HigherOrderLambda
+    | HigherOrderIntrinsic !CoreIntrinsicTag
+    deriving stock (Show, Eq, Ord)
+
+data FoundationBackendClass
+    = FoundationFofProjectable
+    | FoundationRequiresTh0 !(NonEmpty FofExclusion)
+    deriving stock (Show, Eq)
+
+-- | One proposed manifest row.  This is deliberately not an authority-bearing
+-- fact; only the fixed compiled rows can produce 'CheckedFoundation'.
+data FoundationAxiomInput = FoundationAxiomInput
+    !FoundationAxiomTag
+    !(CoreSyntax Void Natural)
+    !FoundationBackendClass
+
+data FoundationManifestError
+    = MissingFoundationIntrinsic !CoreIntrinsicTag
+    | DuplicateFoundationIntrinsic !CoreIntrinsicTag
+    | FoundationIntrinsicTypeMismatch
+        !CoreIntrinsicTag
+        !CoreType
+        !CoreType
+    | MissingFoundationRule !KernelRuleTag
+    | DuplicateFoundationRule !KernelRuleTag
+    | FoundationRuleSignatureMismatch
+        !KernelRuleTag
+        !KernelRuleSignature
+        !KernelRuleSignature
+    | MissingFoundationAxiom !FoundationAxiomTag
+    | DuplicateFoundationAxiom !FoundationAxiomTag
+    | FoundationAxiomIllTyped
+        !FoundationAxiomTag
+        !CoreCheckError
+    | FoundationAxiomFreezeFailed
+        !FoundationAxiomTag
+        !FreezeError
+    | FoundationAxiomStatementMismatch
+        !FoundationAxiomTag
+    | FoundationAxiomBackendClassMismatch
+        !FoundationAxiomTag
+        !FoundationBackendClass
+        !FoundationBackendClass
+    deriving stock (Show, Eq)
+
+data CheckedFoundationAxiom = CheckedFoundationAxiom
+    !(ClosedCheckedProposition Void)
+    !(FrozenCheckedCore Void)
+    !FoundationBackendClass
+
+newtype FoundationManifestAudit = FoundationManifestAudit
+    ( Map FoundationAxiomTag CheckedFoundationAxiom
+    , Map KernelRuleTag KernelRuleSignature
+    )
+
+data CheckedFoundation = CheckedFoundation
+    !(Map FoundationAxiomTag CheckedFoundationAxiom)
+    !(Map KernelRuleTag KernelRuleSignature)
+
+
+compiledFoundationIntrinsicRows
+    :: [(CoreIntrinsicTag, CoreType)]
+compiledFoundationIntrinsicRows =
+    [ (Member, TySet `TyArrow` (TySet `TyArrow` TyProp))
+    , (Empty, TySet)
+    , (PairSet, TySet `TyArrow` (TySet `TyArrow` TySet))
+    , (FamilyUnion, TySet `TyArrow` TySet)
+    , (PowerSet, TySet `TyArrow` TySet)
+    , ( Sep
+      , TySet
+            `TyArrow`
+                ((TySet `TyArrow` TyProp) `TyArrow` TySet)
+      )
+    , ( Repl
+      , TySet
+            `TyArrow`
+                ((TySet `TyArrow` TySet) `TyArrow` TySet)
+      )
+    , (SetChoose, (TySet `TyArrow` TyProp) `TyArrow` TySet)
+    , (UnivOf, TySet `TyArrow` TySet)
+    , ( ISetLfp
+      , TySet
+            `TyArrow`
+                ((TySet `TyArrow` TySet) `TyArrow` TySet)
+      )
+    ]
+
+compiledFoundationRuleRows :: [FoundationRuleInput]
+compiledFoundationRuleRows =
+    [ FoundationRuleInput
+        tag
+        (expectedKernelRuleSignature tag)
+    | tag <- allKernelRuleTags
+    ]
+
+compiledFoundationAxiomRows :: [FoundationAxiomInput]
+compiledFoundationAxiomRows =
+    [ FoundationAxiomInput
+        tag
+        (foundationAxiomSyntax tag)
+        (expectedFoundationBackendClass tag)
+    | tag <- allFoundationAxiomTags
+    ]
+
+checkedFoundation
+    :: Either
+        (NonEmpty FoundationManifestError)
+        CheckedFoundation
+checkedFoundation = do
+    FoundationManifestAudit (axioms, rules) <-
+        auditFoundationManifest
+            compiledFoundationIntrinsicRows
+            compiledFoundationRuleRows
+            compiledFoundationAxiomRows
+    pure (CheckedFoundation axioms rules)
+
+-- | Audit arbitrary proposed rows without granting foundation authority.
+-- This is also the pure mutation boundary used by conformance tests.
+auditFoundationManifest
+    :: [(CoreIntrinsicTag, CoreType)]
+    -> [FoundationRuleInput]
+    -> [FoundationAxiomInput]
+    -> Either
+        (NonEmpty FoundationManifestError)
+        FoundationManifestAudit
+auditFoundationManifest intrinsicRows ruleRows axiomRows =
+    case
+        intrinsicErrors
+            <> ruleErrors
+            <> axiomCoverageErrors
+            <> axiomErrors of
+        [] ->
+            case checkedRows of
+                Left errors ->
+                    Left errors
+                Right rows ->
+                    Right
+                        (FoundationManifestAudit
+                            ( Map.fromList rows
+                            , Map.fromList
+                                [ (tag, signature)
+                                | FoundationRuleInput
+                                    tag
+                                    signature <-
+                                        ruleRows
+                                ]
+                            ))
+        firstError : remainingErrors ->
+            Left (firstError :| remainingErrors)
+  where
+    intrinsicErrors =
+        coverageErrors
+            MissingFoundationIntrinsic
+            DuplicateFoundationIntrinsic
+            allCoreIntrinsicTags
+            (fst <$> intrinsicRows)
+            <> [ FoundationIntrinsicTypeMismatch
+                    tag
+                    (coreIntrinsicType tag)
+                    actual
+               | (tag, actual) <- intrinsicRows
+               , actual /= coreIntrinsicType tag
+               ]
+    axiomCoverageErrors =
+        coverageErrors
+            MissingFoundationAxiom
+            DuplicateFoundationAxiom
+            allFoundationAxiomTags
+            [ tag
+            | FoundationAxiomInput tag _syntax _backendClass <-
+                axiomRows
+            ]
+    ruleErrors =
+        coverageErrors
+            MissingFoundationRule
+            DuplicateFoundationRule
+            allKernelRuleTags
+            [ tag
+            | FoundationRuleInput tag _signature <-
+                ruleRows
+            ]
+            <> [ FoundationRuleSignatureMismatch
+                    tag
+                    (expectedKernelRuleSignature tag)
+                    actual
+               | FoundationRuleInput tag actual <-
+                    ruleRows
+               , actual /= expectedKernelRuleSignature tag
+               ]
+    checkedRows =
+        traverse checkAxiomRow axiomRows
+    axiomErrors =
+        case checkedRows of
+            Left errors ->
+                toList errors
+            Right _rows ->
+                []
+
+checkAxiomRow
+    :: FoundationAxiomInput
+    -> Either
+        (NonEmpty FoundationManifestError)
+        (FoundationAxiomTag, CheckedFoundationAxiom)
+checkAxiomRow
+        (FoundationAxiomInput
+            tag
+            syntax
+            declaredBackendClass) = do
+    proposition <-
+        firstOne (FoundationAxiomIllTyped tag)
+            (checkClosedProposition absurd syntax)
+    frozen <-
+        firstOne (FoundationAxiomFreezeFailed tag)
+            (freezeClosed
+                (checkedPropositionCore proposition))
+    expectedFrozen <-
+        expectedFoundationAxiom tag
+    unless
+        (frozen == expectedFrozen)
+        (Left
+            (FoundationAxiomStatementMismatch tag :| []))
+    let actualBackendClass =
+            classifyFrozenCore frozen
+    unless
+        (declaredBackendClass == actualBackendClass)
+        (Left
+            (FoundationAxiomBackendClassMismatch
+                tag
+                declaredBackendClass
+                actualBackendClass
+                :| []))
+    pure
+        ( tag
+        , CheckedFoundationAxiom
+            proposition
+            frozen
+            actualBackendClass
+        )
+
+expectedFoundationAxiom
+    :: FoundationAxiomTag
+    -> Either
+        (NonEmpty FoundationManifestError)
+        (FrozenCheckedCore Void)
+expectedFoundationAxiom tag = do
+    proposition <-
+        firstOne (FoundationAxiomIllTyped tag)
+            (checkClosedProposition
+                absurd
+                (foundationAxiomSyntax tag))
+    firstOne (FoundationAxiomFreezeFailed tag)
+        (freezeClosed
+            (checkedPropositionCore proposition))
+
+foundationAxiomProposition
+    :: CheckedFoundation
+    -> FoundationAxiomTag
+    -> ClosedCheckedProposition Void
+foundationAxiomProposition foundation tag =
+    case lookupFoundationAxiom foundation tag of
+        CheckedFoundationAxiom proposition _frozen _backendClass ->
+            proposition
+
+foundationAxiomFrozen
+    :: CheckedFoundation
+    -> FoundationAxiomTag
+    -> FrozenCheckedCore Void
+foundationAxiomFrozen foundation tag =
+    case lookupFoundationAxiom foundation tag of
+        CheckedFoundationAxiom _proposition frozen _backendClass ->
+            frozen
+
+foundationAxiomBackendClass
+    :: CheckedFoundation
+    -> FoundationAxiomTag
+    -> FoundationBackendClass
+foundationAxiomBackendClass foundation tag =
+    case lookupFoundationAxiom foundation tag of
+        CheckedFoundationAxiom _proposition _frozen backendClass ->
+            backendClass
+
+lookupFoundationAxiom
+    :: CheckedFoundation
+    -> FoundationAxiomTag
+    -> CheckedFoundationAxiom
+lookupFoundationAxiom
+        (CheckedFoundation axioms _rules)
+        tag =
+    case Map.lookup tag axioms of
+        Just axiom ->
+            axiom
+        Nothing ->
+            impossible
+                "checked foundation omitted a validated axiom tag"
+
+foundationRuleSignature
+    :: CheckedFoundation
+    -> KernelRuleTag
+    -> KernelRuleSignature
+foundationRuleSignature
+        (CheckedFoundation _axioms rules)
+        tag =
+    case Map.lookup tag rules of
+        Just signature ->
+            signature
+        Nothing ->
+            impossible
+                "checked foundation omitted a validated kernel rule"
+
+
+classifyFrozenCore
+    :: FrozenCheckedCore global
+    -> FoundationBackendClass
+classifyFrozenCore =
+    classifyCanonicalFofStructure
+        . frozenCoreTerm
+
+classifyCanonicalFofStructure
+    :: CanonicalTerm global
+    -> FoundationBackendClass
+classifyCanonicalFofStructure term =
+    case Set.toAscList
+            (termFofExclusions
+                term) of
+        [] ->
+            FoundationFofProjectable
+        firstExclusion : remainingExclusions ->
+            FoundationRequiresTh0
+                (firstExclusion :| remainingExclusions)
+
+foundationAxiomDependencies
+    :: CanonicalTerm global
+    -> Set FoundationAxiomTag
+foundationAxiomDependencies = \case
+    CBound{} ->
+        mempty
+    CGlobal{} ->
+        mempty
+    CIntrinsic intrinsic ->
+        intrinsicFoundationAxioms intrinsic
+    COpaqueInteger{} ->
+        mempty
+    CApp function argument ->
+        foundationAxiomDependencies function
+            <> foundationAxiomDependencies argument
+    CLam _binderType body ->
+        foundationAxiomDependencies body
+    CFalsum ->
+        mempty
+    CImp premise conclusion ->
+        foundationAxiomDependencies premise
+            <> foundationAxiomDependencies conclusion
+    CEq _operandType left right ->
+        foundationAxiomDependencies left
+            <> foundationAxiomDependencies right
+    CForall _binderType body ->
+        foundationAxiomDependencies body
+
+intrinsicFoundationAxioms
+    :: CoreIntrinsicTag
+    -> Set FoundationAxiomTag
+intrinsicFoundationAxioms = Set.fromList . \case
+    Member ->
+        []
+    Empty ->
+        [EmptyCharacteristic]
+    PairSet ->
+        [PairSetCharacteristic]
+    FamilyUnion ->
+        [FamilyUnionCharacteristic]
+    PowerSet ->
+        [PowerSetCharacteristic]
+    Sep ->
+        [SeparationCharacteristic]
+    Repl ->
+        [ReplacementCharacteristic]
+    SetChoose ->
+        [SetChooseWitness]
+    UnivOf ->
+        []
+    ISetLfp ->
+        []
+
+termFofExclusions
+    :: CanonicalTerm global
+    -> Set FofExclusion
+termFofExclusions = \case
+    CBound{} ->
+        mempty
+    CGlobal{} ->
+        mempty
+    CIntrinsic intrinsic
+        | intrinsic `elem`
+            [Sep, Repl, SetChoose, ISetLfp] ->
+            Set.singleton
+                (HigherOrderIntrinsic intrinsic)
+        | otherwise ->
+            mempty
+    COpaqueInteger{} ->
+        mempty
+    CApp function argument ->
+        termFofExclusions function
+            <> termFofExclusions argument
+    CLam _binderType body ->
+        Set.insert HigherOrderLambda
+            (termFofExclusions body)
+    CFalsum ->
+        mempty
+    CImp premise conclusion ->
+        termFofExclusions premise
+            <> termFofExclusions conclusion
+    CEq operandType left right ->
+        (case operandType of
+            TyArrow{} ->
+                Set.singleton
+                    (HigherOrderEquality operandType)
+            _ ->
+                mempty)
+            <> termFofExclusions left
+            <> termFofExclusions right
+    CForall binderType body ->
+        (case binderType of
+            TySet ->
+                mempty
+            _ ->
+                Set.singleton
+                    (HigherOrderBinder binderType))
+            <> termFofExclusions body
+
+
+allCoreIntrinsicTags :: [CoreIntrinsicTag]
+allCoreIntrinsicTags =
+    [minBound .. maxBound]
+
+allFoundationAxiomTags :: [FoundationAxiomTag]
+allFoundationAxiomTags =
+    [minBound .. maxBound]
+
+allKernelRuleTags :: [KernelRuleTag]
+allKernelRuleTags =
+    [minBound .. maxBound]
+
+expectedKernelRuleSignature
+    :: KernelRuleTag
+    -> KernelRuleSignature
+expectedKernelRuleSignature = \case
+    SetLfpBound ->
+        KernelRuleSignature
+            [TySet, TySet `TyArrow` TySet]
+            0
+    SetLfpLeast ->
+        KernelRuleSignature
+            [TySet, TySet `TyArrow` TySet, TySet]
+            2
+    SetLfpFixed ->
+        KernelRuleSignature
+            [TySet, TySet `TyArrow` TySet]
+            1
+    SetLfpInduct ->
+        KernelRuleSignature
+            [ TySet
+            , TySet `TyArrow` TySet
+            , TySet `TyArrow` TyProp
+            , TySet
+            ]
+            3
+
+coverageErrors
+    :: Ord tag
+    => (tag -> error)
+    -> (tag -> error)
+    -> [tag]
+    -> [tag]
+    -> [error]
+coverageErrors missing duplicate expected actual =
+    [ missing tag
+    | tag <- expected
+    , occurrenceCount tag == 0
+    ]
+        <> [ duplicate tag
+           | tag <- expected
+           , occurrenceCount tag > 1
+           ]
+  where
+    occurrenceCount tag =
+        length (List.filter (== tag) actual)
+
+firstOne
+    :: (error -> FoundationManifestError)
+    -> Either error value
+    -> Either (NonEmpty FoundationManifestError) value
+firstOne wrap =
+    either
+        (Left . (:| []) . wrap)
+        Right
+
+
+type FoundationSyntax = CoreSyntax Void Natural
+
+foundationAxiomSyntax
+    :: FoundationAxiomTag
+    -> FoundationSyntax
+foundationAxiomSyntax = \case
+    EmptyCharacteristic ->
+        foralls
+            [(x, TySet)]
+            (iff
+                (member (var x) emptySet)
+                coreFalsum)
+    PairSetCharacteristic ->
+        foralls
+            [(a, TySet), (b, TySet), (x, TySet)]
+            (iff
+                (member
+                    (var x)
+                    (pairSet (var a) (var b)))
+                (orP
+                    (eqSet (var x) (var a))
+                    (eqSet (var x) (var b))))
+    FamilyUnionCharacteristic ->
+        foralls
+            [(a, TySet), (x, TySet)]
+            (iff
+                (member
+                    (var x)
+                    (familyUnion (var a)))
+                (exists
+                    b
+                    TySet
+                    (andP
+                        (member (var b) (var a))
+                        (member (var x) (var b)))))
+    PowerSetCharacteristic ->
+        foralls
+            [(a, TySet), (b, TySet)]
+            (iff
+                (member
+                    (var b)
+                    (powerSet (var a)))
+                (subset (var b) (var a)))
+    SeparationCharacteristic ->
+        foralls
+            [ (a, TySet)
+            , (p, TySet `TyArrow` TyProp)
+            , (x, TySet)
+            ]
+            (iff
+                (member
+                    (var x)
+                    (separation (var a) (var p)))
+                (andP
+                    (member (var x) (var a))
+                    (apply (var p) (var x))))
+    ReplacementCharacteristic ->
+        foralls
+            [ (a, TySet)
+            , (f, TySet `TyArrow` TySet)
+            , (y, TySet)
+            ]
+            (iff
+                (member
+                    (var y)
+                    (replacement (var a) (var f)))
+                (exists
+                    x
+                    TySet
+                    (andP
+                        (member (var x) (var a))
+                        (eqSet
+                            (var y)
+                            (apply (var f) (var x))))))
+    SetChooseWitness ->
+        foralls
+            [ (p, TySet `TyArrow` TyProp)
+            , (x, TySet)
+            ]
+            (implies
+                (apply (var p) (var x))
+                (apply
+                    (var p)
+                    (setChoose (var p))))
+    SetExtensionality ->
+        foralls
+            [(a, TySet), (b, TySet)]
+            (implies
+                (subset (var a) (var b))
+                (implies
+                    (subset (var b) (var a))
+                    (eqSet (var a) (var b))))
+    SetInduction ->
+        forallOne
+            p
+            (TySet `TyArrow` TyProp)
+            (implies
+                (forallOne
+                    a
+                    TySet
+                    (implies
+                        (forallOne
+                            x
+                            TySet
+                            (implies
+                                (member (var x) (var a))
+                                (apply (var p) (var x))))
+                        (apply (var p) (var a))))
+                (forallOne
+                    a
+                    TySet
+                    (apply (var p) (var a))))
+    PropositionalExtensionality ->
+        foralls
+            [(p, TyProp), (q, TyProp)]
+            (implies
+                (implies (var p) (var q))
+                (implies
+                    (implies (var q) (var p))
+                    (coreEquality
+                        TyProp
+                        (var p)
+                        (var q))))
+    DoubleNegationElim ->
+        forallOne
+            p
+            TyProp
+            (implies
+                (notP (notP (var p)))
+                (var p))
+    UnivOfContains ->
+        forallOne
+            n
+            TySet
+            (member
+                (var n)
+                (univOf (var n)))
+    UnivOfTransitive ->
+        forallOne
+            n
+            TySet
+            (transitive (univOf (var n)))
+    UnivOfFamilyUnionClosed ->
+        forallOne
+            n
+            TySet
+            (familyUnionClosed
+                (univOf (var n)))
+    UnivOfPowerSetClosed ->
+        forallOne
+            n
+            TySet
+            (powerSetClosed
+                (univOf (var n)))
+    UnivOfReplacementClosed ->
+        forallOne
+            n
+            TySet
+            (replacementClosed
+                (univOf (var n)))
+    UnivOfMinimal ->
+        foralls
+            [(n, TySet), (u, TySet)]
+            (implies
+                (member (var n) (var u))
+                (implies
+                    (transitive (var u))
+                    (implies
+                        (familyUnionClosed (var u))
+                        (implies
+                            (powerSetClosed (var u))
+                            (implies
+                                (replacementClosed (var u))
+                                (subset
+                                    (univOf (var n))
+                                    (var u)))))))
+
+expectedFoundationBackendClass
+    :: FoundationAxiomTag
+    -> FoundationBackendClass
+expectedFoundationBackendClass = \case
+    EmptyCharacteristic ->
+        FoundationFofProjectable
+    PairSetCharacteristic ->
+        FoundationFofProjectable
+    FamilyUnionCharacteristic ->
+        FoundationFofProjectable
+    PowerSetCharacteristic ->
+        FoundationFofProjectable
+    SeparationCharacteristic ->
+        requiresTh0
+            (HigherOrderBinder
+                (TySet `TyArrow` TyProp))
+            [HigherOrderIntrinsic Sep]
+    ReplacementCharacteristic ->
+        requiresTh0
+            (HigherOrderBinder
+                (TySet `TyArrow` TySet))
+            [HigherOrderIntrinsic Repl]
+    SetChooseWitness ->
+        requiresTh0
+            (HigherOrderBinder
+                (TySet `TyArrow` TyProp))
+            [HigherOrderIntrinsic SetChoose]
+    SetExtensionality ->
+        FoundationFofProjectable
+    SetInduction ->
+        requiresTh0
+            (HigherOrderBinder
+                (TySet `TyArrow` TyProp))
+            []
+    PropositionalExtensionality ->
+        requiresTh0
+            (HigherOrderBinder TyProp)
+            []
+    DoubleNegationElim ->
+        requiresTh0
+            (HigherOrderBinder TyProp)
+            []
+    UnivOfContains ->
+        FoundationFofProjectable
+    UnivOfTransitive ->
+        FoundationFofProjectable
+    UnivOfFamilyUnionClosed ->
+        FoundationFofProjectable
+    UnivOfPowerSetClosed ->
+        FoundationFofProjectable
+    UnivOfReplacementClosed ->
+        requiresTh0
+            (HigherOrderBinder
+                (TySet `TyArrow` TySet))
+            [HigherOrderIntrinsic Repl]
+    UnivOfMinimal ->
+        requiresTh0
+            (HigherOrderBinder
+                (TySet `TyArrow` TySet))
+            [HigherOrderIntrinsic Repl]
+  where
+    requiresTh0 firstExclusion remainingExclusions =
+        FoundationRequiresTh0
+            (firstExclusion :| remainingExclusions)
+
+
+x, y, a, b, p, q, f, n, u :: Natural
+x = 0
+y = 1
+a = 2
+b = 3
+p = 4
+q = 5
+f = 6
+n = 7
+u = 8
+
+var :: Natural -> FoundationSyntax
+var = coreLocal
+
+apply
+    :: FoundationSyntax
+    -> FoundationSyntax
+    -> FoundationSyntax
+apply = coreApply
+
+apply2
+    :: FoundationSyntax
+    -> FoundationSyntax
+    -> FoundationSyntax
+    -> FoundationSyntax
+apply2 function firstArgument secondArgument =
+    apply
+        (apply function firstArgument)
+        secondArgument
+
+member
+    :: FoundationSyntax
+    -> FoundationSyntax
+    -> FoundationSyntax
+member =
+    apply2 (coreIntrinsic Member)
+
+emptySet :: FoundationSyntax
+emptySet =
+    coreIntrinsic Empty
+
+pairSet
+    :: FoundationSyntax
+    -> FoundationSyntax
+    -> FoundationSyntax
+pairSet =
+    apply2 (coreIntrinsic PairSet)
+
+familyUnion :: FoundationSyntax -> FoundationSyntax
+familyUnion =
+    apply (coreIntrinsic FamilyUnion)
+
+powerSet :: FoundationSyntax -> FoundationSyntax
+powerSet =
+    apply (coreIntrinsic PowerSet)
+
+separation
+    :: FoundationSyntax
+    -> FoundationSyntax
+    -> FoundationSyntax
+separation =
+    apply2 (coreIntrinsic Sep)
+
+replacement
+    :: FoundationSyntax
+    -> FoundationSyntax
+    -> FoundationSyntax
+replacement =
+    apply2 (coreIntrinsic Repl)
+
+setChoose :: FoundationSyntax -> FoundationSyntax
+setChoose =
+    apply (coreIntrinsic SetChoose)
+
+univOf :: FoundationSyntax -> FoundationSyntax
+univOf =
+    apply (coreIntrinsic UnivOf)
+
+implies
+    :: FoundationSyntax
+    -> FoundationSyntax
+    -> FoundationSyntax
+implies =
+    coreImplication
+
+notP :: FoundationSyntax -> FoundationSyntax
+notP proposition =
+    implies proposition coreFalsum
+
+andP
+    :: FoundationSyntax
+    -> FoundationSyntax
+    -> FoundationSyntax
+andP left right =
+    notP
+        (implies left (notP right))
+
+orP
+    :: FoundationSyntax
+    -> FoundationSyntax
+    -> FoundationSyntax
+orP left right =
+    implies (notP left) right
+
+iff
+    :: FoundationSyntax
+    -> FoundationSyntax
+    -> FoundationSyntax
+iff =
+    coreEquality TyProp
+
+eqSet
+    :: FoundationSyntax
+    -> FoundationSyntax
+    -> FoundationSyntax
+eqSet =
+    coreEquality TySet
+
+forallOne
+    :: Natural
+    -> CoreType
+    -> FoundationSyntax
+    -> FoundationSyntax
+forallOne local binderType =
+    coreForall binderType local
+
+foralls
+    :: [(Natural, CoreType)]
+    -> FoundationSyntax
+    -> FoundationSyntax
+foralls binders body =
+    foldr
+        (uncurry forallOne)
+        body
+        binders
+
+exists
+    :: Natural
+    -> CoreType
+    -> FoundationSyntax
+    -> FoundationSyntax
+exists local binderType body =
+    notP
+        (forallOne
+            local
+            binderType
+            (notP body))
+
+subset
+    :: FoundationSyntax
+    -> FoundationSyntax
+    -> FoundationSyntax
+subset left right =
+    forallOne
+        x
+        TySet
+        (implies
+            (member (var x) left)
+            (member (var x) right))
+
+transitive :: FoundationSyntax -> FoundationSyntax
+transitive universe =
+    forallOne
+        a
+        TySet
+        (implies
+            (member (var a) universe)
+            (subset (var a) universe))
+
+familyUnionClosed :: FoundationSyntax -> FoundationSyntax
+familyUnionClosed universe =
+    forallOne
+        a
+        TySet
+        (implies
+            (member (var a) universe)
+            (member
+                (familyUnion (var a))
+                universe))
+
+powerSetClosed :: FoundationSyntax -> FoundationSyntax
+powerSetClosed universe =
+    forallOne
+        a
+        TySet
+        (implies
+            (member (var a) universe)
+            (member
+                (powerSet (var a))
+                universe))
+
+replacementClosed :: FoundationSyntax -> FoundationSyntax
+replacementClosed universe =
+    foralls
+        [ (a, TySet)
+        , (f, TySet `TyArrow` TySet)
+        ]
+        (implies
+            (member (var a) universe)
+            (implies
+                (forallOne
+                    x
+                    TySet
+                    (implies
+                        (member (var x) (var a))
+                        (member
+                            (apply (var f) (var x))
+                            universe)))
+                (member
+                    (replacement (var a) (var f))
+                    universe)))