summaryrefslogtreecommitdiff
path: root/source/Felix/Checking/Foundation.hs
diff options
context:
space:
mode:
Diffstat (limited to 'source/Felix/Checking/Foundation.hs')
-rw-r--r--source/Felix/Checking/Foundation.hs1037
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)))
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-06 19:58:45 +0000