Migrate to `Felix` namespaceHEADhotg

1 files changed, 0 insertions, 1191 deletions

diff --git a/source/Checking/SetConstruction.hs b/source/Checking/SetConstruction.hs
deleted file mode 100644
index 4c4b4bc..0000000
--- a/source/Checking/SetConstruction.hs
+++ /dev/null
@@ -1,1191 +0,0 @@
-{-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE NoImplicitPrelude #-}
-
--- | Checked source semantics for named separation and functional replacement.
---
--- A value of 'NamedSetConstruction' is the sole transient owner of the
--- source decomposition.  Its smart constructors validate the complete
--- telescope and derive one canonical term.  Local views, transparent content,
--- direct extensional facts, and cache-scoped descriptors all consume that
--- same checked value.
-module Checking.SetConstruction
-    ( NamedSetConstruction
-    , checkedSeparationConstruction
-    , checkedFunctionalReplacementConstruction
-    , namedSetConstructionTerm
-    , namedSetConstructionLocalViews
-    , namedSetConstructionClosedBody
-    , SetConstructionFoundation
-    , setConstructionFoundation
-    , checkedFoundationSetConstruction
-    , NamedSetConstructionFact
-    , namedSetConstructionFactProposition
-    , namedSetConstructionFactDescriptor
-    , namedSetConstructionObjectFact
-    , CheckedRelationalSetConstruction
-    , checkedRelationalReplacementConstruction
-    , relationalSetConstructionTerm
-    , relationalSetConstructionFunctionality
-    , relationalSetConstructionClosedFunctionality
-    , relationalSetConstructionLocalViews
-    , relationalSetConstructionClosedBody
-    , RelationalSetConstructionFact
-    , relationalSetConstructionFactProposition
-    , relationalSetConstructionFactDescriptor
-    , relationalSetConstructionObjectFact
-    ) where
-
-import Base hiding (Empty)
-import Checking.Core
-import Checking.Foundation
-import Checking.Identity
-import Felix.Cache.Codec
-    ( CacheDigest
-    , encodeCache
-    , hashCacheFields
-    , putCanonicalTermCache
-    , putCoreTypeCache
-    )
-
-import Data.List.NonEmpty qualified as NonEmpty
-import Data.Map.Strict qualified as Map
-import Data.Set qualified as Set
-import Numeric.Natural (Natural)
-
-
--- | The exact fixed rows used by the narrow derived extensionality schema.
--- Proof-local construction obtains these rows through the confined foundation
--- lookup; declaration authorization obtains them from 'CheckedFoundation'.
-data SetConstructionFoundation = SetConstructionFoundation
-    !(FrozenCheckedCore Void)
-    !(FrozenCheckedCore Void)
-    !(FrozenCheckedCore Void)
-    !(FrozenCheckedCore Void)
-
-setConstructionFoundation
-    :: FrozenCheckedCore Void
-    -> FrozenCheckedCore Void
-    -> FrozenCheckedCore Void
-    -> FrozenCheckedCore Void
-    -> SetConstructionFoundation
-setConstructionFoundation =
-    SetConstructionFoundation
-
-checkedFoundationSetConstruction
-    :: CheckedFoundation
-    -> SetConstructionFoundation
-checkedFoundationSetConstruction foundation =
-    SetConstructionFoundation
-        (foundationAxiomFrozen foundation FamilyUnionCharacteristic)
-        (foundationAxiomFrozen foundation SeparationCharacteristic)
-        (foundationAxiomFrozen foundation ReplacementCharacteristic)
-        (foundationAxiomFrozen foundation SetChooseWitness)
-
-data NamedSetConstruction global = NamedSetConstruction
-    ![CoreType]
-    !(Map.Map global CoreType)
-    !(NamedSetConstructionShape global)
-    !(BuiltSetConstruction global)
-    deriving stock (Eq)
-
-data NamedSetConstructionShape global
-    = SeparationShape
-        !(CanonicalTerm global)
-        !(CanonicalTerm global)
-    | FunctionalReplacementShape
-        !(NonEmpty (CanonicalTerm global))
-        !(CanonicalTerm global)
-        !(Maybe (CanonicalTerm global))
-    deriving stock (Eq)
-
--- | The one canonical build result retained by the checked construction.
--- Characteristic applications describe the exact primitive rows used by the
--- derived theorem schema; the flattened body is the deterministic composition
--- of those rows for the source telescope.
-data BuiltSetConstruction global = BuiltSetConstruction
-    !(CanonicalTerm global)
-    !(CanonicalTerm global)
-    ![CheckedCharacteristicApplication global]
-    deriving stock (Eq)
-
-data CheckedCharacteristicApplication global =
-    CheckedCharacteristicApplication
-        !CoreIntrinsicTag
-        ![CoreType]
-        !(CanonicalTerm global)
-        !(NonEmpty (CoreType, CanonicalTerm global))
-        !(CanonicalTerm global)
-    deriving stock (Eq)
-
--- | One checked relational replacement.  Unlike the unconditional named
--- constructions above, its flattened membership theorem is available only
--- after the separately checked functionality proposition has authority.
--- This value owns the source telescope, the one canonical choice/replacement
--- term, and the exact primitive characteristic applications used by that
--- narrow derived schema.
-data CheckedRelationalSetConstruction global =
-    CheckedRelationalSetConstruction
-        ![CoreType]
-        !(Map.Map global CoreType)
-        !(CanonicalTerm global)
-        !(CanonicalTerm global)
-        !(CanonicalTerm global)
-        !(CanonicalTerm global)
-        !(CanonicalTerm global)
-        ![CheckedCharacteristicApplication global]
-    deriving stock (Eq)
-
--- | Validate one source relational replacement.  The relation is checked in
--- the nearest-first context @[range, domain] <> outer@, matching the source
--- binder order @y x A P@ without retaining source syntax.
-checkedRelationalReplacementConstruction
-    :: Ord global
-    => (global -> Maybe CoreType)
-    -> ScopedCheckedCore global
-    -> ScopedCheckedCore global
-    -> Maybe (CheckedRelationalSetConstruction global)
-checkedRelationalReplacementConstruction globalType domain relation = do
-    guard (scopedCoreType domain == TySet)
-    guard (scopedCoreType relation == TyProp)
-    let context = scopedCoreContext domain
-    guard (scopedCoreContext relation == TySet : TySet : context)
-    globals <-
-        captureGlobalTypes globalType
-            [scopedCoreTerm domain, scopedCoreTerm relation]
-    let domainTerm = scopedCoreTerm domain
-        relationTerm = scopedCoreTerm relation
-        domainPredicate = CLam TySet (logicalExists relationTerm)
-        restrictedDomain = applyIntrinsic2 Sep domainTerm domainPredicate
-        choiceFunction =
-            CLam TySet
-                (applyIntrinsic SetChoose (CLam TySet relationTerm))
-        replacement = applyIntrinsic2 Repl restrictedDomain choiceFunction
-        functionality = relationalFunctionality domainTerm relationTerm
-        membership = relationalMembership domainTerm relationTerm
-        applications =
-            [ characteristicApplication
-                Sep context restrictedDomain
-                [ (TySet, domainTerm)
-                , (TyArrow TySet TyProp, domainPredicate)
-                ]
-            , characteristicApplication
-                Repl context replacement
-                [ (TySet, restrictedDomain)
-                , (TyArrow TySet TySet, choiceFunction)
-                ]
-            ]
-        construction =
-            CheckedRelationalSetConstruction
-                context globals domainTerm relationTerm replacement
-                functionality membership applications
-    _ <- checkedRelationalDerived construction context TySet replacement
-    _ <- checkedRelationalDerived construction context TyProp functionality
-    _ <- checkedRelationalDerived
-        construction (TySet : context) TyProp membership
-    pure construction
-
--- | Check one source separation.  The callback supplies the exact visible
--- type of every global used by its already checked components.
-checkedSeparationConstruction
-    :: Ord global
-    => (global -> Maybe CoreType)
-    -> ScopedCheckedCore global
-    -> ScopedCheckedCore global
-    -> Maybe (NamedSetConstruction global)
-checkedSeparationConstruction globalType bound predicate = do
-    guard (scopedCoreType bound == TySet)
-    guard (scopedCoreType predicate == TyProp)
-    let context = scopedCoreContext bound
-    guard (scopedCoreContext predicate == TySet : context)
-    globals <-
-        captureGlobalTypes globalType
-            [scopedCoreTerm bound, scopedCoreTerm predicate]
-    finishConstruction
-        context
-        globals
-        (SeparationShape
-            (scopedCoreTerm bound)
-            (scopedCoreTerm predicate))
-
--- | Check source-ordered functional replacement once.  Domain @i@ is checked
--- beneath exactly the preceding @i - 1@ source binders; the value and optional
--- condition are checked beneath the complete telescope.
-checkedFunctionalReplacementConstruction
-    :: Ord global
-    => (global -> Maybe CoreType)
-    -> NonEmpty (ScopedCheckedCore global)
-    -> ScopedCheckedCore global
-    -> Maybe (ScopedCheckedCore global)
-    -> Maybe (NamedSetConstruction global)
-checkedFunctionalReplacementConstruction globalType domains value condition = do
-    let domainList = NonEmpty.toList domains
-        firstDomain = NonEmpty.head domains
-    guard (scopedCoreType firstDomain == TySet)
-    let context = scopedCoreContext firstDomain
-        expectedDomainContexts =
-            [ replicate index TySet <> context
-            | index <- [0 .. length domainList - 1]
-            ]
-        valueContext = replicate (length domainList) TySet <> context
-    guard
-        (and
-            (zipWith
-                (\domain expected ->
-                    scopedCoreType domain == TySet
-                        && scopedCoreContext domain == expected)
-                domainList
-                expectedDomainContexts))
-    guard
-        (scopedCoreType value == TySet
-            && scopedCoreContext value == valueContext)
-    traverse_
-        (\predicate ->
-            guard
-                (scopedCoreType predicate == TyProp
-                    && scopedCoreContext predicate == valueContext))
-        condition
-    globals <-
-        captureGlobalTypes globalType
-            ( (scopedCoreTerm <$> domainList)
-              <> [scopedCoreTerm value]
-              <> maybeToList (scopedCoreTerm <$> condition)
-            )
-    finishConstruction
-        context
-        globals
-        (FunctionalReplacementShape
-            (scopedCoreTerm <$> domains)
-            (scopedCoreTerm value)
-            (scopedCoreTerm <$> condition))
-
-namedSetConstructionTerm
-    :: Ord global
-    => NamedSetConstruction global
-    -> ScopedCheckedCore global
-namedSetConstructionTerm construction =
-    fromMaybe
-        (impossible "a checked construction lost its canonical term")
-        (checkedDerived
-            construction
-            (constructionContext construction)
-            TySet
-            (constructionCanonicalTerm construction))
-
--- | Introduce a fresh named set and return adjacent FOF extensional and exact
--- equation locals.  Weakening is internal so construction-local binders and
--- source-domain order cannot drift at a caller.
-namedSetConstructionLocalViews
-    :: Ord global
-    => SetConstructionFoundation
-    -> NamedSetConstruction global
-    -> Maybe
-        ( ScopedCheckedCore global
-        , ScopedCheckedCore global
-        )
-namedSetConstructionLocalViews foundation construction = do
-    weakened <- weakenConstruction TySet construction
-    let context = TySet : constructionContext construction
-        target = CBound 0
-    extensional <- extensionalView foundation target weakened
-    equation <- checkedDerived weakened context TyProp
-        (CEq TySet target (constructionCanonicalTerm weakened))
-    pure (extensional, equation)
-
--- | Closed transparent content derived from the sole canonical construction
--- term.  This retains the pre-existing object-content identity exactly.
-namedSetConstructionClosedBody
-    :: Ord global
-    => NamedSetConstruction global
-    -> FrozenCheckedCore global
-namedSetConstructionClosedBody construction =
-    fromMaybe
-        (impossible "a checked construction did not close")
-        (freezeDerived construction closedType closedTerm)
-  where
-    context = constructionContext construction
-    closedType = foldr TyArrow TySet (reverse context)
-    closedTerm =
-        foldl (flip CLam) (constructionCanonicalTerm construction) context
-
-data NamedSetConstructionFact = NamedSetConstructionFact
-    !(FrozenCheckedCore ObjectId)
-    !CacheDigest
-
-namedSetConstructionFactProposition
-    :: NamedSetConstructionFact
-    -> FrozenCheckedCore ObjectId
-namedSetConstructionFactProposition
-        (NamedSetConstructionFact proposition _descriptor) =
-    proposition
-
-namedSetConstructionFactDescriptor
-    :: NamedSetConstructionFact
-    -> CacheDigest
-namedSetConstructionFactDescriptor
-        (NamedSetConstructionFact _proposition descriptor) =
-    descriptor
-
--- | Derive the only proposition authorized by
--- @CheckedSetConstructionExtensionality@.  This is a deliberately small
--- trusted theorem schema over the fixed foundation: every primitive
--- characteristic specialization is checked against its exact membership
--- formula before the source telescope is composed.  The caller cannot supply
--- either the resulting proposition or its cache descriptor.
-namedSetConstructionObjectFact
-    :: SetConstructionFoundation
-    -> ObjectId
-    -> NamedSetConstruction ObjectId
-    -> Maybe NamedSetConstructionFact
-namedSetConstructionObjectFact foundation object construction = do
-    let context = constructionContext construction
-        objectType = foldr TyArrow TySet (reverse context)
-    globals <- insertGlobalType object objectType (constructionGlobals construction)
-    let withObject = replaceConstructionGlobals globals construction
-        target =
-            foldl
-                CApp
-                (CGlobal object)
-                [ CBound (fromIntegral index)
-                | index <- reverse [0 .. length context - 1]
-                ]
-    view <- extensionalView foundation target withObject
-    proposition <- freezeDerived withObject TyProp
-        (foldl
-            (flip CForall)
-            (scopedCoreTerm view)
-            context)
-    selfView <- extensionalView
-        foundation
-        (constructionCanonicalTerm construction)
-        construction
-    closedSelf <- freezeDerived construction TyProp
-        (foldl
-            (flip CForall)
-            (scopedCoreTerm selfView)
-            context)
-    let closedBody = namedSetConstructionClosedBody construction
-        descriptor =
-            hashCacheFields
-                "felix-checked-named-set-construction-v1"
-                [ encodeCache do
-                    putCoreTypeCache (frozenCoreType closedBody)
-                    putCanonicalTermCache putObjectIdCache
-                        (frozenCoreTerm closedBody)
-                , encodeCache do
-                    putCanonicalTermCache putObjectIdCache
-                        (frozenCoreTerm closedSelf)
-                ]
-    pure (NamedSetConstructionFact proposition descriptor)
-
-relationalSetConstructionTerm
-    :: Ord global
-    => CheckedRelationalSetConstruction global
-    -> ScopedCheckedCore global
-relationalSetConstructionTerm construction =
-    fromMaybe
-        (impossible "a checked relational construction lost its canonical term")
-        (checkedRelationalDerived
-            construction
-            (relationalConstructionContext construction)
-            TySet
-            (relationalConstructionCanonicalTerm construction))
-
--- | The exact source functionality obligation, still scoped by the outer
--- definition parameters.  It is discharged independently before the derived
--- extensional theorem can be authorized.
-relationalSetConstructionFunctionality
-    :: Ord global
-    => CheckedRelationalSetConstruction global
-    -> ScopedCheckedCore global
-relationalSetConstructionFunctionality construction =
-    fromMaybe
-        (impossible "a checked relational construction lost functionality")
-        (checkedRelationalDerived
-            construction
-            (relationalConstructionContext construction)
-            TyProp
-            (relationalConstructionFunctionalityTerm construction))
-
-relationalSetConstructionClosedFunctionality
-    :: Ord global
-    => CheckedRelationalSetConstruction global
-    -> FrozenCheckedCore global
-relationalSetConstructionClosedFunctionality =
-    closeRelationalFunctionality
-
--- | Introduce a fresh named set.  Assuming the exact checked functionality
--- proposition, derive its two local views; no arbitrary proposition can
--- unlock the extensional view.  The enclosing proof transaction owns the
--- corresponding authority.
-relationalSetConstructionLocalViews
-    :: Ord global
-    => SetConstructionFoundation
-    -> CheckedRelationalSetConstruction global
-    -> ScopedCheckedCore global
-    -> Maybe
-        ( ScopedCheckedCore global
-        , ScopedCheckedCore global
-        )
-relationalSetConstructionLocalViews foundation construction functionality = do
-    guard
-        (functionality
-            == relationalSetConstructionFunctionality construction)
-    validateRelationalSchema foundation construction
-    let context = TySet : relationalConstructionContext construction
-        target = CBound 0
-    extensional <- checkedRelationalDerived construction context TyProp
-        (CForall TySet
-            (CEq TyProp
-                (member (CBound 0) (CBound 1))
-                (shiftCanonical 1 1
-                    (relationalConstructionMembershipTerm construction))))
-    equation <- checkedRelationalDerived construction context TyProp
-        (CEq TySet
-            target
-            (shiftCanonical 1 0
-                (relationalConstructionCanonicalTerm construction)))
-    pure (extensional, equation)
-
-relationalSetConstructionClosedBody
-    :: Ord global
-    => CheckedRelationalSetConstruction global
-    -> FrozenCheckedCore global
-relationalSetConstructionClosedBody construction =
-    fromMaybe
-        (impossible "a checked relational construction did not close")
-        (freezeRelationalDerived construction closedType closedTerm)
-  where
-    context = relationalConstructionContext construction
-    closedType = foldr TyArrow TySet (reverse context)
-    closedTerm =
-        foldl
-            (flip CLam)
-            (relationalConstructionCanonicalTerm construction)
-            context
-
-data RelationalSetConstructionFact = RelationalSetConstructionFact
-    !(FrozenCheckedCore ObjectId)
-    !CacheDigest
-
-relationalSetConstructionFactProposition
-    :: RelationalSetConstructionFact
-    -> FrozenCheckedCore ObjectId
-relationalSetConstructionFactProposition
-        (RelationalSetConstructionFact proposition _descriptor) =
-    proposition
-
-relationalSetConstructionFactDescriptor
-    :: RelationalSetConstructionFact
-    -> CacheDigest
-relationalSetConstructionFactDescriptor
-        (RelationalSetConstructionFact _proposition descriptor) =
-    descriptor
-
--- | The direct relational schema is a deterministic theorem over the fixed
--- separation, choice-witness, and replacement rows.  The functionality fact
--- is a real strictly-earlier candidate: its exact proposition is checked here
--- and its authority safety is consumed separately by declaration admission.
-relationalSetConstructionObjectFact
-    :: SetConstructionFoundation
-    -> ObjectId
-    -> CheckedRelationalSetConstruction ObjectId
-    -> FrozenCheckedCore ObjectId
-    -> Maybe RelationalSetConstructionFact
-relationalSetConstructionObjectFact
-        foundation object construction functionality = do
-    let expectedFunctionality =
-            closeRelationalFunctionality construction
-    guard (functionality == expectedFunctionality)
-    validateRelationalSchema foundation construction
-    let context = relationalConstructionContext construction
-        objectType = foldr TyArrow TySet (reverse context)
-    globals <- insertGlobalType
-        object objectType (relationalConstructionGlobals construction)
-    let withObject = replaceRelationalGlobals globals construction
-        target =
-            foldl
-                CApp
-                (CGlobal object)
-                [ CBound (fromIntegral index)
-                | index <- reverse [0 .. length context - 1]
-                ]
-        membership = relationalConstructionMembershipTerm withObject
-    proposition <- freezeRelationalDerived withObject TyProp
-        (foldl
-            (flip CForall)
-            (CForall TySet
-                (CEq TyProp
-                    (member (CBound 0) (shiftCanonical 1 0 target))
-                    membership))
-            context)
-    closedSelf <- freezeRelationalDerived construction TyProp
-        (foldl
-            (flip CForall)
-            (CForall TySet
-                (CEq TyProp
-                    (member
-                        (CBound 0)
-                        (shiftCanonical 1 0
-                            (relationalConstructionCanonicalTerm construction)))
-                    (relationalConstructionMembershipTerm construction)))
-            context)
-    let closedBody = relationalSetConstructionClosedBody construction
-        descriptor =
-            hashCacheFields
-                "felix-checked-named-relational-set-construction-v1"
-                [ encodeCache do
-                    putCoreTypeCache (frozenCoreType closedBody)
-                    putCanonicalTermCache putObjectIdCache
-                        (frozenCoreTerm closedBody)
-                , encodeCache do
-                    putCanonicalTermCache putObjectIdCache
-                        (frozenCoreTerm expectedFunctionality)
-                , encodeCache do
-                    putCanonicalTermCache putObjectIdCache
-                        (frozenCoreTerm closedSelf)
-                ]
-    pure (RelationalSetConstructionFact proposition descriptor)
-
-finishConstruction
-    :: Ord global
-    => [CoreType]
-    -> Map.Map global CoreType
-    -> NamedSetConstructionShape global
-    -> Maybe (NamedSetConstruction global)
-finishConstruction context globals shape = do
-    let built = buildConstruction context shape
-        construction = NamedSetConstruction context globals shape built
-    _ <- checkedDerived construction context TySet
-        (builtConstructionTerm built)
-    _ <- checkedDerived construction (TySet : context) TyProp
-        (builtConstructionMembership built)
-    pure construction
-
-buildConstruction
-    :: Eq global
-    => [CoreType]
-    -> NamedSetConstructionShape global
-    -> BuiltSetConstruction global
-buildConstruction context = \case
-    SeparationShape bound predicate ->
-        let function = CLam TySet predicate
-            term = applyIntrinsic2 Sep bound function
-            membership =
-                logicalAnd
-                    (member (CBound 0) (shiftCanonical 1 0 bound))
-                    predicate
-            application =
-                characteristicApplication
-                    Sep context term
-                    [ (TySet, bound)
-                    , (TyArrow TySet TyProp, function)
-                    ]
-        in BuiltSetConstruction term membership [application]
-    FunctionalReplacementShape domains value condition ->
-        let (term, applications) =
-                buildFunctionalReplacement
-                    context
-                    domains
-                    value
-                    condition
-            domainList = NonEmpty.toList domains
-            binderCount = length domainList
-            terminal =
-                logicalConjunction
-                    ( maybeToList
-                        (shiftCanonical 1 (fromIntegral binderCount)
-                            <$> condition)
-                      <> [ CEq TySet
-                            (CBound (fromIntegral binderCount))
-                            (shiftCanonical 1
-                                (fromIntegral binderCount)
-                                value)
-                         ]
-                    )
-            membership =
-                foldr
-                    (\(depth, domain) rest ->
-                        logicalExists
-                            (logicalAnd
-                                (member
-                                    (CBound 0)
-                                    (shiftCanonical 1 0
-                                        (shiftCanonical 1 depth domain)))
-                                rest))
-                    terminal
-                    (zip [0 :: Natural ..] domainList)
-        in BuiltSetConstruction term membership applications
-
--- The only functional-replacement term builder.  Its result is reused by the
--- transparent body, exact-content matching, characteristic validation, local
--- views, and descriptor derivation.
-buildFunctionalReplacement
-    :: [CoreType]
-    -> NonEmpty (CanonicalTerm global)
-    -> CanonicalTerm global
-    -> Maybe (CanonicalTerm global)
-    -> (CanonicalTerm global, [CheckedCharacteristicApplication global])
-buildFunctionalReplacement context (domain :| remaining) value condition =
-    case remaining of
-        [] ->
-            let predicate = CLam TySet <$> condition
-                filtered = maybe domain
-                    (applyIntrinsic2 Sep domain)
-                    predicate
-                function = CLam TySet value
-                replacement = applyIntrinsic2 Repl filtered function
-                separationApplications = case predicate of
-                    Nothing -> []
-                    Just checkedPredicate ->
-                        [ characteristicApplication
-                            Sep context filtered
-                            [ (TySet, domain)
-                            , (TyArrow TySet TyProp, checkedPredicate)
-                            ]
-                        ]
-                replacementApplication =
-                    characteristicApplication
-                        Repl context replacement
-                        [ (TySet, filtered)
-                        , (TyArrow TySet TySet, function)
-                        ]
-            in
-                ( replacement
-                , separationApplications <> [replacementApplication]
-                )
-        next : rest ->
-            let (nested, nestedApplications) =
-                    buildFunctionalReplacement
-                        (TySet : context)
-                        (next :| rest)
-                        value
-                        condition
-                function = CLam TySet nested
-                replacement = applyIntrinsic2 Repl domain function
-                union = applyIntrinsic FamilyUnion replacement
-            in
-                ( union
-                , characteristicApplication
-                    Repl context replacement
-                    [ (TySet, domain)
-                    , (TyArrow TySet TySet, function)
-                    ]
-                  : characteristicApplication
-                        FamilyUnion context union
-                        [(TySet, replacement)]
-                  : nestedApplications
-                )
-
-characteristicApplication
-    :: CoreIntrinsicTag
-    -> [CoreType]
-    -> CanonicalTerm global
-    -> [(CoreType, CanonicalTerm global)]
-    -> CheckedCharacteristicApplication global
-characteristicApplication intrinsic context target arguments =
-    CheckedCharacteristicApplication
-        intrinsic
-        context
-        target
-        (NonEmpty.fromList arguments)
-        (expectedCharacteristicBody intrinsic arguments)
-
-expectedCharacteristicBody
-    :: CoreIntrinsicTag
-    -> [(CoreType, CanonicalTerm global)]
-    -> CanonicalTerm global
-expectedCharacteristicBody intrinsic arguments =
-    case (intrinsic, arguments) of
-        (Sep, [(_boundType, bound), (_predicateType, CLam TySet predicate)]) ->
-            logicalAnd
-                (member (CBound 0) (shiftCanonical 2 0 bound))
-                (shiftCanonical 1 1 predicate)
-        (Repl, [(_domainType, domain), (_functionType, CLam TySet value)]) ->
-            logicalExists
-                (logicalAnd
-                    (member (CBound 0) (shiftCanonical 3 0 domain))
-                    (CEq TySet
-                        (CBound 1)
-                        (shiftCanonical 2 1 value)))
-        (FamilyUnion, [(_familyType, family)]) ->
-            logicalExists
-                (logicalAnd
-                    (member (CBound 0) (shiftCanonical 3 0 family))
-                    (member (CBound 1) (CBound 0)))
-        _ ->
-            impossible "invalid checked set-construction characteristic"
-
-extensionalView
-    :: Ord global
-    => SetConstructionFoundation
-    -> CanonicalTerm global
-    -> NamedSetConstruction global
-    -> Maybe (ScopedCheckedCore global)
-extensionalView foundation target construction = do
-    traverse_
-        (validateCharacteristic foundation construction)
-        (constructionApplications construction)
-    checkedDerived construction (constructionContext construction) TyProp
-        (CForall TySet
-            (CEq TyProp
-                (member (CBound 0) (shiftCanonical 1 0 target))
-                (constructionMembership construction)))
-
--- Each primitive step is specialized from the actual fixed row, and the
--- complete normalized membership body is checked.  The final flattened view
--- is then the deterministic composition of these exact primitive schemas.
-validateCharacteristic
-    :: Ord global
-    => SetConstructionFoundation
-    -> NamedSetConstruction global
-    -> CheckedCharacteristicApplication global
-    -> Maybe ()
-validateCharacteristic foundation construction
-        (CheckedCharacteristicApplication
-            intrinsic context targetTerm argumentTerms expectedBody) = do
-    row <- characteristicRow foundation intrinsic
-    target <- checkedDerived construction context TySet targetTerm
-    arguments <- traverse
-        (\(coreType, term) ->
-            checkedDerived construction context coreType term)
-        argumentTerms
-    specialized <- scopedCharacteristicDefinition row target arguments
-    case scopedCoreTerm specialized of
-        CForall TySet
-                (CEq TyProp actualMembership actualBody)
-            | actualMembership
-                == member (CBound 0) (CBound 1)
-            , scopedCoreContext specialized
-                == TySet : scopedCoreContext target
-            , actualBody == expectedBody ->
-                pure ()
-        _ -> Nothing
-
-characteristicRow
-    :: SetConstructionFoundation
-    -> CoreIntrinsicTag
-    -> Maybe (FrozenCheckedCore Void)
-characteristicRow
-        (SetConstructionFoundation
-            familyUnion separation replacement _setChoose) =
-    \case
-        FamilyUnion -> Just familyUnion
-        Sep -> Just separation
-        Repl -> Just replacement
-        _ -> Nothing
-
-validateRelationalSchema
-    :: Ord global
-    => SetConstructionFoundation
-    -> CheckedRelationalSetConstruction global
-    -> Maybe ()
-validateRelationalSchema foundation construction = do
-    traverse_
-        (validateRelationalCharacteristic foundation construction)
-        (relationalConstructionApplications construction)
-    validateChoiceWitness foundation construction
-
-validateRelationalCharacteristic
-    :: Ord global
-    => SetConstructionFoundation
-    -> CheckedRelationalSetConstruction global
-    -> CheckedCharacteristicApplication global
-    -> Maybe ()
-validateRelationalCharacteristic foundation construction
-        (CheckedCharacteristicApplication
-            intrinsic context targetTerm argumentTerms expectedBody) = do
-    row <- characteristicRow foundation intrinsic
-    target <- checkedRelationalDerived construction context TySet targetTerm
-    arguments <- traverse
-        (\(coreType, term) ->
-            checkedRelationalDerived construction context coreType term)
-        argumentTerms
-    specialized <- scopedCharacteristicDefinition row target arguments
-    case scopedCoreTerm specialized of
-        CForall TySet (CEq TyProp actualMembership actualBody)
-            | actualMembership == member (CBound 0) (CBound 1)
-            , scopedCoreContext specialized
-                == TySet : scopedCoreContext target
-            , actualBody == expectedBody ->
-                pure ()
-        _ -> Nothing
-
-validateChoiceWitness
-    :: Ord global
-    => SetConstructionFoundation
-    -> CheckedRelationalSetConstruction global
-    -> Maybe ()
-validateChoiceWitness
-        (SetConstructionFoundation
-            _familyUnion _separation _replacement setChoose)
-        construction = do
-    let context = relationalConstructionContext construction
-        relation = relationalConstructionRelation construction
-        predicate = CLam TySet relation
-        choice = applyIntrinsic SetChoose predicate
-        witnessContext = TySet : TySet : context
-    target <- checkedRelationalDerived construction witnessContext TySet
-        (shiftCanonical 1 0 choice)
-    checkedPredicate <-
-        checkedRelationalDerived construction witnessContext
-            (TyArrow TySet TyProp)
-            (shiftCanonical 1 0 predicate)
-    witness <- checkedRelationalDerived construction witnessContext TySet
-        (CBound 0)
-    specialized <-
-        scopedCharacteristicDefinition
-            setChoose target (checkedPredicate :| [witness])
-    guard
-        (scopedCoreContext specialized
-            == TySet : TySet : TySet : context)
-    guard
-        (scopedCoreTerm specialized
-            == CImp
-                (shiftCanonical 1 0 relation)
-                (shiftCanonical 1 1 relation))
-
-relationalFunctionality
-    :: CanonicalTerm global
-    -> CanonicalTerm global
-    -> CanonicalTerm global
-relationalFunctionality domain relation =
-    CForall TySet
-        (CImp
-            (member (CBound 0) (shiftCanonical 1 0 domain))
-            (CForall TySet
-                (CForall TySet
-                    (CImp
-                        (logicalAnd
-                            (shiftCanonical 1 0 relation)
-                            (shiftCanonical 1 1 relation))
-                        (CEq TySet (CBound 1) (CBound 0))))))
-
-relationalMembership
-    :: CanonicalTerm global
-    -> CanonicalTerm global
-    -> CanonicalTerm global
-relationalMembership domain relation =
-    logicalExists
-        (logicalAnd
-            (member (CBound 0) (shiftCanonical 2 0 domain))
-            (applyRelation
-                (shiftCanonical 2 0
-                    (CLam TySet (CLam TySet relation)))
-                (CBound 0)
-                (CBound 1)))
-  where
-    applyRelation function domainValue rangeValue =
-        case function of
-            CLam TySet domainBody ->
-                case instantiateCanonical domainValue domainBody of
-                    CLam TySet rangeBody ->
-                        instantiateCanonical rangeValue rangeBody
-                    _ -> impossible "a checked relation lost its range binder"
-            _ -> impossible "a checked relation lost its domain binder"
-
-weakenConstruction
-    :: Ord global
-    => CoreType
-    -> NamedSetConstruction global
-    -> Maybe (NamedSetConstruction global)
-weakenConstruction binderType construction =
-    finishConstruction
-        (binderType : constructionContext construction)
-        (constructionGlobals construction)
-        (case constructionShape construction of
-            SeparationShape bound predicate ->
-                SeparationShape
-                    (shiftCanonical 1 0 bound)
-                    (shiftCanonical 1 1 predicate)
-            FunctionalReplacementShape domains value condition ->
-                let domainList = NonEmpty.toList domains
-                    weakenedDomains =
-                        zipWith
-                            (\depth domain -> shiftCanonical 1 depth domain)
-                            [0..]
-                            domainList
-                    binderDepth = fromIntegral (length domainList)
-                in FunctionalReplacementShape
-                    (NonEmpty.fromList weakenedDomains)
-                    (shiftCanonical 1 binderDepth value)
-                    (shiftCanonical 1 binderDepth <$> condition))
-
-captureGlobalTypes
-    :: Ord global
-    => (global -> Maybe CoreType)
-    -> [CanonicalTerm global]
-    -> Maybe (Map.Map global CoreType)
-captureGlobalTypes globalType terms =
-    Map.fromList <$> traverse capture
-        (Set.toAscList (foldMap canonicalTermGlobals terms))
-  where
-    capture global = do
-        coreType <- globalType global
-        pure (global, coreType)
-
-insertGlobalType
-    :: Ord global
-    => global
-    -> CoreType
-    -> Map.Map global CoreType
-    -> Maybe (Map.Map global CoreType)
-insertGlobalType global coreType globals =
-    case Map.lookup global globals of
-        Nothing -> Just (Map.insert global coreType globals)
-        Just existing
-            | existing == coreType -> Just globals
-            | otherwise -> Nothing
-
-checkedDerived
-    :: Ord global
-    => NamedSetConstruction global
-    -> [CoreType]
-    -> CoreType
-    -> CanonicalTerm global
-    -> Maybe (ScopedCheckedCore global)
-checkedDerived construction context expected term = do
-    checked <- either (const Nothing) Just
-        (checkScopedCanonicalCore
-            (`Map.lookup` constructionGlobals construction)
-            context
-            term)
-    guard (scopedCoreType checked == expected)
-    pure checked
-
-freezeDerived
-    :: Ord global
-    => NamedSetConstruction global
-    -> CoreType
-    -> CanonicalTerm global
-    -> Maybe (FrozenCheckedCore global)
-freezeDerived construction expected term = do
-    checked <- checkedDerived construction [] expected term
-    closeScopedCore checked
-
-checkedRelationalDerived
-    :: Ord global
-    => CheckedRelationalSetConstruction global
-    -> [CoreType]
-    -> CoreType
-    -> CanonicalTerm global
-    -> Maybe (ScopedCheckedCore global)
-checkedRelationalDerived construction context expected term = do
-    checked <- either (const Nothing) Just
-        (checkScopedCanonicalCore
-            (`Map.lookup` relationalConstructionGlobals construction)
-            context
-            term)
-    guard (scopedCoreType checked == expected)
-    pure checked
-
-freezeRelationalDerived
-    :: Ord global
-    => CheckedRelationalSetConstruction global
-    -> CoreType
-    -> CanonicalTerm global
-    -> Maybe (FrozenCheckedCore global)
-freezeRelationalDerived construction expected term = do
-    checked <- checkedRelationalDerived construction [] expected term
-    closeScopedCore checked
-
-closeRelationalFunctionality
-    :: Ord global
-    => CheckedRelationalSetConstruction global
-    -> FrozenCheckedCore global
-closeRelationalFunctionality construction =
-    fromMaybe
-        (impossible "a relational functionality proposition did not close")
-        (freezeRelationalDerived construction TyProp
-            (foldl
-                (flip CForall)
-                (relationalConstructionFunctionalityTerm construction)
-                (relationalConstructionContext construction)))
-
-replaceRelationalGlobals
-    :: Map.Map global CoreType
-    -> CheckedRelationalSetConstruction global
-    -> CheckedRelationalSetConstruction global
-replaceRelationalGlobals globals
-        (CheckedRelationalSetConstruction
-            context _oldGlobals domain relation term functionality
-            membership applications) =
-    CheckedRelationalSetConstruction
-        context globals domain relation term functionality membership applications
-
-relationalConstructionContext
-    :: CheckedRelationalSetConstruction global
-    -> [CoreType]
-relationalConstructionContext
-        (CheckedRelationalSetConstruction
-            context _globals _domain _relation _term _functionality
-            _membership _applications) =
-    context
-
-relationalConstructionGlobals
-    :: CheckedRelationalSetConstruction global
-    -> Map.Map global CoreType
-relationalConstructionGlobals
-        (CheckedRelationalSetConstruction
-            _context globals _domain _relation _term _functionality
-            _membership _applications) =
-    globals
-
-relationalConstructionRelation
-    :: CheckedRelationalSetConstruction global
-    -> CanonicalTerm global
-relationalConstructionRelation
-        (CheckedRelationalSetConstruction
-            _context _globals _domain relation _term _functionality
-            _membership _applications) =
-    relation
-
-relationalConstructionCanonicalTerm
-    :: CheckedRelationalSetConstruction global
-    -> CanonicalTerm global
-relationalConstructionCanonicalTerm
-        (CheckedRelationalSetConstruction
-            _context _globals _domain _relation term _functionality
-            _membership _applications) =
-    term
-
-relationalConstructionFunctionalityTerm
-    :: CheckedRelationalSetConstruction global
-    -> CanonicalTerm global
-relationalConstructionFunctionalityTerm
-        (CheckedRelationalSetConstruction
-            _context _globals _domain _relation _term functionality
-            _membership _applications) =
-    functionality
-
-relationalConstructionMembershipTerm
-    :: CheckedRelationalSetConstruction global
-    -> CanonicalTerm global
-relationalConstructionMembershipTerm
-        (CheckedRelationalSetConstruction
-            _context _globals _domain _relation _term _functionality
-            membership _applications) =
-    membership
-
-relationalConstructionApplications
-    :: CheckedRelationalSetConstruction global
-    -> [CheckedCharacteristicApplication global]
-relationalConstructionApplications
-        (CheckedRelationalSetConstruction
-            _context _globals _domain _relation _term _functionality
-            _membership applications) =
-    applications
-
-replaceConstructionGlobals
-    :: Map.Map global CoreType
-    -> NamedSetConstruction global
-    -> NamedSetConstruction global
-replaceConstructionGlobals globals
-        (NamedSetConstruction context _oldGlobals shape built) =
-    NamedSetConstruction context globals shape built
-
-constructionContext :: NamedSetConstruction global -> [CoreType]
-constructionContext (NamedSetConstruction context _globals _shape _built) =
-    context
-
-constructionGlobals
-    :: NamedSetConstruction global
-    -> Map.Map global CoreType
-constructionGlobals (NamedSetConstruction _context globals _shape _built) =
-    globals
-
-constructionShape
-    :: NamedSetConstruction global
-    -> NamedSetConstructionShape global
-constructionShape (NamedSetConstruction _context _globals shape _built) =
-    shape
-
-constructionCanonicalTerm
-    :: NamedSetConstruction global
-    -> CanonicalTerm global
-constructionCanonicalTerm
-        (NamedSetConstruction _context _globals _shape built) =
-    builtConstructionTerm built
-
-constructionMembership
-    :: NamedSetConstruction global
-    -> CanonicalTerm global
-constructionMembership
-        (NamedSetConstruction _context _globals _shape built) =
-    builtConstructionMembership built
-
-constructionApplications
-    :: NamedSetConstruction global
-    -> [CheckedCharacteristicApplication global]
-constructionApplications
-        (NamedSetConstruction _context _globals _shape built) =
-    builtConstructionApplications built
-
-builtConstructionTerm
-    :: BuiltSetConstruction global
-    -> CanonicalTerm global
-builtConstructionTerm (BuiltSetConstruction term _membership _applications) =
-    term
-
-builtConstructionMembership
-    :: BuiltSetConstruction global
-    -> CanonicalTerm global
-builtConstructionMembership
-        (BuiltSetConstruction _term membership _applications) =
-    membership
-
-builtConstructionApplications
-    :: BuiltSetConstruction global
-    -> [CheckedCharacteristicApplication global]
-builtConstructionApplications
-        (BuiltSetConstruction _term _membership applications) =
-    applications
-
-applyIntrinsic
-    :: CoreIntrinsicTag
-    -> CanonicalTerm global
-    -> CanonicalTerm global
-applyIntrinsic intrinsic argument =
-    CApp (CIntrinsic intrinsic) argument
-
-applyIntrinsic2
-    :: CoreIntrinsicTag
-    -> CanonicalTerm global
-    -> CanonicalTerm global
-    -> CanonicalTerm global
-applyIntrinsic2 intrinsic first second =
-    CApp (CApp (CIntrinsic intrinsic) first) second
-
-member
-    :: CanonicalTerm global
-    -> CanonicalTerm global
-    -> CanonicalTerm global
-member = applyIntrinsic2 Member
-
-logicalNot :: CanonicalTerm global -> CanonicalTerm global
-logicalNot proposition = CImp proposition CFalsum
-
-logicalAnd
-    :: CanonicalTerm global
-    -> CanonicalTerm global
-    -> CanonicalTerm global
-logicalAnd left right =
-    logicalNot (CImp left (logicalNot right))
-
-logicalTruth :: CanonicalTerm global
-logicalTruth = CImp CFalsum CFalsum
-
-logicalConjunction
-    :: Eq global
-    => [CanonicalTerm global]
-    -> CanonicalTerm global
-logicalConjunction =
-    foldr combine logicalTruth
-  where
-    combine proposition remaining
-        | proposition == logicalTruth = remaining
-        | remaining == logicalTruth = proposition
-        | otherwise = logicalAnd proposition remaining
-
-logicalExists :: CanonicalTerm global -> CanonicalTerm global
-logicalExists body =
-    logicalNot (CForall TySet (logicalNot body))