Centralize checked set constructions

5 files changed, 768 insertions, 583 deletions

diff --git a/source/Checking/Core.hs b/source/Checking/Core.hs
index c9d8472..61a5617 100644
--- a/source/Checking/Core.hs
+++ b/source/Checking/Core.hs
@@ -48,17 +48,6 @@ module Checking.Core
     , embedClosedCore
     , weakenCheckedScopedCore
     , weakenScopedCore
-    , NamedSetConstruction
-    , checkedSeparationConstruction
-    , checkedFunctionalReplacementConstruction
-    , namedSetConstructionTerm
-    , weakenNamedSetConstruction
-    , namedSetConstructionEquationView
-    , namedSetConstructionExtensionalView
-    , namedSetConstructionLocalViews
-    , namedSetConstructionObjectView
-    , namedSetConstructionClosedTerm
-    , namedSetConstructionClosedSelfView
     , scopedSetDefinition
     , scopedCharacteristicDefinition
     , scopedReplacementGraph
@@ -72,6 +61,7 @@ module Checking.Core
     , openScopedAssumption
     , closeScopedCore
     , instantiateCanonical
+    , shiftCanonical
     , mapCanonicalGlobals
     , canonicalTermGlobals
     , checkCanonicalCore
@@ -85,7 +75,6 @@ import Base hiding (Empty)
 import Bound
 import Control.DeepSeq (NFData)
 import Control.Monad (ap, unless)
-import Data.List.NonEmpty qualified as NonEmpty
 import Data.Set qualified as Set
 import Numeric.Natural (Natural)
 
@@ -712,494 +701,6 @@ weakenScopedCore globalType binderType scoped =
         (shiftCanonical 1 0
             (scopedCoreTerm scoped))
 
--- | One source-owned separation or functional-replacement construction after
--- all of its components have been checked in their exact lexical contexts.
--- The constructors stay private: named-definition views may be obtained only
--- from one of the checked smart constructors below.
-data NamedSetConstruction global
-    = NamedSeparationConstruction
-        ![CoreType]
-        !(CanonicalTerm global)
-        !(CanonicalTerm global)
-    | NamedFunctionalReplacementConstruction
-        ![CoreType]
-        !(NonEmpty (CanonicalTerm global))
-        !(CanonicalTerm global)
-        !(Maybe (CanonicalTerm global))
-    deriving stock (Eq)
-
--- | Check the source decomposition of a separation.  The predicate body is
--- checked under exactly one additional set binder.
-checkedSeparationConstruction
-    :: ScopedCheckedCore global
-    -> ScopedCheckedCore global
-    -> Maybe (NamedSetConstruction global)
-checkedSeparationConstruction
-        (ScopedCheckedCore context TySet bound)
-        (ScopedCheckedCore predicateContext TyProp predicate)
-    | predicateContext == TySet : context =
-        Just (NamedSeparationConstruction context bound predicate)
-checkedSeparationConstruction _bound _predicate =
-    Nothing
-
--- | Check a source-ordered functional replacement.  Its @i@th domain is
--- checked beneath the preceding @i - 1@ source binders, while the value and
--- optional condition are checked beneath all binders.
-checkedFunctionalReplacementConstruction
-    :: NonEmpty (ScopedCheckedCore global)
-    -> ScopedCheckedCore global
-    -> Maybe (ScopedCheckedCore global)
-    -> Maybe (NamedSetConstruction global)
-checkedFunctionalReplacementConstruction domains value condition = do
-    let domainList = NonEmpty.toList domains
-    firstDomain <- listToMaybe domainList
-    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
-    pure
-        (NamedFunctionalReplacementConstruction
-            context
-            (scopedCoreTerm <$> domains)
-            (scopedCoreTerm value)
-            (scopedCoreTerm <$> condition))
-
-namedSetConstructionTerm
-    :: NamedSetConstruction global
-    -> ScopedCheckedCore global
-namedSetConstructionTerm construction =
-    ScopedCheckedCore
-        (namedSetConstructionContext construction)
-        TySet
-        (constructionTerm construction)
-
--- | Add one outer lexical binder without changing any construction-local
--- binder.  Inserting at the exact local depth preserves every source bound.
-weakenNamedSetConstruction
-    :: CoreType
-    -> NamedSetConstruction global
-    -> NamedSetConstruction global
-weakenNamedSetConstruction binderType = \case
-    NamedSeparationConstruction context bound predicate ->
-        NamedSeparationConstruction
-            (binderType : context)
-            (shiftCanonical 1 0 bound)
-            (shiftCanonical 1 1 predicate)
-    NamedFunctionalReplacementConstruction
-            context domains value condition ->
-        let domainList = NonEmpty.toList domains
-            weakenedDomains =
-                zipWith
-                    (\depth domain -> shiftCanonical 1 depth domain)
-                    [0..]
-                    domainList
-            binderDepth = fromIntegral (length domainList)
-        in NamedFunctionalReplacementConstruction
-            (binderType : context)
-            (NonEmpty.fromList weakenedDomains)
-            (shiftCanonical 1 binderDepth value)
-            (shiftCanonical 1 binderDepth <$> condition)
-
--- | The exact higher-order equation for one named construction target.
-namedSetConstructionEquationView
-    :: ScopedCheckedCore global
-    -> NamedSetConstruction global
-    -> Maybe (ScopedCheckedCore global)
-namedSetConstructionEquationView
-        (ScopedCheckedCore targetContext TySet target)
-        construction
-    | targetContext == namedSetConstructionContext construction =
-        Just
-            (ScopedCheckedCore
-                targetContext
-                TyProp
-                (CEq TySet target (constructionTerm construction)))
-namedSetConstructionEquationView _target _construction =
-    Nothing
-
--- | Derive the flattened membership view of a named construction.  Before
--- exposing it, specialize the checked foundation characteristic at every
--- construction layer.  Thus this structural derivation is tied to the fixed
--- foundation rows instead of trusting a caller-provided proposition.
-namedSetConstructionExtensionalView
-    :: Eq global
-    => (CoreIntrinsicTag -> Maybe (FrozenCheckedCore Void))
-    -> ScopedCheckedCore global
-    -> NamedSetConstruction global
-    -> Maybe (ScopedCheckedCore global)
-namedSetConstructionExtensionalView characteristic target construction = do
-    guard
-        (scopedCoreType target == TySet
-            && scopedCoreContext target
-                == namedSetConstructionContext construction)
-    guard (constructionCharacteristicsCheck characteristic construction)
-    pure
-        (ScopedCheckedCore
-            (scopedCoreContext target)
-            TyProp
-            (CForall TySet
-                (CEq TyProp
-                    (member
-                        (CBound 0)
-                        (shiftCanonical 1 0
-                            (scopedCoreTerm target)))
-                    (constructionMembershipBody construction))))
-
--- | Introduce one fresh nearest set binder and expose the adjacent
--- first-order and exact-equation views of one proof-local definition.
-namedSetConstructionLocalViews
-    :: Eq global
-    => (CoreIntrinsicTag -> Maybe (FrozenCheckedCore Void))
-    -> NamedSetConstruction global
-    -> Maybe
-        ( ScopedCheckedCore global
-        , ScopedCheckedCore global
-        )
-namedSetConstructionLocalViews characteristic construction = do
-    let weakened = weakenNamedSetConstruction TySet construction
-        target =
-            ScopedCheckedCore
-                (TySet : namedSetConstructionContext construction)
-                TySet
-                (CBound 0)
-    extensional <-
-        namedSetConstructionExtensionalView
-            characteristic target weakened
-    equation <- namedSetConstructionEquationView target weakened
-    pure (extensional, equation)
-
--- | Close the flattened view of a top-level transparent construction around
--- the source parameters and apply the committed object in source order.
-namedSetConstructionObjectView
-    :: Eq global
-    => (CoreIntrinsicTag -> Maybe (FrozenCheckedCore Void))
-    -> global
-    -> NamedSetConstruction global
-    -> Maybe (FrozenCheckedCore global)
-namedSetConstructionObjectView characteristic object construction = do
-    let context = namedSetConstructionContext construction
-        parameterCount = length context
-        target =
-            ScopedCheckedCore
-                context
-                TySet
-                (foldl
-                    CApp
-                    (CGlobal object)
-                    [ CBound (fromIntegral index)
-                    | index <- reverse [0 .. parameterCount - 1]
-                    ])
-    view <-
-        namedSetConstructionExtensionalView
-            characteristic target construction
-    pure
-        (FrozenCheckedCore
-            TyProp
-            (foldl
-                (flip CForall)
-                (scopedCoreTerm view)
-                context))
-
--- | Closed canonical content used to bind a transient checked construction
--- to a transparent object without entering mathematical identity.
-namedSetConstructionClosedTerm
-    :: NamedSetConstruction global
-    -> FrozenCheckedCore global
-namedSetConstructionClosedTerm construction =
-    FrozenCheckedCore
-        (foldr TyArrow TySet
-            (reverse (namedSetConstructionContext construction)))
-        (foldl
-            (flip CLam)
-            (constructionTerm construction)
-            (namedSetConstructionContext construction))
-
--- | A closed, target-independent description of the flattened view.  It is
--- used only by cache-scoped authority association; the public fact substitutes
--- the actual transparent object as its target.
-namedSetConstructionClosedSelfView
-    :: Eq global
-    => (CoreIntrinsicTag -> Maybe (FrozenCheckedCore Void))
-    -> NamedSetConstruction global
-    -> Maybe (FrozenCheckedCore global)
-namedSetConstructionClosedSelfView characteristic construction = do
-    view <-
-        namedSetConstructionExtensionalView
-            characteristic
-            (namedSetConstructionTerm construction)
-            construction
-    pure
-        (FrozenCheckedCore
-            TyProp
-            (foldl
-                (flip CForall)
-                (scopedCoreTerm view)
-                (scopedCoreContext view)))
-
-namedSetConstructionContext
-    :: NamedSetConstruction global
-    -> [CoreType]
-namedSetConstructionContext = \case
-    NamedSeparationConstruction context _bound _predicate -> context
-    NamedFunctionalReplacementConstruction
-            context _domains _value _condition -> context
-
-constructionTerm
-    :: NamedSetConstruction global
-    -> CanonicalTerm global
-constructionTerm = \case
-    NamedSeparationConstruction _context bound predicate ->
-        CApp
-            (CApp (CIntrinsic Sep) bound)
-            (CLam TySet predicate)
-    NamedFunctionalReplacementConstruction
-            _context domains value condition ->
-        functionalTerm
-            (NonEmpty.toList domains)
-            value
-            condition
-  where
-    functionalTerm (domain : remaining) result predicate =
-        case remaining of
-            [] ->
-                let filtered = case predicate of
-                        Nothing -> domain
-                        Just body ->
-                            CApp
-                                (CApp (CIntrinsic Sep) domain)
-                                (CLam TySet body)
-                in CApp
-                    (CApp (CIntrinsic Repl) filtered)
-                    (CLam TySet result)
-            next : rest ->
-                CApp
-                    (CIntrinsic FamilyUnion)
-                    (CApp
-                        (CApp (CIntrinsic Repl) domain)
-                        (CLam TySet
-                            (functionalTerm (next : rest) result predicate)))
-    functionalTerm [] _result _predicate =
-        impossible "a checked functional replacement has no domain"
-
-constructionMembershipBody
-    :: Eq global
-    => NamedSetConstruction global
-    -> CanonicalTerm global
-constructionMembershipBody = \case
-    NamedSeparationConstruction _context bound predicate ->
-        logicalAndCore
-            (member (CBound 0) (shiftCanonical 1 0 bound))
-            predicate
-    NamedFunctionalReplacementConstruction
-            _context domains value condition ->
-        let domainList = NonEmpty.toList domains
-            binderCount = length domainList
-            terminal =
-                logicalConjunctionCore
-                    ( maybeToList
-                        (shiftCanonical 1 (fromIntegral binderCount)
-                            <$> condition)
-                        <> [ CEq TySet
-                                (CBound (fromIntegral binderCount))
-                                (shiftCanonical 1
-                                    (fromIntegral binderCount)
-                                    value)
-                           ]
-                    )
-        in foldr
-            (\(depth, domain) rest ->
-                logicalExistsCore
-                    (logicalAndCore
-                        (member
-                            (CBound 0)
-                            (shiftCanonical 1 0
-                                (shiftCanonical 1
-                                    depth
-                                    domain)))
-                        rest))
-            terminal
-            (zip [0 :: Natural ..] domainList)
-
-constructionCharacteristicsCheck
-    :: Eq global
-    => (CoreIntrinsicTag -> Maybe (FrozenCheckedCore Void))
-    -> NamedSetConstruction global
-    -> Bool
-constructionCharacteristicsCheck characteristic = \case
-    construction@(NamedSeparationConstruction context bound predicate) ->
-        validates Sep construction
-            [ ScopedCheckedCore context TySet bound
-            , ScopedCheckedCore context
-                (TyArrow TySet TyProp)
-                (CLam TySet predicate)
-            ]
-    NamedFunctionalReplacementConstruction
-            context domains value condition ->
-        validateFunctional
-            context
-            (NonEmpty.toList domains)
-            value
-            condition
-  where
-    validates intrinsic construction arguments =
-        case characteristic intrinsic of
-            Nothing -> False
-            Just row ->
-                isJust
-                    (scopedCharacteristicDefinition
-                        row
-                        (namedSetConstructionTerm construction)
-                        (NonEmpty.fromList arguments))
-
-    validateTerm intrinsic context term arguments =
-        case characteristic intrinsic of
-            Nothing -> False
-            Just row ->
-                isJust
-                    (scopedCharacteristicDefinition
-                        row
-                        (ScopedCheckedCore context TySet term)
-                        (NonEmpty.fromList arguments))
-
-    validateFunctional outer domains value condition =
-        case domains of
-            [] -> False
-            domain : remaining ->
-                case remaining of
-                    [] ->
-                        let predicate = CLam TySet <$> condition
-                            filtered = case predicate of
-                                Nothing -> domain
-                                Just body ->
-                                    CApp
-                                        (CApp (CIntrinsic Sep) domain)
-                                        body
-                            function = CLam TySet value
-                            replacement =
-                                CApp
-                                    (CApp (CIntrinsic Repl) filtered)
-                                    function
-                            separationOk = case predicate of
-                                Nothing -> True
-                                Just body ->
-                                    validateTerm Sep outer filtered
-                                        [ ScopedCheckedCore outer TySet domain
-                                        , ScopedCheckedCore outer
-                                            (TyArrow TySet TyProp)
-                                            body
-                                        ]
-                        in separationOk
-                            && validateTerm Repl outer replacement
-                                [ ScopedCheckedCore outer TySet filtered
-                                , ScopedCheckedCore outer
-                                    (TyArrow TySet TySet)
-                                    function
-                                ]
-                    next : rest ->
-                        let innerContext = TySet : outer
-                            nested =
-                                functionalTermUnchecked
-                                    (next : rest)
-                                    value
-                                    condition
-                            function = CLam TySet nested
-                            replacement =
-                                CApp
-                                    (CApp (CIntrinsic Repl) domain)
-                                    function
-                            union = CApp (CIntrinsic FamilyUnion) replacement
-                        in validateFunctional
-                                innerContext (next : rest) value condition
-                            && validateTerm Repl outer replacement
-                                [ ScopedCheckedCore outer TySet domain
-                                , ScopedCheckedCore outer
-                                    (TyArrow TySet TySet)
-                                    function
-                                ]
-                            && validateTerm FamilyUnion outer union
-                                [ScopedCheckedCore outer TySet replacement]
-
-    functionalTermUnchecked (domain : remaining) result predicate =
-        case remaining of
-            [] ->
-                CApp
-                    (CApp
-                        (CIntrinsic Repl)
-                        (case predicate of
-                            Nothing -> domain
-                            Just body ->
-                                CApp
-                                    (CApp (CIntrinsic Sep) domain)
-                                    (CLam TySet body)))
-                    (CLam TySet result)
-            next : rest ->
-                CApp
-                    (CIntrinsic FamilyUnion)
-                    (CApp
-                        (CApp (CIntrinsic Repl) domain)
-                        (CLam TySet
-                            (functionalTermUnchecked
-                                (next : rest) result predicate)))
-    functionalTermUnchecked [] _result _predicate =
-        impossible "a checked functional replacement has no domain"
-
-member
-    :: CanonicalTerm global
-    -> CanonicalTerm global
-    -> CanonicalTerm global
-member element set =
-    CApp (CApp (CIntrinsic Member) element) set
-
-logicalNotCore :: CanonicalTerm global -> CanonicalTerm global
-logicalNotCore proposition = CImp proposition CFalsum
-
-logicalAndCore
-    :: CanonicalTerm global
-    -> CanonicalTerm global
-    -> CanonicalTerm global
-logicalAndCore left right =
-    logicalNotCore (CImp left (logicalNotCore right))
-
-logicalTruthCore :: CanonicalTerm global
-logicalTruthCore = CImp CFalsum CFalsum
-
-logicalConjunctionCore
-    :: Eq global
-    => [CanonicalTerm global]
-    -> CanonicalTerm global
-logicalConjunctionCore =
-    foldr combine logicalTruthCore
-  where
-    combine proposition remaining
-        | proposition == logicalTruthCore = remaining
-        | remaining == logicalTruthCore = proposition
-        | otherwise = logicalAndCore proposition remaining
-
-logicalExistsCore :: CanonicalTerm global -> CanonicalTerm global
-logicalExistsCore body =
-    logicalNotCore (CForall TySet (logicalNotCore body))
-
 -- | Introduce a fresh set-valued local definition. Separation specializes
 -- the checked foundation characteristic so its local premise remains
 -- first-order.
diff --git a/source/Checking/Declaration.hs b/source/Checking/Declaration.hs
index ee795f0..b114954 100644
--- a/source/Checking/Declaration.hs
+++ b/source/Checking/Declaration.hs
@@ -175,13 +175,9 @@ import Checking.Identity
 import Checking.Kernel.Derivation
 import Checking.Semantic
 import Checking.Materialization qualified as Materialization
+import Checking.SetConstruction
 import Felix.Cache.Codec
-    ( CacheDigest
-    , encodeCache
-    , hashCacheFields
-    , putCanonicalTermCache
-    , putCoreTypeCache
-    )
+    ( encodeCache )
 import Felix.Module
 import Provers qualified
 import Report.Location
@@ -2186,71 +2182,27 @@ prepareNamedSetConstruction
         DeclarationError
         (FrozenCheckedCore ObjectId, KernelConstructionDescriptor)
 prepareNamedSetConstruction foundation closure identity construction = do
-    let expectedContent = namedSetConstructionClosedTerm construction
+    let expectedContent = namedSetConstructionClosedBody construction
     case lookupCheckedObjectContent identity closure of
         Just (TransparentObjectContent _theory coreType body)
             | coreType == frozenCoreType expectedContent
             , body == frozenCoreTerm expectedContent -> pure ()
         _ -> Left KernelConstructionDescriptorMismatch
-    proposition <-
+    derived <-
         maybe
             (Left KernelConstructionDescriptorMismatch)
             Right
-            (namedSetConstructionObjectView
-                (constructionCharacteristic foundation)
+            (namedSetConstructionObjectFact
+                (checkedFoundationSetConstruction foundation)
                 identity
                 construction)
-    descriptorId <-
-        namedSetConstructionDescriptorId foundation construction
     pure
-        ( proposition
-        , CheckedSetConstructionExtensionality identity descriptorId
+        ( namedSetConstructionFactProposition derived
+        , CheckedSetConstructionExtensionality
+            identity
+            (namedSetConstructionFactDescriptor derived)
         )
 
-namedSetConstructionDescriptorId
-    :: CheckedFoundation
-    -> NamedSetConstruction ObjectId
-    -> Either DeclarationError CacheDigest
-namedSetConstructionDescriptorId foundation construction = do
-    selfView <-
-        maybe
-            (Left KernelConstructionDescriptorMismatch)
-            Right
-            (namedSetConstructionClosedSelfView
-                (constructionCharacteristic foundation)
-                construction)
-    let closedTerm = namedSetConstructionClosedTerm construction
-    pure
-        (hashCacheFields
-            "felix-checked-named-set-construction-v1"
-            [ encodeCache do
-                putCoreTypeCache (frozenCoreType closedTerm)
-                putCanonicalTermCache putObjectIdCache
-                    (frozenCoreTerm closedTerm)
-            , encodeCache do
-                putCanonicalTermCache putObjectIdCache
-                    (frozenCoreTerm selfView)
-            ])
-
-constructionCharacteristic
-    :: CheckedFoundation
-    -> CoreIntrinsicTag
-    -> Maybe (FrozenCheckedCore Void)
-constructionCharacteristic foundation = \case
-    FamilyUnion ->
-        Just
-            (foundationAxiomFrozen
-                foundation FamilyUnionCharacteristic)
-    Sep ->
-        Just
-            (foundationAxiomFrozen
-                foundation SeparationCharacteristic)
-    Repl ->
-        Just
-            (foundationAxiomFrozen
-                foundation ReplacementCharacteristic)
-    _ -> Nothing
-
 preparePointwiseDefinitionEquationSpec
     :: CheckedObjectClosure
     -> ObjectId
@@ -3770,25 +3722,16 @@ authorizeNamedSetConstructionCandidate
 authorizeNamedSetConstructionCandidate identity construction candidate =
     authorizeOneCandidate candidate \initial -> do
         let builder = candidateProofBuilder initial
-        expectedDescriptor <-
+        (expected, descriptor) <-
             Except.liftEither
-                (namedSetConstructionDescriptorId
+                (prepareNamedSetConstruction
                     (logicalBuilderFoundation builder)
+                    (candidateProofObjectClosure initial)
+                    identity
                     construction)
-        let descriptor =
-                CheckedSetConstructionExtensionality
-                    identity expectedDescriptor
         when (isNothing (candidateProofCachedValidation initial)) do
-            (expected, preparedDescriptor) <-
-                Except.liftEither
-                    (prepareNamedSetConstruction
-                        (logicalBuilderFoundation builder)
-                        (candidateProofObjectClosure initial)
-                        identity
-                        construction)
             unless
-                ( preparedDescriptor == descriptor
-                  && frozenCoreTerm expected
+                (frozenCoreTerm expected
                         == frozenCoreTerm
                             (checkedPropositionTerm
                                 (candidateCheckedProposition candidate))
diff --git a/source/Checking/Exact.hs b/source/Checking/Exact.hs
index dcfa30f..898bd89 100644
--- a/source/Checking/Exact.hs
+++ b/source/Checking/Exact.hs
@@ -63,6 +63,7 @@ import Checking.Core
 import Checking.Declaration qualified as Declaration
 import Checking.Exact.Vocabulary
 import Checking.Identity
+import Checking.SetConstruction
 import Checking.Semantic
 import Felix.Cache.Codec
 import Felix.Module
@@ -732,6 +733,13 @@ prepareExactSetExpression context expression =
                         (`Map.lookup` elaborationGlobals finalElaboration)
                         (binderTypes context))
                     rawConstruction)
+        traverse_
+            (\checkedConstruction ->
+                unless
+                    (namedSetConstructionTerm checkedConstruction == checked)
+                    (impossible
+                        "exact named construction disagrees with its checked expression"))
+            construction
         pure (PreparedExactSetExpression checked construction)
 
 checkCompiledNamedSetConstruction
@@ -749,7 +757,8 @@ checkCompiledNamedSetConstruction globalType context = \case
                     Nowhere
                     (ExpectedCoreType TySet TyProp)))
             Right
-            (checkedSeparationConstruction checkedBound checkedPredicate)
+            (checkedSeparationConstruction
+                globalType checkedBound checkedPredicate)
     CompiledFunctionalReplacementConstruction domains value condition -> do
         let domainList = NonEmpty.toList domains
             fullContext = replicate (length domainList) TySet <> context
@@ -770,6 +779,7 @@ checkCompiledNamedSetConstruction globalType context = \case
                     (ExpectedCoreType TySet TyProp)))
             Right
             (checkedFunctionalReplacementConstruction
+                globalType
                 (NonEmpty.fromList checkedDomains)
                 checkedValue
                 checkedCondition)
@@ -1275,6 +1285,16 @@ prepareExactDeclaration block entries =
                                         elaborationGlobals finalElaboration)
                                     (replicate (length parameters) TySet))
                                 rawConstruction)
+                    traverse_
+                        (\checkedConstruction ->
+                            unless
+                                (frozenCoreTerm
+                                    (namedSetConstructionClosedBody
+                                        checkedConstruction)
+                                    == canonical)
+                                (impossible
+                                    "exact named construction disagrees with its transparent body"))
+                        construction
                     let requirements =
                             elaborationContextualRequirements finalElaboration
                         body
diff --git a/source/Checking/Exact/Proof.hs b/source/Checking/Exact/Proof.hs
index 18a58a9..23c3dde 100644
--- a/source/Checking/Exact/Proof.hs
+++ b/source/Checking/Exact/Proof.hs
@@ -35,6 +35,7 @@ import Checking.Exact qualified as Exact
 import Checking.Foundation
 import Checking.Identity
 import Checking.Kernel.Derivation (foundationFactDerivation)
+import Checking.SetConstruction
 import Checking.Semantic
 import Felix.Cache.Codec
 import Report.Location
@@ -655,7 +656,7 @@ prepareProof fallback context locals inductionAntecedents goal = \case
                         allocateLocal ExactLocalDefinition context' definition
                     pure (definition :| [], [local])
                 Just construction -> do
-                    characteristics <- prepareConstructionCharacteristics
+                    characteristics <- prepareConstructionFoundation
                     (extensional, equation) <-
                         maybe
                             (impossible
@@ -1023,18 +1024,15 @@ allocateLocal origin context proposition = do
             (Exact.exactBinderContextSupport context)
             proposition)
 
-prepareConstructionCharacteristics
-    :: Prepare
-        (CoreIntrinsicTag -> Maybe (FrozenCheckedCore Void))
-prepareConstructionCharacteristics = do
+prepareConstructionFoundation
+    :: Prepare SetConstructionFoundation
+prepareConstructionFoundation = do
     familyUnion <- foundation FamilyUnionCharacteristic
     separation <- foundation SeparationCharacteristic
     replacement <- foundation ReplacementCharacteristic
-    pure \case
-        FamilyUnion -> Just familyUnion
-        Sep -> Just separation
-        Repl -> Just replacement
-        _ -> Nothing
+    pure
+        (setConstructionFoundation
+            familyUnion separation replacement)
   where
     foundation tag =
         liftDriver
diff --git a/source/Checking/SetConstruction.hs b/source/Checking/SetConstruction.hs
new file mode 100644
index 0000000..47bc9f5
--- /dev/null
+++ b/source/Checking/SetConstruction.hs
@@ -0,0 +1,723 @@
+{-# 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
+    ) 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)
+
+setConstructionFoundation
+    :: FrozenCheckedCore Void
+    -> FrozenCheckedCore Void
+    -> FrozenCheckedCore Void
+    -> SetConstructionFoundation
+setConstructionFoundation =
+    SetConstructionFoundation
+
+checkedFoundationSetConstruction
+    :: CheckedFoundation
+    -> SetConstructionFoundation
+checkedFoundationSetConstruction foundation =
+    SetConstructionFoundation
+        (foundationAxiomFrozen foundation FamilyUnionCharacteristic)
+        (foundationAxiomFrozen foundation SeparationCharacteristic)
+        (foundationAxiomFrozen foundation ReplacementCharacteristic)
+
+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)
+
+-- | 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 <- listToMaybe domainList
+    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)
+
+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
+    term <- checkedDerived construction context TySet
+        (builtConstructionTerm built)
+    membership <- checkedDerived construction (TySet : context) TyProp
+        (builtConstructionMembership built)
+    guard (scopedCoreTerm term == builtConstructionTerm built)
+    guard (scopedCoreTerm membership == 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
+                    (NonEmpty.toList 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]
+    -> [CanonicalTerm global]
+    -> CanonicalTerm global
+    -> Maybe (CanonicalTerm global)
+    -> (CanonicalTerm global, [CheckedCharacteristicApplication global])
+buildFunctionalReplacement context domains value condition =
+    case domains of
+        [] -> impossible "a checked functional replacement has no domain"
+        domain : remaining ->
+            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) =
+    \case
+        FamilyUnion -> Just familyUnion
+        Sep -> Just separation
+        Repl -> Just replacement
+        _ -> Nothing
+
+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
+
+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))