diff options
Diffstat (limited to 'source/Checking/Foundation.hs')
| -rw-r--r-- | source/Checking/Foundation.hs | 1037 |
1 files changed, 0 insertions, 1037 deletions
diff --git a/source/Checking/Foundation.hs b/source/Checking/Foundation.hs deleted file mode 100644 index 317d1b5..0000000 --- a/source/Checking/Foundation.hs +++ /dev/null @@ -1,1037 +0,0 @@ -{-# 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 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 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))) |