Migrate to `Felix` namespaceHEADhotg

1 files changed, 3936 insertions, 0 deletions

diff --git a/source/Felix/Checking/Exact.hs b/source/Felix/Checking/Exact.hs
new file mode 100644
index 0000000..c829743
--- /dev/null
+++ b/source/Felix/Checking/Exact.hs
@@ -0,0 +1,3936 @@
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | Direct compiler for the first exact monomorphic declaration family.
+module Felix.Checking.Exact
+    ( ExactLocalId
+    , exactLocalId
+    , exactLocalIdValue
+    , ExactBinderContext
+    , emptyExactBinderContext
+    , extendExactBinderContext
+    , extendExactAnonymousBinderContext
+    , exactBinderContextSupport
+    , exactBinderContextIndex
+    , PreparedExactProposition
+    , preparedExactPropositionCore
+    , prepareExactProposition
+    , prepareExactSymbolicBoundConstraints
+    , prepareExactSymbolicWitnessConstraints
+    , prepareExactNounWitnessConstraints
+    , PreparedExactSetExpression
+    , PreparedExactSetConstruction(..)
+    , preparedExactSetExpressionCore
+    , preparedExactSetExpressionConstruction
+    , prepareExactSetExpression
+    , PreparedExactLocalFunctionGraph
+    , preparedExactLocalFunctionGraphCore
+    , preparedExactLocalFunctionGraphDomain
+    , preparedExactLocalFunctionGraphMap
+    , prepareExactLocalFunctionGraph
+    , PreparedExactClaimEnvelope
+    , preparedExactClaimTarget
+    , preparedExactClaimVariables
+    , preparedExactClaimContext
+    , preparedExactClaimAntecedentCount
+    , prepareExactClaimEnvelope
+    , PreparedExactDeclaration
+    , preparedExactLocation
+    , preparedExactGlobalKey
+    , preparedExactObjectId
+    , preparedExactObject
+    , preparedExactSyntaxId
+    , preparedExactIsDefinition
+    , prepareExactDeclaration
+    , lowerPreparedExactBinding
+    , CheckedExactBindingAuthorization
+    , authorizeCheckedExactBinding
+    , PreparedExactStructure
+    , prepareExactStructure
+    , CheckedExactStructureAuthorization
+    , lowerPreparedExactStructure
+    , authorizeCheckedExactStructure
+    , PreparedExactSourceAxiom
+    , prepareExactSourceAxiom
+    , lowerPreparedExactSourceAxiom
+    , authorizeCheckedExactSourceAxiom
+    , ExactCompileError(..)
+    , exactCompileErrorLocation
+    , renderExactCompileError
+    ) where
+
+import Base hiding (Empty)
+import Felix.Cache.Codec
+import Felix.Checking.Core
+import Felix.Checking.Declaration qualified as Declaration
+import Felix.Checking.Exact.Vocabulary
+import Felix.Checking.Identity
+import Felix.Checking.Semantic
+import Felix.Checking.SetConstruction
+import Felix.Module
+import Felix.Report.Location
+import Felix.Syntax.Abstract qualified as Raw
+import Felix.Syntax.Interface (CanonicalLexicalEntry(..))
+import Felix.Syntax.Lexicon qualified as Lexicon
+
+import Control.Monad.Except (ExceptT)
+import Control.Monad.Except (MonadError, throwError)
+import Control.Monad.Except qualified as Except
+import Control.Monad (foldM, unless, when)
+import Control.Monad.State.Strict (StateT)
+import Control.Monad.State.Strict qualified as State
+import Data.ByteString (ByteString)
+import Data.Bifunctor (first)
+import Data.List.NonEmpty qualified as NonEmpty
+import Data.Map.Strict qualified as Map
+import Data.Maybe (catMaybes)
+import Data.Set qualified as Set
+import Data.Text qualified as Text
+import Data.Vector (Vector)
+import Data.Vector qualified as Vector
+import Numeric.Natural (Natural)
+
+
+-- | A disposable identity allocated in source order within one proof.
+newtype ExactLocalId = ExactLocalId Natural
+    deriving stock (Show, Eq, Ord)
+
+exactLocalId :: Natural -> ExactLocalId
+exactLocalId = ExactLocalId
+
+exactLocalIdValue :: ExactLocalId -> Natural
+exactLocalIdValue (ExactLocalId value) = value
+
+data ExactBinder = ExactBinder
+    !ExactLocalId
+    !(Maybe Raw.VarSymbol)
+    !CoreType
+    !(Maybe ExactStructureAnnotation)
+
+data ExactStructureAnnotation = ExactStructureAnnotation
+    !SemanticStructurePhrase
+    !(Maybe ObjectId)
+    !(Map.Map Raw.StructSymbol ObjectId)
+
+-- | The active nearest-first binders of one exact proof scope.
+newtype ExactBinderContext = ExactBinderContext [ExactBinder]
+
+emptyExactBinderContext :: ExactBinderContext
+emptyExactBinderContext = ExactBinderContext []
+
+extendExactBinderContext
+    :: NonEmpty (ExactLocalId, Raw.VarSymbol)
+    -> ExactBinderContext
+    -> Either ExactCompileError ExactBinderContext
+extendExactBinderContext additions (ExactBinderContext initial) =
+    ExactBinderContext <$> foldM add initial (toList additions)
+  where
+    add binders (identity, variable)
+        | any (sameVariable variable) binders =
+            Left (ExactDuplicateLocalBinder (locate variable) variable)
+        | any (sameIdentity identity) binders =
+            Left (ExactDuplicateLocalIdentity (locate variable) identity)
+        | otherwise =
+            Right (ExactBinder identity (Just variable) TySet Nothing : binders)
+
+    sameVariable variable (ExactBinder _identity existing _coreType _structure) =
+        existing == Just variable
+
+    sameIdentity identity (ExactBinder existing _variable _coreType _structure) =
+        existing == identity
+
+-- | Add one proof-owned binder which deliberately has no source-resolvable
+-- spelling.  This is used for a nameless singular witness; it participates in
+-- checked support and de Bruijn weakening but cannot shadow or be looked up by
+-- a later source variable.
+extendExactAnonymousBinderContext
+    :: ExactLocalId
+    -> ExactBinderContext
+    -> Either ExactCompileError ExactBinderContext
+extendExactAnonymousBinderContext identity (ExactBinderContext binders)
+    | any sameIdentity binders =
+        Left (ExactDuplicateLocalIdentity Nowhere identity)
+    | otherwise =
+        Right
+            (ExactBinderContext
+                (ExactBinder identity Nothing TySet Nothing : binders))
+  where
+    sameIdentity (ExactBinder existing _variable _coreType _structure) =
+        existing == identity
+
+exactBinderContextSupport
+    :: ExactBinderContext
+    -> Vector (ExactLocalId, CoreType)
+exactBinderContextSupport (ExactBinderContext binders) =
+    Vector.fromList
+        [ (identity, coreType)
+        | ExactBinder identity _variable coreType _structure <- binders
+        ]
+
+exactBinderContextIndex
+    :: Raw.VarSymbol
+    -> ExactBinderContext
+    -> Maybe Natural
+exactBinderContextIndex variable (ExactBinderContext binders) =
+    go 0 binders
+  where
+    go _index [] =
+        Nothing
+    go index (ExactBinder _identity candidate _coreType _structure : rest)
+        | candidate == Just variable = Just index
+        | otherwise = go (index + 1) rest
+
+newtype PreparedExactProposition = PreparedExactProposition
+    (ScopedCheckedCore ObjectId)
+
+preparedExactPropositionCore
+    :: PreparedExactProposition
+    -> ScopedCheckedCore ObjectId
+preparedExactPropositionCore (PreparedExactProposition proposition) =
+    proposition
+
+data PreparedExactSetExpression = PreparedExactSetExpression
+    !(ScopedCheckedCore ObjectId)
+    !(Maybe PreparedExactSetConstruction)
+
+data PreparedExactSetConstruction
+    = PreparedUnconditionalSetConstruction
+        !(NamedSetConstruction ObjectId)
+    | PreparedRelationalSetConstruction
+        !(CheckedRelationalSetConstruction ObjectId)
+
+preparedExactSetExpressionCore
+    :: PreparedExactSetExpression
+    -> ScopedCheckedCore ObjectId
+preparedExactSetExpressionCore (PreparedExactSetExpression expression _construction) =
+    expression
+
+preparedExactSetExpressionConstruction
+    :: PreparedExactSetExpression
+    -> Maybe PreparedExactSetConstruction
+preparedExactSetExpressionConstruction
+        (PreparedExactSetExpression _expression construction) =
+    construction
+
+-- | A checked replacement graph and the two checked arguments used to
+-- specialize its foundation characteristic. This is transient proof
+-- preparation data, not a declaration or durable object.
+data PreparedExactLocalFunctionGraph = PreparedExactLocalFunctionGraph
+    !(ScopedCheckedCore ObjectId)
+    !(ScopedCheckedCore ObjectId)
+    !(ScopedCheckedCore ObjectId)
+
+preparedExactLocalFunctionGraphCore
+    :: PreparedExactLocalFunctionGraph
+    -> ScopedCheckedCore ObjectId
+preparedExactLocalFunctionGraphCore
+        (PreparedExactLocalFunctionGraph graph _domain _function) =
+    graph
+
+preparedExactLocalFunctionGraphDomain
+    :: PreparedExactLocalFunctionGraph
+    -> ScopedCheckedCore ObjectId
+preparedExactLocalFunctionGraphDomain
+        (PreparedExactLocalFunctionGraph _graph domain _function) =
+    domain
+
+preparedExactLocalFunctionGraphMap
+    :: PreparedExactLocalFunctionGraph
+    -> ScopedCheckedCore ObjectId
+preparedExactLocalFunctionGraphMap
+        (PreparedExactLocalFunctionGraph _graph _domain function) =
+    function
+
+-- | One authoritative closed proposition prepared from a top-level claim
+-- header and conclusion. The remaining fields are transient opening data for
+-- the proof compiler.
+data PreparedExactClaimEnvelope = PreparedExactClaimEnvelope
+    !(ScopedCheckedCore ObjectId)
+    ![Raw.VarSymbol]
+    !ExactBinderContext
+    !Natural
+
+preparedExactClaimTarget
+    :: PreparedExactClaimEnvelope
+    -> ScopedCheckedCore ObjectId
+preparedExactClaimTarget
+        (PreparedExactClaimEnvelope target _variables _context _antecedents) =
+    target
+
+preparedExactClaimVariables
+    :: PreparedExactClaimEnvelope
+    -> [Raw.VarSymbol]
+preparedExactClaimVariables
+        (PreparedExactClaimEnvelope _target variables _context _antecedents) =
+    variables
+
+preparedExactClaimContext
+    :: PreparedExactClaimEnvelope
+    -> ExactBinderContext
+preparedExactClaimContext
+        (PreparedExactClaimEnvelope _target _variables context _antecedents) =
+    context
+
+preparedExactClaimAntecedentCount
+    :: PreparedExactClaimEnvelope
+    -> Natural
+preparedExactClaimAntecedentCount
+        (PreparedExactClaimEnvelope _target _variables _context antecedents) =
+    antecedents
+
+
+data ExactDeclarationFamily
+    = ExactSignature
+    | ExactAbbreviation
+    | ExactDefinition
+    deriving stock (Show, Eq, Ord)
+
+data PreparedExactDeclaration = PreparedExactDeclaration
+    !Location
+    !ExactDeclarationFamily
+    !SemanticGlobalKey
+    !SemanticGlobalTarget
+    !(Maybe AssertedObject)
+    !(Maybe SemanticName)
+    !(Maybe PreparedExactSetConstruction)
+    !DeclarationSyntaxId
+
+preparedExactLocation :: PreparedExactDeclaration -> Location
+preparedExactLocation
+        (PreparedExactDeclaration location _family _key _target _object _alias _construction _syntax) =
+    location
+
+preparedExactGlobalKey :: PreparedExactDeclaration -> SemanticGlobalKey
+preparedExactGlobalKey
+        (PreparedExactDeclaration _location _family key _target _object _alias _construction _syntax) =
+    key
+
+preparedExactObjectId :: PreparedExactDeclaration -> ObjectId
+preparedExactObjectId
+        (PreparedExactDeclaration _location _family _key target _object _alias _construction _syntax) =
+    semanticGlobalTargetObject target
+
+preparedExactObject
+    :: PreparedExactDeclaration
+    -> Maybe AssertedObject
+preparedExactObject
+        (PreparedExactDeclaration _location _family _key _target object _alias _construction _syntax) =
+    object
+
+preparedExactSyntaxId
+    :: PreparedExactDeclaration
+    -> DeclarationSyntaxId
+preparedExactSyntaxId
+        (PreparedExactDeclaration _location _family _key _target _object _alias _construction syntax) =
+    syntax
+
+preparedExactIsDefinition :: PreparedExactDeclaration -> Bool
+preparedExactIsDefinition
+        (PreparedExactDeclaration _location family _key _target _object _alias _construction _syntax) =
+    family == ExactDefinition
+
+preparedExactGlobalTarget
+    :: PreparedExactDeclaration
+    -> SemanticGlobalTarget
+preparedExactGlobalTarget
+        (PreparedExactDeclaration
+            _location _family _key target _object _alias _construction _syntax) =
+    target
+
+preparedDefinitionAlias
+    :: PreparedExactDeclaration
+    -> Maybe SemanticName
+preparedDefinitionAlias
+        (PreparedExactDeclaration
+            _location _family _key _target _object alias _construction _syntax) =
+    alias
+
+preparedDefinitionConstruction
+    :: PreparedExactDeclaration
+    -> Maybe PreparedExactSetConstruction
+preparedDefinitionConstruction
+        (PreparedExactDeclaration
+            _location _family _key _target _object _alias construction _syntax) =
+    construction
+
+data PreparedExactSourceAxiom = PreparedExactSourceAxiom
+    !Location
+    !SemanticName
+    !(ScopedCheckedCore ObjectId)
+    !DeclarationSyntaxId
+
+data PreparedExactStructureFact = PreparedExactStructureFact
+    !Location
+    !(FrozenCheckedCore ObjectId)
+    !SemanticName
+
+data PreparedExactStructure = PreparedExactStructure
+    !Location
+    ![AssertedObject]
+    !ObjectId
+    !SemanticStructureDescriptor
+    !SemanticName
+    ![PreparedExactStructureFact]
+    !DeclarationSyntaxId
+
+data CheckedExactStructureAuthorization =
+    CheckedExactStructureAuthorization
+        !ObjectId
+        ![(Location, Declaration.PreparedVampireObligation Void ())]
+
+data ExactCompileError
+    = ExactUnsupportedDeclaration !Location
+    | ExactUnsupportedDeclarationBody !Location
+    | ExactNonCanonicalSetDefinitionAnnotation !Location
+    | ExactGuardedTransparentDefinition !Location
+    | ExactGuardedOpaqueSignature !Location
+    | ExactDefinitionCombinedSymbolicAlias !Location
+    | ExactRelationalReplacementRequiresNamedDefinition !Location
+    | ExactDeclarationOccurrenceMissing !Location
+    | ExactDeclarationOccurrenceAmbiguous !Location
+    | ExactDeclarationHeadMismatch !Location
+    | ExactFixedSemanticCollision !Location !SemanticGlobalKey
+    | ExactGlobalAlreadyVisible !Location !SemanticGlobalKey
+    | ExactGlobalNotVisible !Location !SemanticGlobalKey
+    | ExactDuplicateParameter !Location !Raw.VarSymbol
+    | ExactDuplicateLocalBinder !Location !Raw.VarSymbol
+    | ExactDuplicateLocalIdentity !Location !ExactLocalId
+    | ExactFreeVariable !Location !Raw.VarSymbol
+    | ExactApplicationExpectedFunction !Location !CoreType
+    | ExactApplicationArgumentMismatch
+        !Location !CoreType !CoreType
+    | ExactExpressionExpectedSet !Location !CoreType
+    | ExactFormulaExpectedProposition !Location !CoreType
+    | ExactCoreCheckFailed !Location !CoreCheckError
+    | ExactObjectTypeMismatch !Location !CoreType !CoreType
+    | ExactUnsupportedHeaderAssumption !Location
+    | ExactQuantifiedTermRequiresPropositionContext !Location
+    | ExactStructureNotVisible !Location !SemanticStructurePhrase
+    | ExactBaseStructureNotAssertable !Location !SemanticStructurePhrase
+    | ExactDuplicateStructureAnnotation !Location !Raw.VarSymbol
+    | ExactStructureOperationNotAvailable !Location !Raw.StructSymbol
+    | ExactStructureOperationAmbiguous
+        !Location !Raw.StructSymbol ![ObjectId]
+    | ExactContextualExpansionNotAvailable
+        !Location !SemanticGlobalKey
+    | ExactContextualRequirementConflict
+        !Location !Raw.StructSymbol !ObjectId !ObjectId
+    | ExactStructureOccurrenceMismatch !Location
+    | ExactStructureSelfParent !Location !SemanticStructurePhrase
+    | ExactStructureDuplicateParent !Location !SemanticStructurePhrase
+    | ExactStructureAlreadyVisible !Location !SemanticStructurePhrase
+    | ExactStructureDuplicateOperation !Location !Raw.StructSymbol
+    | ExactStructureOperationAlreadyInherited !Location !Raw.StructSymbol
+    | ExactStructureOperationConflict
+        !Location !Raw.StructSymbol
+        !SemanticStructurePhrase !SemanticStructurePhrase
+    | ExactStructureHasNoCarrier !Location !SemanticStructurePhrase
+    | ExactStructureDescriptorInvalid !Location !SemanticEnvironmentError
+    | ExactStructureObjectNotVisible !Location !ObjectId
+    deriving stock (Show, Eq)
+
+exactCompileErrorLocation :: ExactCompileError -> Location
+exactCompileErrorLocation = \case
+    ExactUnsupportedDeclaration location -> location
+    ExactUnsupportedDeclarationBody location -> location
+    ExactNonCanonicalSetDefinitionAnnotation location -> location
+    ExactGuardedTransparentDefinition location -> location
+    ExactGuardedOpaqueSignature location -> location
+    ExactDefinitionCombinedSymbolicAlias location -> location
+    ExactRelationalReplacementRequiresNamedDefinition location -> location
+    ExactDeclarationOccurrenceMissing location -> location
+    ExactDeclarationOccurrenceAmbiguous location -> location
+    ExactDeclarationHeadMismatch location -> location
+    ExactFixedSemanticCollision location _key -> location
+    ExactGlobalAlreadyVisible location _key -> location
+    ExactGlobalNotVisible location _key -> location
+    ExactDuplicateParameter location _parameter -> location
+    ExactDuplicateLocalBinder location _variable -> location
+    ExactDuplicateLocalIdentity location _identity -> location
+    ExactFreeVariable location _variable -> location
+    ExactApplicationExpectedFunction location _actual -> location
+    ExactApplicationArgumentMismatch location _expected _actual -> location
+    ExactExpressionExpectedSet location _actual -> location
+    ExactFormulaExpectedProposition location _actual -> location
+    ExactCoreCheckFailed location _failure -> location
+    ExactObjectTypeMismatch location _expected _actual -> location
+    ExactUnsupportedHeaderAssumption location -> location
+    ExactQuantifiedTermRequiresPropositionContext location -> location
+    ExactStructureNotVisible location _phrase -> location
+    ExactBaseStructureNotAssertable location _phrase -> location
+    ExactDuplicateStructureAnnotation location _variable -> location
+    ExactStructureOperationNotAvailable location _symbol -> location
+    ExactStructureOperationAmbiguous location _symbol _objects -> location
+    ExactContextualExpansionNotAvailable location _key -> location
+    ExactContextualRequirementConflict location _symbol _first _second -> location
+    ExactStructureOccurrenceMismatch location -> location
+    ExactStructureSelfParent location _phrase -> location
+    ExactStructureDuplicateParent location _phrase -> location
+    ExactStructureAlreadyVisible location _phrase -> location
+    ExactStructureDuplicateOperation location _symbol -> location
+    ExactStructureOperationAlreadyInherited location _symbol -> location
+    ExactStructureOperationConflict location _symbol _first _second -> location
+    ExactStructureHasNoCarrier location _phrase -> location
+    ExactStructureDescriptorInvalid location _failure -> location
+    ExactStructureObjectNotVisible location _object -> location
+
+renderExactCompileError :: ExactCompileError -> Text
+renderExactCompileError = \case
+    ExactUnsupportedDeclaration location ->
+        at location <> "this declaration is not yet supported by the typed checker"
+    ExactUnsupportedDeclarationBody location ->
+        at location <> "this source form is not yet supported by exact elaboration"
+    ExactNonCanonicalSetDefinitionAnnotation location ->
+        at location
+            <> "only the unmodified built-in noun `set` is a harmless definition annotation; "
+            <> "state a total condition in the definiens, or, where a corresponding opaque signature form exists, use it with a following explicit axiom; otherwise migrate the spelling or leave it unsupported"
+    ExactGuardedTransparentDefinition location ->
+        at location
+            <> "a transparent definition cannot have a header assumption; "
+            <> "state a total condition in the definiens, or, where a corresponding opaque signature form exists, use it with a following explicit axiom; otherwise migrate the spelling or leave it unsupported"
+    ExactGuardedOpaqueSignature location ->
+        at location
+            <> "an opaque signature cannot have a header assumption; "
+            <> "state the condition in a following explicit axiom"
+    ExactDefinitionCombinedSymbolicAlias location ->
+        at location
+            <> "a functional definition cannot declare a symbolic equivalent at the same time; "
+            <> "define the symbolic operator first, then define the functional phrase as an abbreviation applying it"
+    ExactRelationalReplacementRequiresNamedDefinition location ->
+        at location
+            <> "relational replacement is supported only as the outer body of a named definition"
+    ExactDeclarationOccurrenceMissing location ->
+        at location <> "the declaration has no associated syntax occurrence"
+    ExactDeclarationOccurrenceAmbiguous location ->
+        at location <> "the declaration has more than one semantic head"
+    ExactDeclarationHeadMismatch location ->
+        at location <> "the parsed declaration head does not match its syntax occurrence"
+    ExactFixedSemanticCollision location key ->
+        at location <> "the declaration collides with fixed semantics for "
+            <> shown key
+    ExactGlobalAlreadyVisible location key ->
+        at location <> "the global " <> shown key <> " is already declared"
+    ExactGlobalNotVisible location key ->
+        at location <> "the global " <> shown key <> " is not visible"
+    ExactDuplicateParameter location parameter ->
+        at location <> "the declaration parameter " <> shown parameter <> " is repeated"
+    ExactDuplicateLocalBinder location variable ->
+        at location <> "the proof binder " <> shown variable <> " is already active"
+    ExactDuplicateLocalIdentity location identity ->
+        at location <> "the proof-local identity " <> shown identity <> " is already active"
+    ExactFreeVariable location variable ->
+        at location <> "the exact source form contains the free variable " <> shown variable
+    ExactApplicationExpectedFunction location actual ->
+        at location <> "an application expected a function, but found " <> shown actual
+    ExactApplicationArgumentMismatch location expected actual ->
+        at location <> "an application expected " <> shown expected
+            <> ", but found " <> shown actual
+    ExactExpressionExpectedSet location actual ->
+        at location <> "an expression has type " <> shown actual <> " instead of Set"
+    ExactFormulaExpectedProposition location actual ->
+        at location <> "a formula has type " <> shown actual <> " instead of Prop"
+    ExactCoreCheckFailed location failure ->
+        at location <> "the checked declaration core is invalid: " <> shown failure
+    ExactObjectTypeMismatch location expected actual ->
+        at location <> "the declaration object has type " <> shown actual
+            <> " instead of " <> shown expected
+    ExactUnsupportedHeaderAssumption location ->
+        at location <> "this top-level header assumption is not yet supported by exact elaboration"
+    ExactQuantifiedTermRequiresPropositionContext location ->
+        at location
+            <> "a quantified term requires a containing proposition"
+    ExactStructureNotVisible location structurePhrase ->
+        at location <> "the structure " <> shown structurePhrase <> " is not visible"
+    ExactBaseStructureNotAssertable location structurePhrase ->
+        at location <> "the metadata-only structure " <> shown structurePhrase
+            <> " cannot be asserted"
+    ExactDuplicateStructureAnnotation location variable ->
+        at location <> "the structure binder " <> shown variable
+            <> " is annotated more than once"
+    ExactStructureOperationNotAvailable location symbol ->
+        at location <> "the structure operation " <> shown symbol
+            <> " is not available in the active structure scope"
+    ExactStructureOperationAmbiguous location symbol objects ->
+        at location <> "the structure operation " <> shown symbol
+            <> " is ambiguous between " <> shown objects
+    ExactContextualExpansionNotAvailable location key ->
+        at location <> "the contextual abbreviation " <> shown key
+            <> " has no compatible active structure"
+    ExactContextualRequirementConflict location symbol firstObject secondObject ->
+        at location <> "the contextual abbreviation requires incompatible "
+            <> shown symbol <> " operations " <> shown firstObject
+            <> " and " <> shown secondObject
+    ExactStructureOccurrenceMismatch location ->
+        at location <> "the structure syntax occurrences do not match the declaration"
+    ExactStructureSelfParent location structurePhrase ->
+        at location <> "the structure " <> shown structurePhrase
+            <> " cannot inherit from itself"
+    ExactStructureDuplicateParent location structurePhrase ->
+        at location <> "the parent structure " <> shown structurePhrase
+            <> " is repeated"
+    ExactStructureAlreadyVisible location structurePhrase ->
+        at location <> "the structure " <> shown structurePhrase
+            <> " is already declared"
+    ExactStructureDuplicateOperation location symbol ->
+        at location <> "the structure operation " <> shown symbol
+            <> " is repeated"
+    ExactStructureOperationAlreadyInherited location symbol ->
+        at location <> "the structure operation " <> shown symbol
+            <> " is already inherited"
+    ExactStructureOperationConflict location symbol firstOrigin secondOrigin ->
+        at location <> "the inherited structure operation " <> shown symbol
+            <> " conflicts between " <> shown firstOrigin
+            <> " and " <> shown secondOrigin
+    ExactStructureHasNoCarrier location structurePhrase ->
+        at location <> "the structure " <> shown structurePhrase
+            <> " does not inherit the base carrier operation"
+    ExactStructureDescriptorInvalid location _failure ->
+        at location <> "the canonical structure descriptor is inconsistent"
+    ExactStructureObjectNotVisible location identity ->
+        at location <> "the structure fact mentions unavailable object "
+            <> shown identity
+  where
+    at location = locationToText location <> ": "
+    shown :: Show value => value -> Text
+    shown = Text.pack . show
+
+data ElaborationState = ElaborationState
+    { elaborationBinders :: !(Map.Map Raw.VarSymbol Natural)
+    -- Counts every active de Bruijn binder, including anonymous and
+    -- contextual binders which have no entry in 'elaborationBinders'.
+    , elaborationBinderDepth :: !Natural
+    , elaborationStructures :: !(Map.Map Natural ExactStructureAnnotation)
+    , elaborationGlobals :: !(Map.Map ObjectId CoreType)
+    , elaborationContextualBinder :: !(Maybe Natural)
+    , elaborationContextualRequirements
+        :: !(Map.Map Raw.StructSymbol ObjectId)
+    }
+
+type Elaborate =
+    StateT
+        ElaborationState
+        (ExceptT ExactCompileError (Declaration.LoweringDriver))
+
+data PreparedHead = PreparedHead
+    !SemanticGlobalKey
+    ![Raw.VarSymbol]
+    !CoreType
+
+data PreparedBody
+    = OpaqueBody
+    | TransparentBody
+        !(CanonicalTerm ObjectId)
+        !(Maybe PreparedExactSetConstruction)
+    | ContextualTransparentBody
+        !(Map.Map Raw.StructSymbol ObjectId)
+        !(CanonicalTerm ObjectId)
+
+data CompiledBody = CompiledBody
+    !(CanonicalTerm ObjectId)
+    !(Maybe CompiledNamedSetConstruction)
+
+data CompiledNamedSetConstruction
+    = CompiledSeparationConstruction
+        !(CanonicalTerm ObjectId)
+        !(CanonicalTerm ObjectId)
+    | CompiledFunctionalReplacementConstruction
+        !(NonEmpty (CanonicalTerm ObjectId))
+        !(CanonicalTerm ObjectId)
+        !(Maybe (CanonicalTerm ObjectId))
+    | CompiledRelationalReplacementConstruction
+        !(CanonicalTerm ObjectId)
+        !(CanonicalTerm ObjectId)
+
+prepareExactProposition
+    :: ExactBinderContext
+    -> Raw.Stmt
+    -> Declaration.LoweringDriver
+        (Either ExactCompileError PreparedExactProposition)
+prepareExactProposition context statement =
+    prepareExactPropositionTerm
+        context
+        (locate statement)
+        (compileStatement statement)
+
+-- | Compile the source bound of already-opened symbolic binders.  This is the
+-- shared checked constraint seam used by quantified statements and proof
+-- binders, so relation signs, carrier casts, and global occurrences are
+-- elaborated exactly once by the ordinary expression compiler.
+prepareExactSymbolicBoundConstraints
+    :: ExactBinderContext
+    -> NonEmpty Raw.VarSymbol
+    -> Raw.Bound
+    -> Declaration.LoweringDriver
+        (Either ExactCompileError PreparedExactProposition)
+prepareExactSymbolicBoundConstraints context variables bound =
+    prepareExactPropositionTerm
+        context
+        (case bound of
+            Raw.Unbounded -> locate (NonEmpty.head variables)
+            _ -> locate bound)
+        (logicalConjunction
+            <$> compileSymbolicBoundConstraintList variables bound)
+
+-- | Compile the opened body used by a symbolic existential witness.  Its
+-- grouping is deliberately identical to 'SymbolicExists': all bound
+-- constraints form the existential restriction and the stated proposition is
+-- its body.
+prepareExactSymbolicWitnessConstraints
+    :: ExactBinderContext
+    -> NonEmpty Raw.VarSymbol
+    -> Raw.Bound
+    -> Raw.Stmt
+    -> Declaration.LoweringDriver
+        (Either ExactCompileError PreparedExactProposition)
+prepareExactSymbolicWitnessConstraints context variables bound statement =
+    prepareExactPropositionTerm context (locate statement) do
+        constraints <-
+            logicalConjunction
+                <$> compileSymbolicBoundConstraintList variables bound
+        body <- compileStatement statement
+        pure
+            (if constraints == logicalTruth
+                then body
+                else logicalAnd constraints body)
+
+-- | Compile the checked constraint of an already-opened noun witness.  Named
+-- binders are resolved normally; a nameless singular noun uses the nearest
+-- anonymous binder and therefore introduces no lookup spelling.
+prepareExactNounWitnessConstraints
+    :: ExactBinderContext
+    -> Raw.NounPhrase []
+    -> Declaration.LoweringDriver
+        (Either ExactCompileError PreparedExactProposition)
+prepareExactNounWitnessConstraints context nounPhrase =
+    case nounPhrase of
+        Raw.NounPhrase left noun variables right suchThat ->
+            prepareExactPropositionTerm context (locate noun) do
+                subjects <-
+                    case NonEmpty.nonEmpty variables of
+                        Just binders ->
+                            toList
+                                <$> traverse compileIntroducedVariable binders
+                        Nothing ->
+                            pure [CBound 0]
+                compileNounPhraseConstraints
+                    subjects left noun right suchThat
+
+prepareExactPropositionTerm
+    :: ExactBinderContext
+    -> Location
+    -> Elaborate (CanonicalTerm ObjectId)
+    -> Declaration.LoweringDriver
+        (Either ExactCompileError PreparedExactProposition)
+prepareExactPropositionTerm context location compile =
+    Except.runExceptT do
+        let initialElaboration = initialElaborationState context
+        (term, finalElaboration) <-
+            State.runStateT compile initialElaboration
+        checked <-
+            either
+                (Except.throwError . ExactCoreCheckFailed location)
+                pure
+                (checkScopedCanonicalCore
+                    (`Map.lookup` elaborationGlobals finalElaboration)
+                    (binderTypes context)
+                    term)
+        unless (scopedCoreType checked == TyProp)
+            (Except.throwError
+                (ExactFormulaExpectedProposition
+                    location
+                    (scopedCoreType checked)))
+        pure (PreparedExactProposition checked)
+
+prepareExactSetExpression
+    :: ExactBinderContext
+    -> Raw.Expr
+    -> Declaration.LoweringDriver
+        (Either ExactCompileError PreparedExactSetExpression)
+prepareExactSetExpression context expression =
+    Except.runExceptT do
+        let initialElaboration = initialElaborationState context
+        (compiled, finalElaboration) <-
+            State.runStateT
+                (compileNamedSetExpression expression)
+                initialElaboration
+        let CompiledBody term rawConstruction = compiled
+        checked <-
+            either
+                (Except.throwError
+                    . ExactCoreCheckFailed (locate expression))
+                pure
+                (checkScopedCanonicalCore
+                    (`Map.lookup` elaborationGlobals finalElaboration)
+                    (binderTypes context)
+                    term)
+        unless (scopedCoreType checked == TySet)
+            (Except.throwError
+                (ExactExpressionExpectedSet
+                    (locate expression)
+                    (scopedCoreType checked)))
+        construction <-
+            Except.liftEither
+                (traverse
+                    (checkCompiledNamedSetConstruction
+                        (`Map.lookup` elaborationGlobals finalElaboration)
+                        (binderTypes context))
+                    rawConstruction)
+        traverse_
+            (\checkedConstruction ->
+                unless
+                    (preparedSetConstructionTerm checkedConstruction == checked)
+                    (impossible
+                        "exact named construction disagrees with its checked expression"))
+            construction
+        pure (PreparedExactSetExpression checked construction)
+
+checkCompiledNamedSetConstruction
+    :: (ObjectId -> Maybe CoreType)
+    -> [CoreType]
+    -> CompiledNamedSetConstruction
+    -> Either ExactCompileError PreparedExactSetConstruction
+checkCompiledNamedSetConstruction globalType context = \case
+    CompiledSeparationConstruction bound predicate -> do
+        checkedBound <- checkAt context TySet bound
+        checkedPredicate <- checkAt (TySet : context) TyProp predicate
+        maybe
+            (Left
+                (ExactCoreCheckFailed
+                    Nowhere
+                    (ExpectedCoreType TySet TyProp)))
+            (Right . PreparedUnconditionalSetConstruction)
+            (checkedSeparationConstruction
+                globalType checkedBound checkedPredicate)
+    CompiledFunctionalReplacementConstruction domains value condition -> do
+        let domainList = NonEmpty.toList domains
+            fullContext = replicate (length domainList) TySet <> context
+        checkedDomains <-
+            traverse
+                (\(depth, domain) ->
+                    checkAt
+                        (replicate depth TySet <> context)
+                        TySet
+                        domain)
+                (zip [0..] domainList)
+        checkedValue <- checkAt fullContext TySet value
+        checkedCondition <- traverse (checkAt fullContext TyProp) condition
+        maybe
+            (Left
+                (ExactCoreCheckFailed
+                    Nowhere
+                    (ExpectedCoreType TySet TyProp)))
+            (Right . PreparedUnconditionalSetConstruction)
+            (checkedFunctionalReplacementConstruction
+                globalType
+                (NonEmpty.fromList checkedDomains)
+                checkedValue
+                checkedCondition)
+    CompiledRelationalReplacementConstruction domain relation -> do
+        checkedDomain <- checkAt context TySet domain
+        checkedRelation <- checkAt (TySet : TySet : context) TyProp relation
+        maybe
+            (Left
+                (ExactCoreCheckFailed
+                    Nowhere
+                    (ExpectedCoreType TySet TyProp)))
+            (Right . PreparedRelationalSetConstruction)
+            (checkedRelationalReplacementConstruction
+                globalType checkedDomain checkedRelation)
+  where
+    checkAt expectedContext expectedType term = do
+        checked <-
+            first
+                (ExactCoreCheckFailed Nowhere)
+                (checkScopedCanonicalCore globalType expectedContext term)
+        unless
+            (scopedCoreType checked == expectedType)
+            (Left
+                (ExactCoreCheckFailed
+                    Nowhere
+                    (ExpectedCoreType
+                        expectedType
+                        (scopedCoreType checked))))
+        pure checked
+
+preparedSetConstructionTerm
+    :: PreparedExactSetConstruction
+    -> ScopedCheckedCore ObjectId
+preparedSetConstructionTerm = \case
+    PreparedUnconditionalSetConstruction construction ->
+        namedSetConstructionTerm construction
+    PreparedRelationalSetConstruction construction ->
+        relationalSetConstructionTerm construction
+
+preparedSetConstructionClosedBody
+    :: PreparedExactSetConstruction
+    -> FrozenCheckedCore ObjectId
+preparedSetConstructionClosedBody = \case
+    PreparedUnconditionalSetConstruction construction ->
+        namedSetConstructionClosedBody construction
+    PreparedRelationalSetConstruction construction ->
+        relationalSetConstructionClosedBody construction
+
+prepareExactLocalFunctionGraph
+    :: Location
+    -> ExactBinderContext
+    -> ExactBinderContext
+    -> Raw.Expr
+    -> Raw.Expr
+    -> Declaration.LoweringDriver
+        (Either ExactCompileError PreparedExactLocalFunctionGraph)
+prepareExactLocalFunctionGraph
+        location context argumentContext domainExpression valueExpression =
+    Except.runExceptT do
+        domain <-
+            preparedExactSetExpressionCore
+                <$> ( Except.lift
+                        (prepareExactSetExpression context domainExpression)
+                        >>= Except.liftEither
+                    )
+        value <-
+            preparedExactSetExpressionCore
+                <$> ( Except.lift
+                        (prepareExactSetExpression
+                            argumentContext valueExpression)
+                        >>= Except.liftEither
+                    )
+        pair <- prepareOrderedPair
+        case scopedReplacementGraph pair domain value of
+            Just (graph, checkedDomain, function) ->
+                pure
+                    (PreparedExactLocalFunctionGraph
+                        graph checkedDomain function)
+            Nothing ->
+                impossible
+                    "checked local-function components did not form a replacement graph"
+  where
+    prepareOrderedPair = do
+        let initialElaboration = initialElaborationState context
+            key =
+                SemanticExpressionFunction
+                    (Raw.mixfixPattern Raw.PairSymbol)
+            expected = TySet `TyArrow` (TySet `TyArrow` TySet)
+        ((term, actual), finalElaboration) <-
+            State.runStateT
+                (applyResolvedTyped location key [])
+                initialElaboration
+        unless (actual == expected)
+            (Except.throwError
+                (ExactObjectTypeMismatch location expected actual))
+        either
+            (Except.throwError . ExactCoreCheckFailed location)
+            pure
+            (checkScopedCanonicalCore
+                (`Map.lookup` elaborationGlobals finalElaboration)
+                (binderTypes context)
+                term)
+
+prepareExactClaimEnvelope
+    :: [Raw.Asm]
+    -> Raw.Stmt
+    -> Declaration.LoweringDriver
+        (Either ExactCompileError PreparedExactClaimEnvelope)
+prepareExactClaimEnvelope assumptions statement =
+    discover [] emptyExactBinderContext
+  where
+    discover variables context = do
+        attempted <- prepareExactClaimAttempt context assumptions statement
+        case attempted of
+            Left (ExactFreeVariable _location variable)
+                | variable `elem` variables ->
+                    impossible
+                        "exact claim discovery repeated an active free variable"
+                | otherwise ->
+                    case extendExactBinderContext
+                            ( ( exactLocalId
+                                    (fromIntegral (length variables))
+                              , variable
+                              ) :| []
+                            )
+                            context of
+                        Left failure ->
+                            pure (Left failure)
+                        Right extended ->
+                            discover (variables <> [variable]) extended
+            Left failure ->
+                pure (Left failure)
+            Right (target, antecedentCount, structures) ->
+                pure
+                    (Right
+                        (PreparedExactClaimEnvelope
+                            target
+                            variables
+                            (annotateBinderContext structures context)
+                            antecedentCount))
+
+prepareExactClaimAttempt
+    :: ExactBinderContext
+    -> [Raw.Asm]
+    -> Raw.Stmt
+    -> Declaration.LoweringDriver
+        (Either
+            ExactCompileError
+            ( ScopedCheckedCore ObjectId
+            , Natural
+            , Map.Map Natural ExactStructureAnnotation
+            ))
+prepareExactClaimAttempt context assumptions statement =
+    Except.runExceptT do
+        let initialElaboration = initialElaborationState context
+        ((antecedents, conclusion), finalElaboration) <-
+            State.runStateT
+                ( do
+                    antecedents <-
+                        concat <$> traverse compileHeaderAssumption assumptions
+                    conclusion <- compileStatement statement
+                    pure (antecedents, conclusion)
+                )
+                initialElaboration
+        checkedAntecedents <-
+            traverse
+                (uncurry
+                    (checkEnvelopeProposition
+                        finalElaboration
+                        context))
+                antecedents
+        checkedConclusion <-
+            checkEnvelopeProposition
+                finalElaboration
+                context
+                (locate statement)
+                conclusion
+        let implication =
+                foldr
+                    (\antecedent continuation ->
+                        fromMaybe
+                            (impossible
+                                "checked claim antecedents have unequal contexts")
+                            (implyScopedCore antecedent continuation))
+                    checkedConclusion
+                    checkedAntecedents
+            closed = closeClaimBinders implication
+        unless (null (scopedCoreContext closed))
+            (impossible "exact claim closure retained a binder")
+        pure
+            ( closed
+            , fromIntegral (length antecedents)
+            , elaborationStructures finalElaboration
+            )
+
+checkEnvelopeProposition
+    :: ElaborationState
+    -> ExactBinderContext
+    -> Location
+    -> CanonicalTerm ObjectId
+    -> ExceptT
+        ExactCompileError
+        (Declaration.LoweringDriver)
+        (ScopedCheckedCore ObjectId)
+checkEnvelopeProposition elaboration context location term = do
+    checked <-
+        either
+            (Except.throwError . ExactCoreCheckFailed location)
+            pure
+            (checkScopedCanonicalCore
+                (`Map.lookup` elaborationGlobals elaboration)
+                (binderTypes context)
+                term)
+    unless (scopedCoreType checked == TyProp)
+        (Except.throwError
+            (ExactFormulaExpectedProposition
+                location
+                (scopedCoreType checked)))
+    pure checked
+
+closeClaimBinders
+    :: ScopedCheckedCore global
+    -> ScopedCheckedCore global
+closeClaimBinders scoped =
+    case scopedCoreContext scoped of
+        [] -> scoped
+        _binder : _remaining ->
+            closeClaimBinders
+                (fromMaybe
+                    (impossible
+                        "a checked claim binder could not be closed")
+                    (closeScopedForall scoped))
+
+binderIndices :: ExactBinderContext -> Map.Map Raw.VarSymbol Natural
+binderIndices (ExactBinderContext binders) =
+    Map.fromList
+        [ (variable, fromIntegral index)
+        | (index, ExactBinder _identity (Just variable) _coreType _structure) <-
+            zip [0 :: Int ..] binders
+        ]
+
+binderStructures
+    :: ExactBinderContext
+    -> Map.Map Natural ExactStructureAnnotation
+binderStructures (ExactBinderContext binders) =
+    Map.fromList
+        [ (fromIntegral index, structure)
+        | (index, ExactBinder _identity _variable _coreType (Just structure)) <-
+            zip [0 :: Int ..] binders
+        ]
+
+binderTypes :: ExactBinderContext -> [CoreType]
+binderTypes (ExactBinderContext binders) =
+    [ coreType
+    | ExactBinder _identity _variable coreType _structure <- binders
+    ]
+
+initialElaborationState :: ExactBinderContext -> ElaborationState
+initialElaborationState context =
+    ElaborationState
+        { elaborationBinders = binderIndices context
+        , elaborationBinderDepth =
+            fromIntegral (length (binderTypes context))
+        , elaborationStructures = binderStructures context
+        , elaborationGlobals = mempty
+        , elaborationContextualBinder = Nothing
+        , elaborationContextualRequirements = mempty
+        }
+
+annotateBinderContext
+    :: Map.Map Natural ExactStructureAnnotation
+    -> ExactBinderContext
+    -> ExactBinderContext
+annotateBinderContext structures (ExactBinderContext binders) =
+    ExactBinderContext
+        [ ExactBinder identity variable coreType
+            (Map.lookup (fromIntegral index) structures)
+        | (index, ExactBinder identity variable coreType _old) <-
+            zip [0 :: Int ..] binders
+        ]
+
+compileHeaderAssumption
+    :: Raw.Asm
+    -> Elaborate [(Location, CanonicalTerm ObjectId)]
+compileHeaderAssumption = \case
+    Raw.AsmSuppose statement -> do
+        proposition <- compileStatement statement
+        pure [(locate statement, proposition)]
+    Raw.AsmLetNoun variables nounPhrase
+        | exactSetNounPhrase nounPhrase -> do
+            traverse_ compileIntroducedVariable variables
+            pure []
+        | otherwise -> do
+            subjects <- traverse compileIntroducedVariable variables
+            constraints <-
+                traverse (`compileNounPhraseMaybe` nounPhrase) subjects
+            pure
+                [ (locate variable, constraint)
+                | (variable, constraint) <-
+                    zip (toList variables) (toList constraints)
+                ]
+    Raw.AsmLetIn variables domain -> do
+        variableTerms <- traverse compileIntroducedVariable variables
+        domainTerm <- compileExpressionAsSet domain
+        traverse
+            (\(variable, variableTerm) -> do
+                proposition <-
+                    compileMembership
+                        (locate domain)
+                        Raw.Positive
+                        variableTerm
+                        domainTerm
+                pure (locate variable, proposition))
+            (zip (toList variables) (toList variableTerms))
+    Raw.AsmLetEq variable expression -> do
+        variableTerm <- compileIntroducedVariable variable
+        expressionTerm <- compileExpressionAsSet expression
+        pure
+            [ ( locate variable
+              , CEq TySet variableTerm expressionTerm
+              )
+            ]
+    Raw.AsmLetThe variable _function ->
+        Except.throwError
+            (ExactUnsupportedHeaderAssumption (locate variable))
+    Raw.AsmLetStruct variable structure -> do
+        subject <- compileIntroducedVariable variable
+        annotation <-
+            resolveStructureAnnotation
+                (locate variable)
+                structure
+        index <-
+            maybe
+                (impossible "an introduced structure variable is unbound")
+                pure
+                =<< Map.lookup variable <$> State.gets elaborationBinders
+        existing <- State.gets (Map.lookup index . elaborationStructures)
+        when
+            (isJust existing)
+            (Except.throwError
+                (ExactDuplicateStructureAnnotation
+                    (locate variable) variable))
+        State.modify' \state ->
+            state
+                { elaborationStructures =
+                    Map.insert index annotation
+                        (elaborationStructures state)
+                }
+        predicate <-
+            maybe
+                (impossible "an assertable structure has no predicate")
+                pure
+                (structureAnnotationPredicate annotation)
+        recordExactGlobal
+            predicate
+            (TyArrow TySet TyProp)
+        pure
+            [ ( locate variable
+              , CApp
+                    (CGlobal predicate)
+                    subject
+              )
+            ]
+
+compileIntroducedVariable
+    :: Raw.VarSymbol
+    -> Elaborate (CanonicalTerm ObjectId)
+compileIntroducedVariable variable =
+    compileExpressionAsSet (Raw.ExprVar variable)
+
+resolveStructureAnnotation
+    :: Location
+    -> Raw.StructPhrase
+    -> Elaborate ExactStructureAnnotation
+resolveStructureAnnotation location rawPhrase = do
+    let structurePhrase = semanticStructurePhrase rawPhrase
+    resolved <-
+        State.lift
+            (Except.lift
+                (Declaration.resolveVisibleStructureLowering structurePhrase))
+    structure <-
+        maybe
+            (Except.throwError
+                (ExactStructureNotVisible location structurePhrase))
+            pure
+            resolved
+    predicate <-
+        maybe
+            (Except.throwError
+                (ExactBaseStructureNotAssertable location structurePhrase))
+            pure
+            (Declaration.resolvedStructurePredicate structure)
+    pure
+        (ExactStructureAnnotation
+            structurePhrase
+            (Just predicate)
+            (Declaration.resolvedStructureOperations structure))
+
+structureAnnotationPredicate :: ExactStructureAnnotation -> Maybe ObjectId
+structureAnnotationPredicate
+        (ExactStructureAnnotation _ predicate _operations) =
+    predicate
+
+structureAnnotationOperation
+    :: Raw.StructSymbol
+    -> ExactStructureAnnotation
+    -> Maybe ObjectId
+structureAnnotationOperation symbol
+        (ExactStructureAnnotation _phrase _predicate operations) =
+    Map.lookup symbol operations
+
+recordExactGlobal :: ObjectId -> CoreType -> Elaborate ()
+recordExactGlobal identity coreType = do
+    existing <- State.gets (Map.lookup identity . elaborationGlobals)
+    case existing of
+        Nothing ->
+            State.modify' \state ->
+                state
+                    { elaborationGlobals =
+                        Map.insert identity coreType
+                            (elaborationGlobals state)
+                    }
+        Just actual
+            | actual == coreType -> pure ()
+            | otherwise ->
+                impossible "one exact global acquired two checked types"
+
+prepareExactSourceAxiom
+    :: Raw.Block
+    -> Declaration.LoweringDriver
+        (Either ExactCompileError PreparedExactSourceAxiom)
+prepareExactSourceAxiom = \case
+    Raw.BlockAxiom
+            location _title (Raw.Marker marker)
+            (Raw.Axiom assumptions statement) -> do
+            prepared <- prepareExactClaimEnvelope assumptions statement
+            pure do
+                envelope <- prepared
+                let core = preparedExactClaimTarget envelope
+                    alias = semanticName marker
+                unless (null (scopedCoreContext core))
+                    (Left (ExactUnsupportedDeclarationBody location))
+                pure
+                    (PreparedExactSourceAxiom
+                        location
+                        alias
+                        core
+                        (declarationSyntaxId
+                            (encodePreparedSourceAxiom core alias)))
+    block ->
+        pure (Left (ExactUnsupportedDeclaration (locate block)))
+
+lowerPreparedExactSourceAxiom
+    :: PreparedExactSourceAxiom
+    -> Declaration.LoweringDriver
+        (Either
+            Declaration.DeclarationError
+            (Declaration.CheckedDeclaration ()))
+lowerPreparedExactSourceAxiom
+        (PreparedExactSourceAxiom _location alias target syntax) =
+    fmap
+        (\spec ->
+            Declaration.checkedCompiledDeclaration
+                syntax [] [] [] []
+                [ Declaration.checkedCandidate
+                    spec
+                    Declaration.checkedSourceAxiomPlanning
+                    :| []
+                ]
+                ())
+        <$> Declaration.prepareCandidateSpecLowering
+            [] target SearchEligible [alias]
+
+authorizeCheckedExactSourceAxiom
+    :: ()
+    -> [NonEmpty Declaration.ReservedCandidate]
+    -> Declaration.Declaration ()
+authorizeCheckedExactSourceAxiom () = \case
+    [candidate :| []] ->
+        Declaration.authorizeSourceAxiomCandidate candidate
+    stages ->
+        Declaration.failDeclaration
+            (Declaration.CheckedAuthorizationCandidateShapeMismatch
+                1 (length stages))
+
+prepareExactDeclaration
+    :: Raw.Block
+    -> [CanonicalLexicalEntry]
+    -> Declaration.LoweringDriver
+        (Either ExactCompileError PreparedExactDeclaration)
+prepareExactDeclaration block entries =
+    Except.runExceptT do
+        entry <-
+            case entries of
+                [] -> Except.throwError
+                    (ExactDeclarationOccurrenceMissing (locate block))
+                [single] -> pure single
+                _ -> Except.throwError
+                    (ExactDeclarationOccurrenceAmbiguous (locate block))
+        key <-
+            maybe
+                (Except.throwError
+                    (ExactUnsupportedDeclaration (locate block)))
+                pure
+                (semanticGlobalKeyFromLexicalEntry entry)
+        when
+            (isJust (fixedSemanticMeaning key))
+            (Except.throwError
+                (ExactFixedSemanticCollision (locate block) key))
+        visible <- Except.lift
+            (Declaration.resolveVisibleGlobalLowering key)
+        when
+            (isJust visible)
+            (Except.throwError
+                (ExactGlobalAlreadyVisible (locate block) key))
+        (head', family, rawBody) <-
+            prepareHead block key
+        slot <- Except.lift Declaration.nextDeclarationSlotLowering
+        theory <- Except.lift Declaration.currentTheoryLowering
+        (body, globals) <-
+            case rawBody of
+                Nothing -> pure (OpaqueBody, Map.empty)
+                Just buildBody -> do
+                    let initialElaboration =
+                            ElaborationState
+                                { elaborationBinders = mempty
+                                , elaborationBinderDepth = 0
+                                , elaborationStructures = mempty
+                                , elaborationGlobals = mempty
+                                , elaborationContextualBinder = Nothing
+                                , elaborationContextualRequirements = mempty
+                                }
+                    (CompiledBody canonical rawConstruction, finalElaboration) <-
+                        State.runStateT buildBody initialElaboration
+                    let PreparedHead _semanticKey parameters _coreType = head'
+                    construction <-
+                        Except.liftEither
+                            (traverse
+                                (checkCompiledNamedSetConstruction
+                                    (`Map.lookup`
+                                        elaborationGlobals finalElaboration)
+                                    (replicate (length parameters) TySet))
+                                rawConstruction)
+                    traverse_
+                        (\checkedConstruction ->
+                            unless
+                                (frozenCoreTerm
+                                    (preparedSetConstructionClosedBody
+                                        checkedConstruction)
+                                    == canonical)
+                                (impossible
+                                    "exact named construction disagrees with its transparent body"))
+                        construction
+                    let requirements =
+                            elaborationContextualRequirements finalElaboration
+                        body
+                            | Map.null requirements =
+                                TransparentBody canonical construction
+                            | family == ExactAbbreviation =
+                                ContextualTransparentBody
+                                    requirements
+                                    (CLam TySet canonical)
+                            | otherwise =
+                                impossible
+                                    "a non-abbreviation acquired contextual requirements"
+                    pure (body, elaborationGlobals finalElaboration)
+        let PreparedHead semanticKey _parameters coreType = head'
+        unless (semanticKey == key)
+            (Except.throwError
+                (ExactDeclarationHeadMismatch (locate block)))
+        (target, content) <-
+            case body of
+                OpaqueBody -> do
+                    let seed =
+                            opaqueDeclarationSeed
+                                (declarationSlotModule slot)
+                                (declarationSlotOrdinal slot)
+                                SignatureDeclaration
+                                (generatedObjectSlot 0)
+                        content' =
+                            OpaqueObjectContent theory seed coreType
+                        identity = opaqueObjectId theory seed coreType
+                    pure (GlobalReference identity, content')
+                TransparentBody canonical _construction -> do
+                    checked <-
+                        either
+                            (Except.throwError
+                                . ExactCoreCheckFailed (locate block))
+                            pure
+                            (checkCanonicalCore
+                                (`Map.lookup` globals)
+                                canonical)
+                    unless
+                        (frozenCoreType checked == coreType)
+                        (Except.throwError
+                            (ExactObjectTypeMismatch
+                                (locate block)
+                                coreType
+                                (frozenCoreType checked)))
+                    let content' =
+                            TransparentObjectContent
+                                theory
+                                coreType
+                                canonical
+                    let identity =
+                            transparentObjectId theory coreType canonical
+                        semanticTarget =
+                            case family of
+                                ExactAbbreviation ->
+                                    TransparentExpansion identity
+                                ExactDefinition -> GlobalReference identity
+                                ExactSignature ->
+                                    impossible
+                                        "a signature acquired a transparent body"
+                    pure (semanticTarget, content')
+                ContextualTransparentBody requirements canonical -> do
+                    let contextualType = TyArrow TySet coreType
+                    checked <-
+                        either
+                            (Except.throwError
+                                . ExactCoreCheckFailed (locate block))
+                            pure
+                            (checkCanonicalCore
+                                (`Map.lookup` globals)
+                                canonical)
+                    unless
+                        (frozenCoreType checked == contextualType)
+                        (Except.throwError
+                            (ExactObjectTypeMismatch
+                                (locate block)
+                                contextualType
+                                (frozenCoreType checked)))
+                    let content' =
+                            TransparentObjectContent
+                                theory
+                                contextualType
+                                canonical
+                        identity =
+                            transparentObjectId
+                                theory contextualType canonical
+                    pure
+                        ( ContextualTransparentExpansion
+                            identity requirements
+                        , content'
+                        )
+        let targetObject = semanticGlobalTargetObject target
+        available <-
+            Except.lift (Declaration.objectAvailableLowering targetObject)
+        let alias = definitionAlias block
+            asserted
+                | available = Nothing
+                | otherwise = Just (assertedObject targetObject content)
+            syntax =
+                declarationSyntaxId
+                    (encodePreparedSyntax family head' body alias)
+        pure
+            (PreparedExactDeclaration
+                (locate block)
+                family
+                key
+                target
+                asserted
+                alias
+                (case family of
+                    ExactDefinition -> case body of
+                        TransparentBody _canonical construction -> construction
+                        _ -> Nothing
+                    _ -> Nothing)
+                syntax)
+
+lowerPreparedExactBinding
+    :: PreparedExactDeclaration
+    -> Declaration.LoweringDriver
+        (Either
+            Declaration.DeclarationError
+            (Declaration.CheckedDeclaration CheckedExactBindingAuthorization))
+lowerPreparedExactBinding prepared =
+    case preparedDefinitionAlias prepared of
+        Nothing ->
+            pure
+                (Right
+                    (checked [] CheckedExactBindingNone))
+        Just alias -> case preparedDefinitionConstruction prepared of
+            Nothing ->
+                fmap
+                    (\spec ->
+                        checked
+                            [ Declaration.checkedCandidate
+                                spec
+                                (Declaration.checkedDefinitionEquationPlanning
+                                    identity)
+                                :| []
+                            ]
+                            (CheckedExactBindingDefinition identity))
+                    <$> Declaration.prepareDefinitionEquationSpecLowering
+                        objects identity alias
+            Just (PreparedUnconditionalSetConstruction construction) ->
+                Except.runExceptT do
+                    equation <-
+                        Except.lift
+                            (Declaration.prepareDefinitionEquationSpecWithEligibilityLowering
+                                objects identity SearchIneligible alias)
+                            >>= Except.liftEither
+                    (extensional, descriptor) <-
+                        Except.lift
+                            (Declaration.prepareNamedSetConstructionSpecLowering
+                                objects identity construction)
+                            >>= Except.liftEither
+                    pure
+                        (checked
+                            [ Declaration.checkedCandidate
+                                equation
+                                (Declaration.checkedDefinitionEquationPlanning
+                                    identity)
+                                :| [ Declaration.checkedCandidate
+                                        extensional
+                                        (Declaration.checkedKernelPlanning
+                                            descriptor [])
+                                   ]
+                            ]
+                            (CheckedExactBindingConstruction
+                                identity construction))
+            Just (PreparedRelationalSetConstruction construction) ->
+                Except.runExceptT do
+                    equation <-
+                        Except.lift
+                            (Declaration.prepareDefinitionEquationSpecWithEligibilityLowering
+                                objects identity SearchIneligible alias)
+                            >>= Except.liftEither
+                    let functionality =
+                            relationalSetConstructionClosedFunctionality
+                                construction
+                        functionalityScoped =
+                            embedClosedCore [] functionality
+                    functionalitySpec <-
+                        Except.lift
+                            (Declaration.prepareFrozenCandidateSpecLowering
+                                objects functionality SearchIneligible [])
+                            >>= Except.liftEither
+                    obligation <-
+                        Except.lift
+                            (Declaration.prepareScopedVampireObligationLowering
+                                Vector.empty
+                                functionalityScoped
+                                []
+                                []
+                                Declaration.VampireImplicitPremises)
+                            >>= either
+                                (Except.throwError
+                                    . Declaration.ProofObligationFailedAt location
+                                    . Declaration.CurrentCandidateVampirePreparationFailed)
+                                pure
+                    (extensional, descriptor) <-
+                        Except.lift
+                            (Declaration.prepareRelationalSetConstructionSpecLowering
+                                objects identity construction functionality)
+                            >>= Except.liftEither
+                    pure
+                        (checked
+                            [ Declaration.checkedCandidate
+                                equation
+                                (Declaration.checkedDefinitionEquationPlanning
+                                    identity)
+                                :| [ Declaration.checkedCandidate
+                                        functionalitySpec
+                                        (Declaration.checkedSourceProofPlanning
+                                            [Declaration.checkedPlannedVampireRequest
+                                                location obligation]
+                                            [])
+                                   ]
+                            , Declaration.checkedCandidate
+                                extensional
+                                (Declaration.checkedStagedKernelPlanning
+                                    descriptor
+                                    [Declaration.plannedEarlierCandidate 0 1])
+                                :| []
+                            ]
+                            (CheckedExactBindingRelationalConstruction
+                                identity construction obligation))
+  where
+    identity = preparedExactObjectId prepared
+    objects = maybeToList (preparedExactObject prepared)
+    location = preparedExactLocation prepared
+    checked stages body =
+        Declaration.checkedCompiledDeclaration
+            (preparedExactSyntaxId prepared)
+            objects
+            []
+            [semanticGlobalBinding
+                (preparedExactGlobalKey prepared)
+                (preparedExactGlobalTarget prepared)]
+            []
+            stages
+            body
+
+data CheckedExactBindingAuthorization
+    = CheckedExactBindingNone
+    | CheckedExactBindingDefinition !ObjectId
+    | CheckedExactBindingConstruction
+        !ObjectId
+        !(NamedSetConstruction ObjectId)
+    | CheckedExactBindingRelationalConstruction
+        !ObjectId
+        !(CheckedRelationalSetConstruction ObjectId)
+        !(Declaration.PreparedVampireObligation Void ())
+
+authorizeCheckedExactBinding
+    :: CheckedExactBindingAuthorization
+    -> [NonEmpty Declaration.ReservedCandidate]
+    -> Declaration.Declaration ()
+authorizeCheckedExactBinding body stages =
+    case (body, stages) of
+        (CheckedExactBindingNone, []) -> pure ()
+        (CheckedExactBindingDefinition identity, [candidate :| []]) ->
+            Declaration.authorizeDefinitionEquationCandidate
+                identity candidate
+        ( CheckedExactBindingConstruction identity construction
+          , [equation :| [extensional]]
+          ) -> do
+            Declaration.authorizeDefinitionEquationCandidate
+                identity equation
+            Declaration.authorizeNamedSetConstructionCandidate
+                identity construction extensional
+        ( CheckedExactBindingRelationalConstruction
+                identity construction obligation
+          , [equation :| [functionality], extensional :| []]
+          ) -> do
+            Declaration.authorizeDefinitionEquationCandidate
+                identity equation
+            Declaration.authorizeVampireCandidate
+                functionality
+                (Declaration.acceptPreparedVampireObligation obligation)
+            Declaration.authorizeRelationalSetConstructionCandidate
+                identity construction functionality extensional
+        _ ->
+            Declaration.failDeclaration
+                (Declaration.CheckedAuthorizationCandidateShapeMismatch
+                    (case body of
+                        CheckedExactBindingNone -> 0
+                        CheckedExactBindingDefinition{} -> 1
+                        CheckedExactBindingConstruction{} -> 1
+                        CheckedExactBindingRelationalConstruction{} -> 2)
+                    (length stages))
+
+prepareExactStructure
+    :: Raw.Block
+    -> [CanonicalLexicalEntry]
+    -> Declaration.LoweringDriver
+        (Either ExactCompileError PreparedExactStructure)
+prepareExactStructure block entries =
+    Except.runExceptT do
+        (location, marker, structure) <-
+            case block of
+                Raw.BlockStruct location _title (Raw.Marker marker) structure ->
+                    pure (location, marker, structure)
+                _ -> Except.throwError
+                    (ExactUnsupportedDeclaration (locate block))
+        validateStructureOccurrences location structure entries
+        let structurePhrase =
+                semanticStructurePhrase (Raw.structPhrase structure)
+            parentPhrases =
+                semanticStructurePhrase <$> Raw.structParents structure
+        when
+            (structurePhrase `elem` parentPhrases)
+            (Except.throwError
+                (ExactStructureSelfParent location structurePhrase))
+        case firstDuplicate parentPhrases of
+            Just duplicate ->
+                Except.throwError
+                    (ExactStructureDuplicateParent location duplicate)
+            Nothing -> pure ()
+        visible <- Except.lift
+            (Declaration.resolveVisibleStructureLowering structurePhrase)
+        when
+            (isJust visible)
+            (Except.throwError
+                (ExactStructureAlreadyVisible location structurePhrase))
+        parents <- traverse (resolveParent location) parentPhrases
+        inherited <-
+            foldM mergeParentOperations Map.empty
+                (zip parentPhrases parents)
+        case firstDuplicate (Raw.structFixes structure) of
+            Just duplicate ->
+                Except.throwError
+                    (ExactStructureDuplicateOperation location duplicate)
+            Nothing -> pure ()
+        traverse_
+            (\symbol ->
+                when
+                    (Map.member symbol inherited)
+                    (Except.throwError
+                        (ExactStructureOperationAlreadyInherited
+                            location symbol)))
+            (Raw.structFixes structure)
+        slot <- Except.lift Declaration.nextDeclarationSlotLowering
+        theory <- Except.lift Declaration.currentTheoryLowering
+        let operationType = TyArrow TySet TySet
+            makeOperation index symbol =
+                let seed =
+                        opaqueDeclarationSeed
+                            (declarationSlotModule slot)
+                            (declarationSlotOrdinal slot)
+                            StructureDeclaration
+                            (generatedObjectSlot index)
+                    content = OpaqueObjectContent theory seed operationType
+                    identity = opaqueObjectId theory seed operationType
+                in ( symbol
+                   , identity
+                   , assertedObject identity content
+                   )
+            ownOperations =
+                zipWith makeOperation [0 ..] (Raw.structFixes structure)
+            operationObjects =
+                [ asserted
+                | (_symbol, _identity, asserted) <- ownOperations
+                ]
+            completeOperations =
+                Map.union
+                    (Map.fromList
+                        [ (symbol, identity)
+                        | (symbol, identity, _asserted) <- ownOperations
+                        ])
+                    (fst <$> inherited)
+        unless
+            (Map.member Raw.CarrierSymbol completeOperations)
+            (Except.throwError
+                (ExactStructureHasNoCarrier location structurePhrase))
+        context <-
+            either Except.throwError pure
+                (extendExactBinderContext
+                    ((exactLocalId 0, Raw.structLabel structure) :| [])
+                    emptyExactBinderContext)
+        let provisionalAnnotation =
+                ExactStructureAnnotation
+                    structurePhrase Nothing completeOperations
+            structureContext =
+                annotateBinderContext
+                    (Map.singleton 0 provisionalAnnotation)
+                    context
+        checkedAssumptions <-
+            traverse
+                (\(assumptionMarker, assumption) -> do
+                    prepared <- Except.lift
+                        (prepareExactProposition structureContext assumption)
+                    proposition <- Except.liftEither prepared
+                    pure
+                        ( locate assumption
+                        , assumptionMarker
+                        , preparedExactPropositionCore proposition
+                        ))
+                (Raw.structAssumes structure)
+        parentTerms <-
+            fmap catMaybes
+                (traverse
+                    (\parent ->
+                        case Declaration.resolvedStructurePredicate parent of
+                            Nothing -> pure Nothing
+                            Just predicate ->
+                                pure
+                                    (Just
+                                        (CApp
+                                            (CGlobal predicate)
+                                            (CBound 0))))
+                    parents)
+        let assumptionTerms =
+                [ scopedCoreTerm proposition
+                | (_assumptionLocation, _assumptionMarker, proposition) <-
+                    checkedAssumptions
+                ]
+            predicateBody =
+                CLam TySet
+                    (logicalConjunction
+                        (parentTerms <> assumptionTerms))
+            predicateType = TyArrow TySet TyProp
+            predicateContent =
+                TransparentObjectContent theory predicateType predicateBody
+            predicate =
+                transparentObjectId theory predicateType predicateBody
+        predicateAvailable <-
+            Except.lift (Declaration.objectAvailableLowering predicate)
+        let predicateObject =
+                [ assertedObject predicate predicateContent
+                | not predicateAvailable
+                ]
+            ownBindings =
+                [ semanticStructureOperation symbol identity
+                | (symbol, identity, _asserted) <- ownOperations
+                ]
+        descriptor <-
+            Except.liftEither
+                (first
+                    (ExactStructureDescriptorInvalid location)
+                    (semanticStructureDescriptor
+                        structurePhrase
+                        (Just predicate)
+                        parentPhrases
+                        ownBindings))
+        let structureApplication =
+                CApp (CGlobal predicate) (CBound 0)
+            inheritance =
+                [ ( location
+                  , semanticName (marker <> "inherit")
+                  , CForall TySet
+                        (CImp structureApplication
+                            (logicalConjunction parentTerms))
+                  )
+                | not (null parentTerms)
+                ]
+            projections =
+                [ ( assumptionLocation
+                  , semanticName assumptionMarker
+                  , CForall TySet
+                        (CImp structureApplication
+                            (scopedCoreTerm proposition))
+                  )
+                | ( assumptionLocation
+                  , Raw.Marker assumptionMarker
+                  , proposition
+                  ) <- checkedAssumptions
+                ]
+            generatedTerms = inheritance <> projections
+            localTypes =
+                Map.fromList
+                    ((predicate, predicateType)
+                        : [ (identity, operationType)
+                          | (_symbol, identity, _asserted) <- ownOperations
+                          ])
+        resolvedTypes <-
+            resolveStructureGlobalTypes
+                localTypes
+                [ term
+                | (_factLocation, _alias, term) <- generatedTerms
+                ]
+        generated <-
+            traverse
+                (\(factLocation, alias, term) -> do
+                    frozen <-
+                        either
+                            (Except.throwError
+                                . ExactCoreCheckFailed factLocation)
+                            pure
+                            (checkCanonicalCore
+                                (`Map.lookup` resolvedTypes)
+                                term)
+                    pure
+                        (PreparedExactStructureFact
+                            factLocation frozen alias))
+                generatedTerms
+        environment <-
+            Except.liftEither
+                (first
+                    (ExactStructureDescriptorInvalid location)
+                    (semanticEnvironmentWithStructures [] [descriptor]))
+        let syntax =
+                declarationSyntaxId
+                    (encodePreparedStructure
+                        environment
+                        predicate
+                        generated)
+        pure
+            (PreparedExactStructure
+                location
+                (operationObjects <> predicateObject)
+                predicate
+                descriptor
+                (semanticName marker)
+                generated
+                syntax)
+  where
+    resolveParent location structurePhrase = do
+        resolved <- Except.lift
+            (Declaration.resolveVisibleStructureLowering structurePhrase)
+        maybe
+            (Except.throwError
+                (ExactStructureNotVisible location structurePhrase))
+            pure
+            resolved
+
+    mergeParentOperations inherited (parentPhrase, parent) =
+        foldM
+            (insertParentOperation parentPhrase)
+            inherited
+            (Map.toAscList
+                (Declaration.resolvedStructureOperations parent))
+
+    insertParentOperation parentPhrase inherited (symbol, identity) =
+        case Map.lookup symbol inherited of
+            Nothing ->
+                pure
+                    (Map.insert symbol (identity, parentPhrase) inherited)
+            Just (existing, existingOrigin)
+                | existing == identity -> pure inherited
+                | otherwise ->
+                    Except.throwError
+                        (ExactStructureOperationConflict
+                            (locate block)
+                            symbol
+                            existingOrigin
+                            parentPhrase)
+
+    resolveStructureGlobalTypes localTypes terms = do
+        let dependencies = Set.unions (canonicalTermGlobals <$> terms)
+        foldM
+            (\types identity ->
+                case Map.lookup identity types of
+                    Just{} -> pure types
+                    Nothing -> do
+                        coreType <- Except.lift
+                            (Declaration.objectTypeLowering identity)
+                        case coreType of
+                            Nothing ->
+                                Except.throwError
+                                    (ExactStructureObjectNotVisible
+                                        (locate block) identity)
+                            Just actual ->
+                                pure (Map.insert identity actual types))
+            localTypes
+            (Set.toAscList dependencies)
+
+lowerPreparedExactStructure
+    :: PreparedExactStructure
+    -> Declaration.LoweringDriver
+        (Either
+            Declaration.DeclarationError
+            (Declaration.CheckedDeclaration
+                CheckedExactStructureAuthorization))
+lowerPreparedExactStructure
+        (PreparedExactStructure
+            _location objects predicate descriptor alias generatedFacts syntax) =
+    Except.runExceptT do
+        definition <-
+            Except.lift
+                (Declaration.preparePointwiseDefinitionEquationSpecLowering
+                    objects predicate alias)
+                >>= Except.liftEither
+        generatedCandidates <-
+            traverse
+                (\(PreparedExactStructureFact
+                        factLocation target factAlias) -> do
+                    generatedSpec <- Except.lift
+                        (Declaration.prepareFrozenCandidateSpecLowering
+                            objects target SearchEligible [factAlias])
+                        >>= Except.liftEither
+                    obligation <- Except.lift
+                        (Declaration.prepareStagedCandidateVampireLowering
+                            factLocation objects definition generatedSpec)
+                        >>= Except.liftEither
+                    pure
+                        ( Declaration.checkedCandidate generatedSpec
+                            (Declaration.checkedSourceProofPlanning
+                                [ Declaration.checkedPlannedVampireRequest
+                                    factLocation obligation
+                                ]
+                                [ Declaration.plannedEarlierCandidate 0 0
+                                ])
+                        , (factLocation, obligation)
+                        ))
+                generatedFacts
+        let generatedAuthorizations =
+                snd <$> generatedCandidates
+            stages =
+                [ Declaration.checkedCandidate definition
+                    (Declaration.checkedDefinitionEquationPlanning predicate)
+                    :| []
+                ]
+                    <> maybeToList
+                        (NonEmpty.nonEmpty
+                            (fst <$> generatedCandidates))
+            body =
+                CheckedExactStructureAuthorization
+                    predicate
+                    generatedAuthorizations
+        pure
+            (Declaration.checkedCompiledDeclaration
+                syntax objects [] [] [descriptor] stages
+                body)
+
+authorizeCheckedExactStructure
+    :: CheckedExactStructureAuthorization
+    -> [NonEmpty Declaration.ReservedCandidate]
+    -> Declaration.Declaration ()
+authorizeCheckedExactStructure
+        (CheckedExactStructureAuthorization predicate obligations)
+        stages =
+    case (obligations, stages) of
+        ([], [definition :| []]) ->
+            Declaration.authorizeDefinitionEquationCandidate
+                predicate definition
+        (_, [definition :| [], generatedCandidates])
+            | length obligations == NonEmpty.length generatedCandidates -> do
+                Declaration.authorizeDefinitionEquationCandidate
+                    predicate definition
+                Declaration.authorizeVampireCandidateBatch
+                    (NonEmpty.zipWith
+                        (\candidate (factLocation, obligation) ->
+                            ( factLocation
+                            , candidate
+                            , do
+                                void
+                                    (Declaration.useStagedCandidate
+                                        definition)
+                                pure obligation
+                            ))
+                        generatedCandidates
+                        (NonEmpty.fromList obligations))
+        _ ->
+            Declaration.failDeclaration
+                (Declaration.CheckedAuthorizationCandidateShapeMismatch
+                    (if null obligations then 1 else 2)
+                    (length stages))
+
+validateStructureOccurrences
+    :: Location
+    -> Raw.StructDefn
+    -> [CanonicalLexicalEntry]
+    -> ExceptT ExactCompileError (Declaration.LoweringDriver) ()
+validateStructureOccurrences location structure entries = do
+    let Raw.LexicalItemSgPl forms structureMarker =
+            Raw.structPhrase structure
+        expected =
+            CanonicalStructureNoun
+                (Raw.sg forms)
+                (Raw.pl forms)
+                structureMarker
+                : [ CanonicalStructureOperation command
+                  | Raw.StructSymbol command <- Raw.structFixes structure
+                  ]
+    unless
+        (entries == expected)
+        (Except.throwError
+            (ExactStructureOccurrenceMismatch location))
+
+encodePreparedStructure
+    :: SemanticEnvironmentDelta
+    -> ObjectId
+    -> [PreparedExactStructureFact]
+    -> ByteString
+encodePreparedStructure environment predicate generated =
+    encodeCache do
+        putCacheTag 0x04
+        putSemanticEnvironmentDeltaCache environment
+        putObjectIdCache predicate
+        putCacheList
+            (\(PreparedExactStructureFact _location target alias) -> do
+                putCanonicalTermCache putObjectIdCache
+                    (frozenCoreTerm target)
+                putCacheText (semanticNameText alias))
+            generated
+
+prepareHead
+    :: Raw.Block
+    -> SemanticGlobalKey
+    -> ExceptT
+        ExactCompileError
+        (Declaration.LoweringDriver)
+        ( PreparedHead
+        , ExactDeclarationFamily
+        , Maybe (Elaborate CompiledBody)
+        )
+prepareHead block key =
+    case block of
+        Raw.BlockSig location _title _marker assumptions signature -> do
+            rejectHeaderAssumptions ExactGuardedOpaqueSignature assumptions
+            head' <- prepareSignature location key signature
+            pure (head', ExactSignature, Nothing)
+        Raw.BlockAbbr location _title _marker abbreviation -> do
+            (head', buildBody) <-
+                prepareAbbreviation location key abbreviation
+            pure (head', ExactAbbreviation, Just buildBody)
+        Raw.BlockDefn location _title _marker definition -> do
+            (head', buildBody) <-
+                prepareDefinition location key definition
+            pure (head', ExactDefinition, Just buildBody)
+        _ ->
+            Except.throwError (ExactUnsupportedDeclaration (locate block))
+
+prepareSignature
+    :: Location
+    -> SemanticGlobalKey
+    -> Raw.Signature
+    -> ExceptT
+        ExactCompileError
+        (Declaration.LoweringDriver)
+        PreparedHead
+prepareSignature location key = \case
+    Raw.SignatureAdj subject (Raw.Adj _ item arguments) -> do
+        ensureAdjectiveKey location item key
+        makePreparedHead
+            location key (subject : arguments) TyProp
+    Raw.SignatureSymbolic (Raw.SymbolPattern symbol parameters) nounPhrase -> do
+        unless
+            ( key
+                == SemanticExpressionFunction
+                    (Raw.mixfixPattern symbol)
+            )
+            (Except.throwError (ExactDeclarationHeadMismatch location))
+        unless
+            (exactSetNounPhrase nounPhrase)
+            (Except.throwError (ExactUnsupportedDeclarationBody location))
+        makePreparedHead location key parameters TySet
+    _ ->
+        Except.throwError (ExactUnsupportedDeclaration location)
+
+prepareAbbreviation
+    :: Location
+    -> SemanticGlobalKey
+    -> Raw.Abbreviation
+    -> ExceptT
+        ExactCompileError
+        (Declaration.LoweringDriver)
+        ( PreparedHead
+        , Elaborate CompiledBody
+        )
+prepareAbbreviation location key = \case
+    Raw.AbbreviationEq (Raw.SymbolPattern symbol parameters) expression -> do
+        ensureExpressionKey location symbol key
+        makeContextualTransparentHead
+            location key parameters TySet
+            (ordinaryCompiledBody <$> compileExpressionAsSet expression)
+    Raw.AbbreviationFun (Raw.Fun _ item parameters) term -> do
+        ensureFunctionPhraseKey location item key
+        makeContextualTransparentHead
+            location key parameters TySet
+            (ordinaryCompiledBody <$> compileTermAsSet term)
+    Raw.AbbreviationAdj subject (Raw.Adj _ item arguments) statement -> do
+        ensureAdjectiveKey location item key
+        makeContextualTransparentHead
+            location key (subject : arguments) TyProp
+            (ordinaryCompiledBody <$> compileStatement statement)
+    Raw.AbbreviationVerb subject (Raw.Verb _ item arguments) statement -> do
+        ensureVerbKey location item key
+        makeContextualTransparentHead
+            location key (subject : arguments) TyProp
+            (ordinaryCompiledBody <$> compileStatement statement)
+    Raw.AbbreviationNoun subject (Raw.Noun _ item arguments) statement -> do
+        ensureNounKey location item key
+        makeContextualTransparentHead
+            location key (subject : arguments) TyProp
+            (ordinaryCompiledBody <$> compileStatement statement)
+    Raw.AbbreviationRel left relation parameters right statement -> do
+        ensureRelationKey location relation key
+        makeContextualTransparentHead
+            location key (parameters <> [left, right]) TyProp
+            (ordinaryCompiledBody <$> compileStatement statement)
+
+prepareDefinition
+    :: Location
+    -> SemanticGlobalKey
+    -> Raw.Defn
+    -> ExceptT
+        ExactCompileError
+        (Declaration.LoweringDriver)
+        ( PreparedHead
+        , Elaborate CompiledBody
+        )
+prepareDefinition location key = \case
+    Raw.Defn assumptions head' statement -> do
+        rejectHeaderAssumptions ExactGuardedTransparentDefinition assumptions
+        (parameters, resultType) <-
+            definitionHead location key head'
+        makeTransparentHead
+            location key parameters resultType
+            (ordinaryCompiledBody <$> compileStatement statement)
+    Raw.DefnFun assumptions (Raw.Fun _ item parameters) symbolic term -> do
+        rejectHeaderAssumptions ExactGuardedTransparentDefinition assumptions
+        traverse_
+            (Except.throwError
+                . ExactDefinitionCombinedSymbolicAlias
+                . locate)
+            symbolic
+        ensureFunctionPhraseKey location item key
+        makeTransparentHead
+            location key parameters TySet
+            (compileNamedSetTerm term)
+    Raw.DefnOp (Raw.SymbolPattern symbol parameters) expression -> do
+        ensureExpressionKey location symbol key
+        makeTransparentHead
+            location key parameters TySet
+            (compileNamedSetExpression expression)
+
+definitionHead
+    :: Location
+    -> SemanticGlobalKey
+    -> Raw.DefnHead
+    -> ExceptT
+        ExactCompileError
+        (Declaration.LoweringDriver)
+        ([Raw.VarSymbol], CoreType)
+definitionHead location key = \case
+    Raw.DefnAdj annotation subject (Raw.Adj _ item arguments) -> do
+        validateDefinitionAnnotation annotation
+        ensureAdjectiveKey location item key
+        pure (subject : arguments, TyProp)
+    Raw.DefnVerb annotation subject (Raw.Verb _ item arguments) -> do
+        validateDefinitionAnnotation annotation
+        ensureVerbKey location item key
+        pure (subject : arguments, TyProp)
+    Raw.DefnNoun subject (Raw.Noun _ item arguments) -> do
+        ensureNounKey location item key
+        pure (subject : arguments, TyProp)
+    Raw.DefnRel left relation parameters right -> do
+        ensureRelationKey location relation key
+        pure (parameters <> [left, right], TyProp)
+    Raw.DefnSymbolicPredicate
+            (Raw.PrefixPredicate command arity)
+            _marker
+            parameters -> do
+        unless
+            ( key
+                == SemanticPrefixPredicate
+                    command
+                    (fromIntegral arity)
+            )
+            (Except.throwError (ExactDeclarationHeadMismatch location))
+        pure (toList parameters, TyProp)
+
+validateDefinitionAnnotation
+    :: MonadError ExactCompileError monad
+    => Maybe (Raw.NounPhrase Maybe)
+    -> monad ()
+validateDefinitionAnnotation = traverse_ \nounPhrase ->
+    unless (exactSetNounPhrase nounPhrase)
+        (throwError
+            (ExactNonCanonicalSetDefinitionAnnotation
+                (exactNounPhraseLocation nounPhrase)))
+
+rejectHeaderAssumptions
+    :: MonadError ExactCompileError monad
+    => (Location -> ExactCompileError)
+    -> [Raw.Asm]
+    -> monad ()
+rejectHeaderAssumptions makeError = \case
+    [] -> pure ()
+    assumption : _ ->
+        throwError (makeError (exactAssumptionLocation assumption))
+
+exactAssumptionLocation :: Raw.Asm -> Location
+exactAssumptionLocation = \case
+    Raw.AsmSuppose statement -> locate statement
+    Raw.AsmLetNoun variables _nounPhrase -> locate variables
+    Raw.AsmLetIn variables _expression -> locate variables
+    Raw.AsmLetThe variable _function -> locate variable
+    Raw.AsmLetEq variable _expression -> locate variable
+    Raw.AsmLetStruct variable _structure -> locate variable
+
+exactNounPhraseLocation :: Raw.NounPhraseOf t argument -> Location
+exactNounPhraseLocation
+        (Raw.NounPhrase _left noun _variables _right _suchThat) =
+    locate noun
+
+makeTransparentHead
+    :: Location
+    -> SemanticGlobalKey
+    -> [Raw.VarSymbol]
+    -> CoreType
+    -> Elaborate CompiledBody
+    -> ExceptT
+        ExactCompileError
+        (Declaration.LoweringDriver)
+        ( PreparedHead
+        , Elaborate CompiledBody
+        )
+makeTransparentHead location key parameters resultType body = do
+    (prepared, binders) <-
+        prepareParameters location key parameters resultType
+    let close = do
+            State.modify' \state ->
+                state
+                    { elaborationBinders = binders
+                    , elaborationBinderDepth =
+                        fromIntegral (length parameters)
+                    }
+            CompiledBody body' construction <- body
+            pure
+                (CompiledBody
+                    (foldr (const (CLam TySet)) body' parameters)
+                    construction)
+    pure (prepared, close)
+
+makeContextualTransparentHead
+    :: Location
+    -> SemanticGlobalKey
+    -> [Raw.VarSymbol]
+    -> CoreType
+    -> Elaborate CompiledBody
+    -> ExceptT
+        ExactCompileError
+        (Declaration.LoweringDriver)
+        ( PreparedHead
+        , Elaborate CompiledBody
+        )
+makeContextualTransparentHead location key parameters resultType body = do
+    (prepared, binders) <-
+        prepareParameters location key parameters resultType
+    let close = do
+            State.modify' \state ->
+                state
+                    { elaborationBinders = binders
+                    , elaborationBinderDepth =
+                        fromIntegral (length parameters) + 1
+                    , elaborationContextualBinder =
+                        Just (fromIntegral (length parameters))
+                    }
+            CompiledBody body' _construction <- body
+            pure
+                (CompiledBody
+                    (foldr (const (CLam TySet)) body' parameters)
+                    Nothing)
+    pure (prepared, close)
+
+makePreparedHead
+    :: Location
+    -> SemanticGlobalKey
+    -> [Raw.VarSymbol]
+    -> CoreType
+    -> ExceptT
+        ExactCompileError
+        (Declaration.LoweringDriver)
+        PreparedHead
+makePreparedHead location key parameters resultType = do
+    (prepared, _binders) <-
+        prepareParameters location key parameters resultType
+    pure prepared
+
+prepareParameters
+    :: Location
+    -> SemanticGlobalKey
+    -> [Raw.VarSymbol]
+    -> CoreType
+    -> ExceptT
+        ExactCompileError
+        (Declaration.LoweringDriver)
+        ( PreparedHead
+        , Map.Map Raw.VarSymbol Natural
+        )
+prepareParameters
+        location key parameters resultType = do
+    case firstDuplicate parameters of
+        Just duplicate ->
+            Except.throwError
+                (ExactDuplicateParameter location duplicate)
+        Nothing -> pure ()
+    let indices =
+            reverse (take (length parameters) [0 ..])
+        binders =
+            Map.fromList
+                (zip parameters indices)
+        coreType = foldr (const (TyArrow TySet)) resultType parameters
+    pure
+        ( PreparedHead key parameters coreType
+        , binders
+        )
+
+compileExpressionAsSet
+    :: Raw.Expr
+    -> Elaborate (CanonicalTerm ObjectId)
+compileExpressionAsSet expression = do
+    (term, actual) <- compileExpression expression
+    unless (actual == TySet)
+        (Except.throwError
+            (ExactExpressionExpectedSet (locate expression) actual))
+    pure term
+
+-- | Compile one set expression once while retaining the checked-source shape
+-- needed only when that expression is subsequently named by a definition.
+-- Nested constructions remain ordinary exact terms.
+compileNamedSetExpression
+    :: Raw.Expr
+    -> Elaborate CompiledBody
+compileNamedSetExpression = \case
+    Raw.ExprSep _location variable bound predicate -> do
+        (term, bound', predicate') <-
+            compileSeparation variable bound predicate
+        pure
+            (CompiledBody term
+                (Just
+                    (CompiledSeparationConstruction
+                        bound' predicate')))
+    Raw.ExprReplace _location value bounds condition -> do
+        replacement <-
+            compileFunctionalReplacement value bounds condition
+        pure
+            (CompiledBody
+                (compiledFunctionalReplacementTerm replacement)
+                (Just
+                    (CompiledFunctionalReplacementConstruction
+                        (compiledFunctionalReplacementDomains replacement)
+                        (compiledFunctionalReplacementValue replacement)
+                        (compiledFunctionalReplacementCondition replacement))))
+    Raw.ExprReplacePred _location range domainVariable bound predicate -> do
+        (term, domain, relation) <-
+            compileRelationalReplacement
+                range domainVariable bound predicate
+        pure
+            (CompiledBody term
+                (Just
+                    (CompiledRelationalReplacementConstruction
+                        domain relation)))
+    expression ->
+        (`CompiledBody` Nothing)
+            <$> compileExpressionAsSet expression
+
+compileNamedSetTerm :: Raw.Term -> Elaborate CompiledBody
+compileNamedSetTerm = \case
+    Raw.TermExpr expression -> compileNamedSetExpression expression
+    term -> ordinaryCompiledBody <$> compileTermAsSet term
+
+ordinaryCompiledBody :: CanonicalTerm ObjectId -> CompiledBody
+ordinaryCompiledBody term = CompiledBody term Nothing
+
+compileTermAsSet
+    :: Raw.Term
+    -> Elaborate (CanonicalTerm ObjectId)
+compileTermAsSet = \case
+    Raw.TermExpr expression ->
+        compileExpressionAsSet expression
+    Raw.TermFun (Raw.Fun location item arguments) -> do
+        let patterns = Raw.lexicalItemSgPlPattern item
+            key = SemanticFunctionPhrase (Raw.sg patterns) (Raw.pl patterns)
+        compiled <- traverse compileTermAsSet arguments
+        applyResolved location key compiled
+    Raw.TermQuantified _quantifier location _nounPhrase ->
+        Except.throwError
+            (ExactQuantifiedTermRequiresPropositionContext location)
+    term ->
+        Except.throwError
+            (ExactUnsupportedDeclarationBody (locate term))
+
+-- | Compile a source term only at a proposition consumer.  Indefinite terms
+-- own the continuation, so their noun constraints and quantifier surround
+-- exactly the proposition which consumes the resulting set.  Function-phrase
+-- arguments recurse through the same seam and therefore never masquerade as
+-- independently set-valued terms.
+compileTermInProposition
+    :: Raw.Term
+    -> (CanonicalTerm ObjectId
+        -> Elaborate (CanonicalTerm ObjectId))
+    -> Elaborate (CanonicalTerm ObjectId)
+compileTermInProposition term continuation =
+    case term of
+        Raw.TermExpr expression ->
+            compileExpressionAsSet expression >>= continuation
+        Raw.TermFun (Raw.Fun location item arguments) -> do
+            let patterns = Raw.lexicalItemSgPlPattern item
+                key =
+                    SemanticFunctionPhrase
+                        (Raw.sg patterns)
+                        (Raw.pl patterns)
+            compileTermsInProposition arguments \compiled -> do
+                value <- applyResolved location key compiled
+                continuation value
+        Raw.TermQuantified quantifier _location nounPhrase ->
+            compileQuantifiedTermInProposition
+                quantifier nounPhrase continuation
+        Raw.TermIota location _variable _statement ->
+            Except.throwError (ExactUnsupportedDeclarationBody location)
+
+-- | Compile source-ordered proposition terms.  The first source occurrence
+-- receives the outermost continuation and therefore the widest scope.
+compileTermsInProposition
+    :: [Raw.Term]
+    -> ([CanonicalTerm ObjectId]
+        -> Elaborate (CanonicalTerm ObjectId))
+    -> Elaborate (CanonicalTerm ObjectId)
+compileTermsInProposition terms continuation =
+    case terms of
+        [] -> continuation []
+        term : remaining ->
+            compileTermInProposition term \compiled -> do
+                compiledDepth <- State.gets elaborationBinderDepth
+                compileTermsInProposition remaining \rest -> do
+                    compiled' <-
+                        weakenElaboratedTermFrom compiledDepth compiled
+                    continuation (compiled' : rest)
+
+weakenElaboratedTermFrom
+    :: Natural
+    -> CanonicalTerm ObjectId
+    -> Elaborate (CanonicalTerm ObjectId)
+weakenElaboratedTermFrom originalDepth term = do
+    currentDepth <- State.gets elaborationBinderDepth
+    when (currentDepth < originalDepth)
+        (impossible
+            "a proposition-term continuation escaped its binder scope")
+    pure
+        (shiftCanonical
+            (currentDepth - originalDepth)
+            0
+            term)
+
+compileExpression
+    :: Raw.Expr
+    -> Elaborate (CanonicalTerm ObjectId, CoreType)
+compileExpression = \case
+    Raw.ExprVar variable -> do
+        binders <- State.gets elaborationBinders
+        case Map.lookup variable binders of
+            Just index ->
+                pure (CBound index, TySet)
+            Nothing ->
+                Except.throwError
+                    (ExactFreeVariable (locate variable) variable)
+    Raw.ExprInteger _location integer ->
+        pure (COpaqueInteger (toInteger integer), TySet)
+    Raw.ExprOp location symbol arguments -> do
+        let key =
+                SemanticExpressionFunction
+                    (Raw.mixfixPattern symbol)
+        compiled <- traverse compileExpression arguments
+        case fixedSemanticMeaning key of
+            Just (FixedIntrinsic intrinsic) ->
+                applyTyped
+                    location
+                    (CIntrinsic intrinsic)
+                    (coreIntrinsicType intrinsic)
+                    compiled
+            Just (FixedNegatedIntrinsic _intrinsic) ->
+                impossible
+                    "expression key resolved to a negated intrinsic"
+            Just FixedEquality ->
+                impossible
+                    "expression key resolved to fixed equality"
+            Just FixedDisequality ->
+                impossible
+                    "expression key resolved to fixed disequality"
+            Nothing ->
+                applyResolvedTyped
+                    location
+                    key
+                    compiled
+    Raw.ExprStructOp location symbol maybeArgument ->
+        compileStructureOperation location symbol maybeArgument
+    Raw.ExprFiniteSet _location elements -> do
+        compiled <- traverse compileExpressionAsSet elements
+        pure
+            ( foldr
+                canonicalSetInsert
+                (CIntrinsic Empty)
+                compiled
+            , TySet
+            )
+    Raw.ExprSep _location variable bound predicate -> do
+        (term, _bound, _predicate) <-
+            compileSeparation variable bound predicate
+        pure (term, TySet)
+    Raw.ExprReplace _location value bounds condition -> do
+        replacement <-
+            compileFunctionalReplacement value bounds condition
+        pure (compiledFunctionalReplacementTerm replacement, TySet)
+    Raw.ExprReplacePred location _value _variable _bound _predicate ->
+        Except.throwError
+            (ExactRelationalReplacementRequiresNamedDefinition location)
+
+compileStructureOperation
+    :: Location
+    -> Raw.StructSymbol
+    -> Maybe Raw.Expr
+    -> Elaborate (CanonicalTerm ObjectId, CoreType)
+compileStructureOperation location symbol maybeArgument = do
+    (argument, object) <-
+        case maybeArgument of
+            Just expression -> do
+                term <- compileExpressionAsSet expression
+                structures <- State.gets elaborationStructures
+                case termStructureAnnotation term structures of
+                    Just annotation -> do
+                        object <-
+                            maybe
+                                (Except.throwError
+                                    (ExactStructureOperationNotAvailable
+                                        location symbol))
+                                pure
+                                (structureAnnotationOperation
+                                    symbol annotation)
+                        pure (term, object)
+                    Nothing -> do
+                        object <-
+                            resolveUniqueStructureOperation location symbol
+                        pure (term, object)
+            Nothing -> do
+                structures <- State.gets elaborationStructures
+                case
+                    [ (CBound index, object)
+                    | (index, structure) <- Map.toAscList structures
+                    , Just object <-
+                        [structureAnnotationOperation symbol structure]
+                    ] of
+                    firstMatch : _ -> pure firstMatch
+                    [] -> do
+                        contextual <- State.gets elaborationContextualBinder
+                        case contextual of
+                            Nothing ->
+                                Except.throwError
+                                    (ExactStructureOperationNotAvailable
+                                        location symbol)
+                            Just index -> do
+                                object <-
+                                    resolveUniqueStructureOperation
+                                        location symbol
+                                recordContextualRequirement
+                                    location symbol object
+                                pure (CBound index, object)
+    recordExactGlobal object (TyArrow TySet TySet)
+    pure (CApp (CGlobal object) argument, TySet)
+  where
+    termStructureAnnotation term structures =
+        case term of
+            CBound index -> Map.lookup index structures
+            _ -> Nothing
+
+resolveUniqueStructureOperation
+    :: Location
+    -> Raw.StructSymbol
+    -> Elaborate ObjectId
+resolveUniqueStructureOperation location symbol = do
+    objects <-
+        State.lift
+            (Except.lift
+                (Declaration.resolveVisibleStructureOperationObjectsLowering
+                    symbol))
+    case objects of
+        [] ->
+            Except.throwError
+                (ExactStructureOperationNotAvailable location symbol)
+        [object] -> pure object
+        _ ->
+            Except.throwError
+                (ExactStructureOperationAmbiguous location symbol objects)
+
+recordContextualRequirement
+    :: Location
+    -> Raw.StructSymbol
+    -> ObjectId
+    -> Elaborate ()
+recordContextualRequirement location symbol object = do
+    existing <-
+        State.gets
+            (Map.lookup symbol . elaborationContextualRequirements)
+    case existing of
+        Nothing ->
+            State.modify' \state ->
+                state
+                    { elaborationContextualRequirements =
+                        Map.insert symbol object
+                            (elaborationContextualRequirements state)
+                    }
+        Just actual
+            | actual == object -> pure ()
+            | otherwise ->
+                Except.throwError
+                    (ExactContextualRequirementConflict
+                        location symbol actual object)
+
+structureCarrierCast
+    :: Location
+    -> CanonicalTerm ObjectId
+    -> Elaborate (CanonicalTerm ObjectId)
+structureCarrierCast location term =
+    case term of
+        CBound index -> do
+            annotation <- State.gets (Map.lookup index . elaborationStructures)
+            case annotation of
+                Nothing -> pure term
+                Just structure -> do
+                    carrier <-
+                        maybe
+                            (Except.throwError
+                                (ExactStructureOperationNotAvailable
+                                    location Raw.CarrierSymbol))
+                            pure
+                            (structureAnnotationOperation
+                                Raw.CarrierSymbol structure)
+                    recordExactGlobal carrier (TyArrow TySet TySet)
+                    pure (CApp (CGlobal carrier) term)
+        _ -> pure term
+
+compileMembership
+    :: Location
+    -> Raw.Sign
+    -> CanonicalTerm ObjectId
+    -> CanonicalTerm ObjectId
+    -> Elaborate (CanonicalTerm ObjectId)
+compileMembership location sign element set = do
+    checkedSet <- structureCarrierCast location set
+    let proposition =
+            CApp
+                (CApp (CIntrinsic Member) element)
+                checkedSet
+    pure case sign of
+        Raw.Positive -> proposition
+        Raw.Negative -> logicalNot proposition
+
+compileSeparation
+    :: Raw.VarSymbol
+    -> Raw.Expr
+    -> Raw.Stmt
+    -> Elaborate
+        ( CanonicalTerm ObjectId
+        , CanonicalTerm ObjectId
+        , CanonicalTerm ObjectId
+        )
+compileSeparation variable bound predicate = do
+    bound' <- compileExpressionAsSet bound
+    predicate' <-
+        withSetBinders (variable :| [])
+            (compileStatement predicate)
+    pure
+        ( CApp
+            (CApp (CIntrinsic Sep) bound')
+            (CLam TySet predicate')
+        , bound'
+        , predicate'
+        )
+
+compileRelationalReplacement
+    :: Raw.VarSymbol
+    -> Raw.VarSymbol
+    -> Raw.Expr
+    -> Raw.Stmt
+    -> Elaborate
+        ( CanonicalTerm ObjectId
+        , CanonicalTerm ObjectId
+        , CanonicalTerm ObjectId
+        )
+compileRelationalReplacement range domainVariable bound predicate = do
+    domain <- compileExpressionAsSet bound
+    relation <-
+        withSetBinders (domainVariable :| [range])
+            (compileStatement predicate)
+    let restrictedDomain =
+            CApp
+                (CApp (CIntrinsic Sep) domain)
+                (CLam TySet (logicalExists relation))
+        choiceFunction =
+            CLam TySet
+                (CApp (CIntrinsic SetChoose) (CLam TySet relation))
+        replacement =
+            CApp
+                (CApp (CIntrinsic Repl) restrictedDomain)
+                choiceFunction
+    pure (replacement, domain, relation)
+
+data CompiledFunctionalReplacement = CompiledFunctionalReplacement
+    !(CanonicalTerm ObjectId)
+    !(NonEmpty (CanonicalTerm ObjectId))
+    !(CanonicalTerm ObjectId)
+    !(Maybe (CanonicalTerm ObjectId))
+
+compiledFunctionalReplacementTerm
+    :: CompiledFunctionalReplacement
+    -> CanonicalTerm ObjectId
+compiledFunctionalReplacementTerm
+        (CompiledFunctionalReplacement term _domains _value _condition) =
+    term
+
+compiledFunctionalReplacementDomains
+    :: CompiledFunctionalReplacement
+    -> NonEmpty (CanonicalTerm ObjectId)
+compiledFunctionalReplacementDomains
+        (CompiledFunctionalReplacement _term domains _value _condition) =
+    domains
+
+compiledFunctionalReplacementValue
+    :: CompiledFunctionalReplacement
+    -> CanonicalTerm ObjectId
+compiledFunctionalReplacementValue
+        (CompiledFunctionalReplacement _term _domains value _condition) =
+    value
+
+compiledFunctionalReplacementCondition
+    :: CompiledFunctionalReplacement
+    -> Maybe (CanonicalTerm ObjectId)
+compiledFunctionalReplacementCondition
+        (CompiledFunctionalReplacement _term _domains _value condition) =
+    condition
+
+compileFunctionalReplacement
+    :: Raw.Expr
+    -> NonEmpty (Raw.VarSymbol, Raw.Expr)
+    -> Maybe Raw.Stmt
+    -> Elaborate CompiledFunctionalReplacement
+compileFunctionalReplacement
+        value ((variable, domain) :| remaining) condition = do
+    domain' <- compileExpressionAsSet domain
+    case remaining of
+        [] -> do
+            (value', condition') <-
+                withSetBinders (variable :| []) do
+                    value' <- compileExpressionAsSet value
+                    condition' <- traverse compileStatement condition
+                    pure (value', condition')
+            let filteredDomain =
+                    case condition' of
+                        Nothing -> domain'
+                        Just predicate ->
+                            CApp
+                                (CApp (CIntrinsic Sep) domain')
+                                (CLam TySet predicate)
+            pure
+                (CompiledFunctionalReplacement
+                    (CApp
+                        (CApp (CIntrinsic Repl) filteredDomain)
+                        (CLam TySet value'))
+                    (domain' :| [])
+                    value'
+                    condition')
+        next : rest -> do
+            nested <-
+                withSetBinders (variable :| [])
+                    (compileFunctionalReplacement
+                        value (next :| rest) condition)
+            pure
+                (CompiledFunctionalReplacement
+                    (CApp
+                        (CIntrinsic FamilyUnion)
+                        (CApp
+                            (CApp (CIntrinsic Repl) domain')
+                            (CLam TySet
+                                (compiledFunctionalReplacementTerm nested))))
+                    (domain'
+                        NonEmpty.<|
+                            compiledFunctionalReplacementDomains nested)
+                    (compiledFunctionalReplacementValue nested)
+                    (compiledFunctionalReplacementCondition nested))
+
+compileStatement
+    :: Raw.Stmt
+    -> Elaborate (CanonicalTerm ObjectId)
+compileStatement = \case
+    Raw.StmtFormula formula ->
+        compileFormula formula
+    Raw.StmtVerbPhrase terms verbPhrase ->
+        compileTermsInProposition (toList terms) \subjects ->
+            logicalConjunction
+                <$> traverse (`compileVerbPhrase` verbPhrase) subjects
+    Raw.StmtNoun terms nounPhrase ->
+        compileTermsInProposition (toList terms) \subjects ->
+            logicalConjunction
+                <$> traverse (`compileNounPhraseMaybe` nounPhrase) subjects
+    Raw.StmtExists _location nounPhrase ->
+        compileExistentialNounPhrase nounPhrase
+    Raw.StmtQuantPhrase
+            _location
+            (Raw.QuantPhrase quantifier nounPhrase)
+            statement ->
+        compileQuantifiedNounPhrase quantifier nounPhrase statement
+    Raw.StmtConnected connective location left right ->
+        compileConnective
+            (fromMaybe (locate left) location)
+            connective
+            compileStatement
+            left
+            right
+    Raw.StmtNeg _location statement ->
+        logicalNot <$> compileStatement statement
+    Raw.SymbolicQuantified
+            _location quantifier variables bound suchThat statement ->
+        compileSymbolicQuantified
+            quantifier variables bound suchThat (compileStatement statement)
+    Raw.StmtStruct term rawPhrase ->
+        compileTermInProposition term \subject -> do
+            annotation <-
+                resolveStructureAnnotation (locate term) rawPhrase
+            predicate <-
+                maybe
+                    (impossible "an assertable structure has no predicate")
+                    pure
+                    (structureAnnotationPredicate annotation)
+            recordExactGlobal
+                predicate
+                (TyArrow TySet TyProp)
+            pure
+                (CApp
+                    (CGlobal predicate)
+                    subject)
+
+compileQuantifiedTermInProposition
+    :: Raw.Quantifier
+    -> Raw.NounPhrase Maybe
+    -> (CanonicalTerm ObjectId
+        -> Elaborate (CanonicalTerm ObjectId))
+    -> Elaborate (CanonicalTerm ObjectId)
+compileQuantifiedTermInProposition quantifier
+        (Raw.NounPhrase left noun named right suchThat)
+        compileBody =
+    case named of
+        Nothing ->
+            withAnonymousSetBinder compileFor
+        Just variable ->
+            withSetBinders (variable :| []) do
+                subject <- compileIntroducedVariable variable
+                compileFor subject
+  where
+    compileFor subject = do
+        constraints <-
+            compileNounPhraseConstraints
+                [subject] left noun right suchThat
+        body <- compileBody subject
+        pure (quantifyNounPhrase quantifier 1 constraints body)
+
+compileSymbolicQuantified
+    :: Raw.Quantifier
+    -> NonEmpty Raw.VarSymbol
+    -> Raw.Bound
+    -> Maybe Raw.Stmt
+    -> Elaborate (CanonicalTerm ObjectId)
+    -> Elaborate (CanonicalTerm ObjectId)
+compileSymbolicQuantified quantifier variables bound suchThat compileBody =
+    withSetBinders variables do
+        boundConstraints <-
+            compileSymbolicBoundConstraintList variables bound
+        suchThatConstraints <-
+            maybeToList <$> traverse compileStatement suchThat
+        body <- compileBody
+        pure
+            (quantifyNounPhrase
+                quantifier
+                (length (toList variables))
+                (logicalConjunction
+                    (boundConstraints <> suchThatConstraints))
+                body)
+
+compileSymbolicBoundConstraintList
+    :: NonEmpty Raw.VarSymbol
+    -> Raw.Bound
+    -> Elaborate [CanonicalTerm ObjectId]
+compileSymbolicBoundConstraintList variables = \case
+    Raw.Unbounded ->
+        pure []
+    Raw.Bounded _location sign relation domain -> do
+        subjects <- traverse compileIntroducedVariable variables
+        domain' <- compileExpressionAsSet domain
+        traverse
+            (\subject -> do
+                proposition <-
+                    compileAtomicRelationTerms subject relation domain'
+                pure case sign of
+                    Raw.Positive -> proposition
+                    Raw.Negative -> logicalNot proposition)
+            (toList subjects)
+
+compileAtomicRelationTerms
+    :: CanonicalTerm ObjectId
+    -> Raw.Relation
+    -> CanonicalTerm ObjectId
+    -> Elaborate (CanonicalTerm ObjectId)
+compileAtomicRelationTerms left relation right =
+    case relation of
+        Raw.Relation location symbol parameters -> do
+            let key =
+                    SemanticRelation
+                        (Raw.relationSymbolToken symbol)
+                        (Raw.relationSymbolParameterArity symbol)
+            compiledParameters <- traverse compileExpressionAsSet parameters
+            case fixedSemanticMeaning key of
+                Just FixedEquality
+                    | null parameters -> pure (CEq TySet left right)
+                Just FixedDisequality
+                    | null parameters ->
+                        pure (logicalNot (CEq TySet left right))
+                Just (FixedIntrinsic Member)
+                    | null parameters ->
+                        compileMembership location Raw.Positive left right
+                Just (FixedNegatedIntrinsic Member)
+                    | null parameters ->
+                        compileMembership location Raw.Negative left right
+                Just (FixedIntrinsic intrinsic) -> do
+                    (term, actual) <-
+                        applyTyped
+                            location
+                            (CIntrinsic intrinsic)
+                            (coreIntrinsicType intrinsic)
+                            ((\term -> (term, TySet))
+                                <$> (compiledParameters <> [left, right]))
+                    unless (actual == TyProp)
+                        (Except.throwError
+                            (ExactFormulaExpectedProposition location actual))
+                    pure term
+                Just (FixedNegatedIntrinsic intrinsic) -> do
+                    (term, actual) <-
+                        applyTyped
+                            location
+                            (CIntrinsic intrinsic)
+                            (coreIntrinsicType intrinsic)
+                            ((\term -> (term, TySet))
+                                <$> (compiledParameters <> [left, right]))
+                    unless (actual == TyProp)
+                        (Except.throwError
+                            (ExactFormulaExpectedProposition location actual))
+                    pure (logicalNot term)
+                _ -> do
+                    (term, actual) <-
+                        applyResolvedTyped
+                            location key
+                            ((\term -> (term, TySet))
+                                <$> (compiledParameters <> [left, right]))
+                    unless (actual == TyProp)
+                        (Except.throwError
+                            (ExactFormulaExpectedProposition location actual))
+                    pure term
+        Raw.RelationExpr location expression ->
+            compileRelationExpression location expression left right
+
+compileVerbPhrase
+    :: CanonicalTerm ObjectId
+    -> Raw.VerbPhrase
+    -> Elaborate (CanonicalTerm ObjectId)
+compileVerbPhrase subject = \case
+    Raw.VPVerb verb ->
+        compileVerb subject verb
+    Raw.VPVerbNot verb ->
+        logicalNot <$> compileVerb subject verb
+    Raw.VPAdj adjectives ->
+        logicalConjunction
+            <$> traverse (compileAdjective subject) adjectives
+    Raw.VPAdjNot adjectives ->
+        logicalNot . logicalConjunction
+            <$> traverse (compileAdjective subject) adjectives
+
+compilePredicateArguments
+    :: CanonicalTerm ObjectId
+    -> [Raw.Term]
+    -> ( CanonicalTerm ObjectId
+        -> [CanonicalTerm ObjectId]
+        -> Elaborate (CanonicalTerm ObjectId)
+       )
+    -> Elaborate (CanonicalTerm ObjectId)
+compilePredicateArguments subject arguments continuation = do
+    subjectDepth <- State.gets elaborationBinderDepth
+    compileTermsInProposition arguments \compiled -> do
+        subject' <- weakenElaboratedTermFrom subjectDepth subject
+        continuation subject' compiled
+
+compileVerb
+    :: CanonicalTerm ObjectId
+    -> Raw.Verb
+    -> Elaborate (CanonicalTerm ObjectId)
+compileVerb subject (Raw.Verb location item arguments) = do
+    let patterns = Raw.lexicalItemSgPlPattern item
+    compilePredicateArguments subject arguments \subject' compiled ->
+        applyResolvedPredicate
+            location
+            (SemanticVerb (Raw.sg patterns) (Raw.pl patterns))
+            (subject' : compiled)
+
+compileAdjective
+    :: CanonicalTerm ObjectId
+    -> Raw.Adj
+    -> Elaborate (CanonicalTerm ObjectId)
+compileAdjective subject (Raw.Adj location item arguments) =
+    compilePredicateArguments subject arguments \subject' compiled ->
+        applyResolvedPredicateChoice
+            location
+            ( SemanticRightAdjective (Raw.lexicalItemPattern item)
+                :| [SemanticLeftAdjective (Raw.lexicalItemPattern item)]
+            )
+            (subject' : compiled)
+
+compileLeftAdjective
+    :: CanonicalTerm ObjectId
+    -> Raw.AdjL
+    -> Elaborate (CanonicalTerm ObjectId)
+compileLeftAdjective subject (Raw.AdjL location item arguments) =
+    compilePredicateArguments subject arguments \subject' compiled ->
+        applyResolvedPredicate
+            location
+            (SemanticLeftAdjective (Raw.lexicalItemPattern item))
+            (subject' : compiled)
+
+compileRightAttribute
+    :: CanonicalTerm ObjectId
+    -> Raw.AdjR
+    -> Elaborate (CanonicalTerm ObjectId)
+compileRightAttribute subject = \case
+    Raw.AdjR location item arguments ->
+        compilePredicateArguments subject arguments \subject' compiled ->
+            applyResolvedPredicate
+                location
+                (SemanticRightAdjective (Raw.lexicalItemPattern item))
+                (subject' : compiled)
+    Raw.AttrRThat verbPhrase ->
+        compileVerbPhrase subject verbPhrase
+
+compileNoun
+    :: CanonicalTerm ObjectId
+    -> Raw.Noun
+    -> Elaborate (CanonicalTerm ObjectId)
+compileNoun subject (Raw.Noun location item arguments)
+    | Lexicon.isBuiltinSetNoun item =
+        pure logicalTruth
+    | otherwise = do
+        let patterns = Raw.lexicalItemSgPlPattern item
+            key = SemanticNoun (Raw.sg patterns) (Raw.pl patterns)
+        compilePredicateArguments subject arguments \subject' compiled ->
+            case fixedSemanticMeaning key of
+                Just (FixedIntrinsic Member) ->
+                    case compiled of
+                        [set] ->
+                            compileMembership
+                                location Raw.Positive subject' set
+                        _ ->
+                            impossible
+                                "the fixed element noun does not have one argument"
+                Just (FixedIntrinsic intrinsic) -> do
+                    (term, actual) <-
+                        applyTyped
+                            location
+                            (CIntrinsic intrinsic)
+                            (coreIntrinsicType intrinsic)
+                            ((\argument -> (argument, TySet))
+                                <$> (subject' : compiled))
+                    unless (actual == TyProp)
+                        (Except.throwError
+                            (ExactFormulaExpectedProposition location actual))
+                    pure term
+                Just{} ->
+                    impossible "a fixed noun is not a predicate intrinsic"
+                Nothing ->
+                    applyResolvedPredicate
+                        location key (subject' : compiled)
+
+compileNounPhraseConstraints
+    :: [CanonicalTerm ObjectId]
+    -> [Raw.AdjL]
+    -> Raw.Noun
+    -> [Raw.AdjR]
+    -> Maybe Raw.Stmt
+    -> Elaborate (CanonicalTerm ObjectId)
+compileNounPhraseConstraints subjects left noun right suchThat = do
+    nounConstraints <- traverse (`compileNoun` noun) subjects
+    leftConstraints <- concat
+        <$> traverse
+            (\subject -> traverse (compileLeftAdjective subject) left)
+            subjects
+    rightConstraints <- concat
+        <$> traverse
+            (\subject -> traverse (compileRightAttribute subject) right)
+            subjects
+    suchThatConstraint <- traverse compileStatement suchThat
+    pure
+        (logicalConjunction
+            ( nounConstraints
+                <> leftConstraints
+                <> rightConstraints
+                <> maybeToList suchThatConstraint
+            ))
+
+compileNounPhraseMaybe
+    :: CanonicalTerm ObjectId
+    -> Raw.NounPhrase Maybe
+    -> Elaborate (CanonicalTerm ObjectId)
+compileNounPhraseMaybe subject
+        (Raw.NounPhrase left noun named right suchThat) =
+    case named of
+        Nothing ->
+            compileNounPhraseConstraints
+                [subject] left noun right suchThat
+        Just variable -> do
+            abstracted <-
+                withSetBinders (variable :| [])
+                    (compileNounPhraseConstraints
+                        [CBound 0] left noun right suchThat)
+            pure (instantiateCanonical subject abstracted)
+
+compileExistentialNounPhrase
+    :: Raw.NounPhrase []
+    -> Elaborate (CanonicalTerm ObjectId)
+compileExistentialNounPhrase
+        (Raw.NounPhrase left noun variables right suchThat) =
+    case NonEmpty.nonEmpty variables of
+        Just binders ->
+            withSetBinders binders do
+                subjects <- traverse compileIntroducedVariable binders
+                constraints <-
+                    compileNounPhraseConstraints
+                        (toList subjects) left noun right suchThat
+                pure
+                    (foldr
+                        (const logicalExists)
+                        constraints
+                        binders)
+        Nothing ->
+            withAnonymousSetBinder \subject ->
+                logicalExists
+                    <$> compileNounPhraseConstraints
+                        [subject] left noun right suchThat
+
+compileQuantifiedNounPhrase
+    :: Raw.Quantifier
+    -> Raw.NounPhrase []
+    -> Raw.Stmt
+    -> Elaborate (CanonicalTerm ObjectId)
+compileQuantifiedNounPhrase quantifier
+        (Raw.NounPhrase left noun variables right suchThat)
+        statement =
+    case NonEmpty.nonEmpty variables of
+        Just binders ->
+            withSetBinders binders do
+                subjects <- traverse compileIntroducedVariable binders
+                constraints <-
+                    compileNounPhraseConstraints
+                        (toList subjects) left noun right suchThat
+                body <- compileStatement statement
+                pure
+                    (quantifyNounPhrase
+                        quantifier
+                        (length (toList binders))
+                        constraints
+                        body)
+        Nothing ->
+            withAnonymousSetBinder \subject -> do
+                constraints <-
+                    compileNounPhraseConstraints
+                        [subject] left noun right suchThat
+                body <- compileStatement statement
+                pure (quantifyNounPhrase quantifier 1 constraints body)
+
+quantifyNounPhrase
+    :: Raw.Quantifier
+    -> Int
+    -> CanonicalTerm ObjectId
+    -> CanonicalTerm ObjectId
+    -> CanonicalTerm ObjectId
+quantifyNounPhrase quantifier binderCount constraints body =
+    case quantifier of
+        Raw.Universally ->
+            quantify
+                (if constraints == logicalTruth
+                    then body
+                    else CImp constraints body)
+        Raw.Existentially ->
+            quantify
+                (if constraints == logicalTruth
+                    then body
+                    else logicalAnd constraints body)
+        Raw.Nonexistentially ->
+            logicalNot
+                (quantify
+                    (if constraints == logicalTruth
+                        then body
+                        else logicalAnd constraints body))
+  where
+    quantify scoped =
+        foldr (const binder) scoped [1 .. binderCount]
+    binder = case quantifier of
+        Raw.Universally -> CForall TySet
+        Raw.Existentially -> logicalExists
+        Raw.Nonexistentially -> logicalExists
+
+withAnonymousSetBinder
+    :: (CanonicalTerm ObjectId -> Elaborate value)
+    -> Elaborate value
+withAnonymousSetBinder action = do
+    outer <- State.gets elaborationBinders
+    outerDepth <- State.gets elaborationBinderDepth
+    outerStructures <- State.gets elaborationStructures
+    outerContextual <- State.gets elaborationContextualBinder
+    State.modify' \state ->
+        state
+            { elaborationBinders = (+ 1) <$> outer
+            , elaborationBinderDepth = outerDepth + 1
+            , elaborationStructures =
+                Map.mapKeysMonotonic (+ 1) outerStructures
+            , elaborationContextualBinder = (+ 1) <$> outerContextual
+            }
+    result <- action (CBound 0)
+    State.modify' \state ->
+        state
+            { elaborationBinders = outer
+            , elaborationBinderDepth = outerDepth
+            , elaborationStructures = outerStructures
+            , elaborationContextualBinder = outerContextual
+            }
+    pure result
+
+withSetBinders
+    :: NonEmpty Raw.VarSymbol
+    -> Elaborate value
+    -> Elaborate value
+withSetBinders variables action = do
+    outer <- State.gets elaborationBinders
+    outerDepth <- State.gets elaborationBinderDepth
+    outerStructures <- State.gets elaborationStructures
+    outerContextual <- State.gets elaborationContextualBinder
+    case firstDuplicate (toList variables) of
+        Just duplicate ->
+            Except.throwError
+                (ExactDuplicateLocalBinder
+                    (locate duplicate)
+                    duplicate)
+        Nothing -> pure ()
+    case find (`Map.member` outer) (toList variables) of
+        Just shadowed ->
+            Except.throwError
+                (ExactDuplicateLocalBinder
+                    (locate shadowed)
+                    shadowed)
+        Nothing -> pure ()
+    let binderCount = fromIntegral (length (toList variables))
+        shifted = (+ binderCount) <$> outer
+        introduced =
+            Map.fromList
+                (zip
+                    (toList variables)
+                    (reverse [0 .. binderCount - 1]))
+    State.modify' \state ->
+        state
+            { elaborationBinders = introduced <> shifted
+            , elaborationBinderDepth = outerDepth + binderCount
+            , elaborationStructures =
+                Map.mapKeysMonotonic (+ binderCount) outerStructures
+            , elaborationContextualBinder =
+                (+ binderCount) <$> outerContextual
+            }
+    result <- action
+    State.modify' \state ->
+        state
+            { elaborationBinders = outer
+            , elaborationBinderDepth = outerDepth
+            , elaborationStructures = outerStructures
+            , elaborationContextualBinder = outerContextual
+            }
+    pure result
+
+compileFormula
+    :: Raw.Formula
+    -> Elaborate (CanonicalTerm ObjectId)
+compileFormula = \case
+    Raw.FormulaChain chain ->
+        compileRelationChain chain
+    Raw.PropositionalConstant _ Raw.IsBottom ->
+        pure CFalsum
+    Raw.PropositionalConstant _ Raw.IsTop ->
+        pure (CImp CFalsum CFalsum)
+    Raw.FormulaNeg _ formula ->
+        logicalNot <$> compileFormula formula
+    Raw.FormulaPredicate
+            location
+            (Raw.PrefixPredicate command arity)
+            _marker
+            arguments -> do
+        compiled <- traverse compileExpression arguments
+        (term, actual) <-
+            applyResolvedTyped
+                location
+                (SemanticPrefixPredicate
+                    command
+                    (fromIntegral arity))
+                (toList compiled)
+        unless (actual == TyProp)
+            (Except.throwError
+                (ExactFormulaExpectedProposition location actual))
+        pure term
+    Raw.Connected location connective left right ->
+        compileConnective
+            location
+            connective
+            compileFormula
+            left
+            right
+    Raw.FormulaQuantified
+            _location quantifier variables bound formula ->
+        compileSymbolicQuantified
+            quantifier variables bound Nothing (compileFormula formula)
+compileConnective
+    :: Location
+    -> Raw.Connective
+    -> (input -> Elaborate (CanonicalTerm ObjectId))
+    -> input
+    -> input
+    -> Elaborate (CanonicalTerm ObjectId)
+compileConnective _location connective compile left right = do
+    left' <- compile left
+    right' <- compile right
+    case connective of
+        Raw.Conjunction ->
+            pure (logicalAnd left' right')
+        Raw.Disjunction ->
+            pure (logicalOr left' right')
+        Raw.Implication ->
+            pure (CImp left' right')
+        Raw.Equivalence ->
+            pure (CEq TyProp left' right')
+        Raw.ExclusiveOr ->
+            pure
+                (logicalAnd
+                    (logicalOr left' right')
+                    (logicalNot (logicalAnd left' right')))
+        Raw.NegatedDisjunction ->
+            pure (logicalNot (logicalOr left' right'))
+
+logicalAnd
+    :: CanonicalTerm global
+    -> CanonicalTerm global
+    -> CanonicalTerm global
+logicalAnd left right =
+    logicalNot (CImp left (logicalNot right))
+
+logicalTruth :: CanonicalTerm global
+logicalTruth =
+    CImp CFalsum CFalsum
+
+logicalConjunction
+    :: (Foldable collection, Eq global)
+    => collection (CanonicalTerm global)
+    -> CanonicalTerm global
+logicalConjunction =
+    foldr combine logicalTruth
+  where
+    combine proposition remaining
+        | proposition == logicalTruth = remaining
+        | remaining == logicalTruth = proposition
+        | otherwise = logicalAnd proposition remaining
+
+logicalOr
+    :: CanonicalTerm global
+    -> CanonicalTerm global
+    -> CanonicalTerm global
+logicalOr left right =
+    CImp (logicalNot left) right
+
+logicalExists
+    :: CanonicalTerm global
+    -> CanonicalTerm global
+logicalExists body =
+    logicalNot (CForall TySet (logicalNot body))
+
+compileAtomicRelation
+    :: NonEmpty Raw.Expr
+    -> Raw.Relation
+    -> NonEmpty Raw.Expr
+    -> Elaborate (CanonicalTerm ObjectId)
+compileAtomicRelation left relation right =
+    case (toList left, relation, toList right) of
+        ([leftExpression], Raw.Relation location symbol parameters, [rightExpression]) -> do
+            let key =
+                    SemanticRelation
+                        (Raw.relationSymbolToken symbol)
+                        (Raw.relationSymbolParameterArity symbol)
+            case fixedSemanticMeaning key of
+                Just FixedEquality
+                    | null parameters -> do
+                        left' <- compileExpressionAsSet leftExpression
+                        right' <- compileExpressionAsSet rightExpression
+                        pure (CEq TySet left' right')
+                    | otherwise ->
+                        Except.throwError
+                            (ExactUnsupportedDeclarationBody location)
+                Just FixedDisequality
+                    | null parameters -> do
+                        left' <- compileExpressionAsSet leftExpression
+                        right' <- compileExpressionAsSet rightExpression
+                        pure (logicalNot (CEq TySet left' right'))
+                    | otherwise ->
+                        Except.throwError
+                            (ExactUnsupportedDeclarationBody location)
+                Just (FixedIntrinsic Member)
+                    | null parameters -> do
+                        left' <- compileExpressionAsSet leftExpression
+                        right' <- compileExpressionAsSet rightExpression
+                        compileMembership
+                            location Raw.Positive left' right'
+                Just (FixedNegatedIntrinsic Member)
+                    | null parameters -> do
+                        left' <- compileExpressionAsSet leftExpression
+                        right' <- compileExpressionAsSet rightExpression
+                        compileMembership
+                            location Raw.Negative left' right'
+                Just (FixedIntrinsic intrinsic) -> do
+                    compiled <- traverse compileExpression
+                        (parameters <> [leftExpression, rightExpression])
+                    (term, actual) <-
+                        applyTyped
+                            location
+                            (CIntrinsic intrinsic)
+                            (coreIntrinsicType intrinsic)
+                            compiled
+                    unless (actual == TyProp)
+                        (Except.throwError
+                            (ExactFormulaExpectedProposition location actual))
+                    pure term
+                Just (FixedNegatedIntrinsic intrinsic) -> do
+                    compiled <- traverse compileExpression
+                        (parameters <> [leftExpression, rightExpression])
+                    (term, actual) <-
+                        applyTyped
+                            location
+                            (CIntrinsic intrinsic)
+                            (coreIntrinsicType intrinsic)
+                            compiled
+                    unless (actual == TyProp)
+                        (Except.throwError
+                            (ExactFormulaExpectedProposition location actual))
+                    pure (logicalNot term)
+                Nothing -> do
+                    compiled <- traverse compileExpression
+                        (parameters <> [leftExpression, rightExpression])
+                    (term, actual) <-
+                        applyResolvedTyped location key compiled
+                    unless (actual == TyProp)
+                        (Except.throwError
+                            (ExactFormulaExpectedProposition location actual))
+                    pure term
+        ([leftExpression], Raw.RelationExpr location expression, [rightExpression]) -> do
+            left' <- compileExpressionAsSet leftExpression
+            right' <- compileExpressionAsSet rightExpression
+            compileRelationExpression location expression left' right'
+        _ ->
+            Except.throwError
+                (ExactUnsupportedDeclarationBody (locate relation))
+
+compileRelationExpression
+    :: Location
+    -> Raw.Expr
+    -> CanonicalTerm ObjectId
+    -> CanonicalTerm ObjectId
+    -> Elaborate (CanonicalTerm ObjectId)
+compileRelationExpression location expression left right = do
+    relation <- compileExpressionAsSet expression
+    pair <-
+        applyResolved
+            location
+            (SemanticExpressionFunction
+                (Raw.mixfixPattern Raw.PairSymbol))
+            [left, right]
+    compileMembership location Raw.Positive pair relation
+
+compileRelationChain
+    :: Raw.Chain
+    -> Elaborate (CanonicalTerm ObjectId)
+compileRelationChain chain =
+    logicalConjunction <$> traverse compileLink (chainLinks chain)
+  where
+    compileLink (sign, relation, left, right) = do
+        proposition <-
+            compileAtomicRelation
+                (left :| []) relation (right :| [])
+        pure case sign of
+            Raw.Positive -> proposition
+            Raw.Negative -> logicalNot proposition
+
+    chainLinks = \case
+        Raw.ChainBase left sign relation right ->
+            [ (sign, relation, leftExpression, rightExpression)
+            | leftExpression <- toList left
+            , rightExpression <- toList right
+            ]
+        Raw.ChainCons left sign relation rest ->
+            let firstRight = chainFirstLeft rest
+            in
+                [ (sign, relation, leftExpression, rightExpression)
+                | leftExpression <- toList left
+                , rightExpression <- toList firstRight
+                ]
+                <> chainLinks rest
+
+    chainFirstLeft = \case
+        Raw.ChainBase left _sign _relation _right -> left
+        Raw.ChainCons left _sign _relation _rest -> left
+
+applyResolved
+    :: Location
+    -> SemanticGlobalKey
+    -> [CanonicalTerm ObjectId]
+    -> Elaborate (CanonicalTerm ObjectId)
+applyResolved location key arguments = do
+    (term, actual) <-
+        applyResolvedTyped
+            location key ((\argument -> (argument, TySet)) <$> arguments)
+    unless (actual == TySet)
+        (Except.throwError
+            (ExactExpressionExpectedSet location actual))
+    pure term
+
+applyResolvedPredicate
+    :: Location
+    -> SemanticGlobalKey
+    -> [CanonicalTerm ObjectId]
+    -> Elaborate (CanonicalTerm ObjectId)
+applyResolvedPredicate location key =
+    applyResolvedPredicateChoice location (key :| [])
+
+applyResolvedPredicateChoice
+    :: Location
+    -> NonEmpty SemanticGlobalKey
+    -> [CanonicalTerm ObjectId]
+    -> Elaborate (CanonicalTerm ObjectId)
+applyResolvedPredicateChoice location keys arguments = do
+    case firstFixedMeaning (toList keys) of
+        Just meaning ->
+            maybe
+                (impossible
+                    "a fixed equality predicate has an invalid source arity")
+                pure
+                (lowerFixedEqualityPredicate meaning arguments)
+        Nothing -> do
+            visible <- for (toList keys) \key -> do
+                found <-
+                    State.lift
+                        (Except.lift
+                            (Declaration.resolveVisibleGlobalLowering key))
+                pure ((\target -> (key, target)) <$> found)
+            case catMaybes visible of
+                [(key, _target)] -> do
+                    (term, actual) <-
+                        applyResolvedTyped
+                            location key
+                            ((\argument -> (argument, TySet)) <$> arguments)
+                    unless (actual == TyProp)
+                        (Except.throwError
+                            (ExactFormulaExpectedProposition location actual))
+                    pure term
+                [] ->
+                    Except.throwError
+                        (ExactGlobalNotVisible location (NonEmpty.head keys))
+                _ ->
+                    impossible
+                        "one adjective surface resolves to several exact globals"
+  where
+    firstFixedMeaning =
+        foldr
+            (\key found -> fixedSemanticMeaning key <|> found)
+            Nothing
+
+applyResolvedTyped
+    :: Location
+    -> SemanticGlobalKey
+    -> [(CanonicalTerm ObjectId, CoreType)]
+    -> Elaborate (CanonicalTerm ObjectId, CoreType)
+applyResolvedTyped location key arguments = do
+    visible <-
+        State.lift
+            (Except.lift
+                (Declaration.resolveVisibleGlobalContentLowering key))
+    (target, content, dependencies) <-
+        maybe
+            (Except.throwError (ExactGlobalNotVisible location key))
+            pure
+            visible
+    case target of
+        GlobalReference identity -> do
+            let coreType = objectContentType content
+            State.modify' \state ->
+                state
+                    { elaborationGlobals =
+                        Map.insert
+                            identity coreType
+                            (elaborationGlobals state)
+                    }
+            applyTyped location (CGlobal identity) coreType arguments
+        TransparentExpansion _identity ->
+            case content of
+                TransparentObjectContent _theory coreType body -> do
+                    State.modify' \state ->
+                        state
+                            { elaborationGlobals =
+                                Map.union
+                                    dependencies
+                                    (elaborationGlobals state)
+                            }
+                    applyExpandedTyped
+                        location body coreType arguments
+                _ ->
+                    impossible
+                        "validated transparent expansion has opaque content"
+        ContextualTransparentExpansion _identity requirements ->
+            case content of
+                TransparentObjectContent _theory coreType body -> do
+                    State.modify' \state ->
+                        state
+                            { elaborationGlobals =
+                                Map.union
+                                    dependencies
+                                    (elaborationGlobals state)
+                            }
+                    contextArgument <-
+                        resolveContextualExpansionArgument
+                            location key requirements
+                    applyExpandedTyped
+                        location body coreType
+                        ((contextArgument, TySet) : arguments)
+                _ ->
+                    impossible
+                        "validated contextual expansion has opaque content"
+
+resolveContextualExpansionArgument
+    :: Location
+    -> SemanticGlobalKey
+    -> Map.Map Raw.StructSymbol ObjectId
+    -> Elaborate (CanonicalTerm ObjectId)
+resolveContextualExpansionArgument location key requirements = do
+    contextual <- State.gets elaborationContextualBinder
+    case contextual of
+        Just index -> do
+            traverse_
+                (uncurry (recordContextualRequirement location))
+                (Map.toAscList requirements)
+            pure (CBound index)
+        Nothing -> do
+            structures <- State.gets elaborationStructures
+            case
+                [ CBound index
+                | (index, structure) <- Map.toAscList structures
+                , all
+                    (\(symbol, object) ->
+                        structureAnnotationOperation symbol structure
+                            == Just object)
+                    (Map.toAscList requirements)
+                ] of
+                firstMatch : _ -> pure firstMatch
+                [] ->
+                    Except.throwError
+                        (ExactContextualExpansionNotAvailable location key)
+
+applyExpandedTyped
+    :: Location
+    -> CanonicalTerm ObjectId
+    -> CoreType
+    -> [(CanonicalTerm ObjectId, CoreType)]
+    -> Elaborate (CanonicalTerm ObjectId, CoreType)
+applyExpandedTyped location body coreType arguments =
+    foldM step (body, coreType) arguments
+  where
+    step (current, currentType) (argument, argumentType) =
+        case currentType of
+            TyArrow expected result
+                | expected == argumentType ->
+                    pure
+                        ( case current of
+                            CLam binderType lambdaBody
+                                | binderType == expected ->
+                                    instantiateCanonical
+                                        argument lambdaBody
+                            _ -> CApp current argument
+                        , result
+                        )
+                | otherwise ->
+                    Except.throwError
+                        (ExactApplicationArgumentMismatch
+                            location expected argumentType)
+            actual ->
+                Except.throwError
+                    (ExactApplicationExpectedFunction location actual)
+
+applyTyped
+    :: Location
+    -> CanonicalTerm ObjectId
+    -> CoreType
+    -> [(CanonicalTerm ObjectId, CoreType)]
+    -> Elaborate (CanonicalTerm ObjectId, CoreType)
+applyTyped location function functionType arguments =
+    foldM step (function, functionType) arguments
+  where
+    step (currentFunction, currentType) (argument, argumentType) =
+        case currentType of
+            TyArrow expected result
+                | expected == argumentType ->
+                    pure (CApp currentFunction argument, result)
+                | otherwise ->
+                    Except.throwError
+                        (ExactApplicationArgumentMismatch
+                            location expected argumentType)
+            actual ->
+                Except.throwError
+                    (ExactApplicationExpectedFunction location actual)
+
+logicalNot :: CanonicalTerm global -> CanonicalTerm global
+logicalNot proposition =
+    CImp proposition CFalsum
+
+ensureExpressionKey
+    :: MonadError ExactCompileError monad
+    => Location
+    -> Raw.FunctionSymbol
+    -> SemanticGlobalKey
+    -> monad ()
+ensureExpressionKey location symbol key =
+    unless
+        (key == SemanticExpressionFunction (Raw.mixfixPattern symbol))
+        (throwError (ExactDeclarationHeadMismatch location))
+
+ensureAdjectiveKey
+    :: MonadError ExactCompileError monad
+    => Location
+    -> Raw.LexicalItem
+    -> SemanticGlobalKey
+    -> monad ()
+ensureAdjectiveKey location item key =
+    unless
+        ( key == SemanticLeftAdjective (Raw.lexicalItemPattern item)
+          || key == SemanticRightAdjective (Raw.lexicalItemPattern item)
+        )
+        (throwError (ExactDeclarationHeadMismatch location))
+
+ensureFunctionPhraseKey
+    :: MonadError ExactCompileError monad
+    => Location
+    -> Raw.LexicalItemSgPl
+    -> SemanticGlobalKey
+    -> monad ()
+ensureFunctionPhraseKey location item key =
+    let patterns = Raw.lexicalItemSgPlPattern item
+    in unless
+        (key == SemanticFunctionPhrase (Raw.sg patterns) (Raw.pl patterns))
+        (throwError (ExactDeclarationHeadMismatch location))
+
+ensureNounKey
+    :: MonadError ExactCompileError monad
+    => Location
+    -> Raw.LexicalItemSgPl
+    -> SemanticGlobalKey
+    -> monad ()
+ensureNounKey location item key =
+    let patterns = Raw.lexicalItemSgPlPattern item
+    in unless
+        (key == SemanticNoun (Raw.sg patterns) (Raw.pl patterns))
+        (throwError (ExactDeclarationHeadMismatch location))
+
+ensureVerbKey
+    :: MonadError ExactCompileError monad
+    => Location
+    -> Raw.LexicalItemSgPl
+    -> SemanticGlobalKey
+    -> monad ()
+ensureVerbKey location item key =
+    let patterns = Raw.lexicalItemSgPlPattern item
+    in unless
+        (key == SemanticVerb (Raw.sg patterns) (Raw.pl patterns))
+        (throwError (ExactDeclarationHeadMismatch location))
+
+ensureRelationKey
+    :: MonadError ExactCompileError monad
+    => Location
+    -> Raw.RelationSymbol
+    -> SemanticGlobalKey
+    -> monad ()
+ensureRelationKey location relation key =
+    unless
+        ( key
+            == SemanticRelation
+                (Raw.relationSymbolToken relation)
+                (Raw.relationSymbolParameterArity relation)
+        )
+        (throwError (ExactDeclarationHeadMismatch location))
+
+exactSetNounPhrase :: Raw.NounPhrase Maybe -> Bool
+exactSetNounPhrase = \case
+    Raw.NounPhrase
+            []
+            (Raw.Noun _ item [])
+            Nothing
+            []
+            Nothing ->
+        Lexicon.isBuiltinSetNoun item
+    _ -> False
+
+encodePreparedSyntax
+    :: ExactDeclarationFamily
+    -> PreparedHead
+    -> PreparedBody
+    -> Maybe SemanticName
+    -> ByteString
+encodePreparedSyntax
+        family (PreparedHead key _parameters coreType) body alias =
+    encodeCache do
+        putCacheTag case family of
+            ExactSignature -> 0x00
+            ExactAbbreviation -> 0x01
+            ExactDefinition -> 0x02
+        putSemanticGlobalKeyCache key
+        putCoreTypeCache coreType
+        case body of
+            OpaqueBody -> putCacheTag 0x00
+            TransparentBody canonical _construction -> do
+                putCacheTag 0x01
+                putCanonicalTermCache putObjectIdCache canonical
+            ContextualTransparentBody requirements canonical -> do
+                putCacheTag 0x02
+                putCanonicalCacheMap
+                    (\(Raw.StructSymbol symbol) -> putCacheText symbol)
+                    putObjectIdCache
+                    requirements
+                putCanonicalTermCache putObjectIdCache canonical
+        putCacheMaybe
+            (putCacheText . semanticNameText)
+            alias
+
+encodePreparedSourceAxiom
+    :: ScopedCheckedCore ObjectId
+    -> SemanticName
+    -> ByteString
+encodePreparedSourceAxiom proposition alias =
+    encodeCache do
+        putCacheTag 0x03
+        putCanonicalTermCache putObjectIdCache
+            (scopedCoreTerm proposition)
+        putCacheText (semanticNameText alias)
+
+definitionAlias :: Raw.Block -> Maybe SemanticName
+definitionAlias = \case
+    Raw.BlockDefn _location _title (Raw.Marker marker) _definition ->
+        Just (semanticName marker)
+    _ -> Nothing
+
+firstDuplicate :: Ord value => [value] -> Maybe value
+firstDuplicate =
+    go Set.empty
+  where
+    go _seen [] = Nothing
+    go seen (value : rest)
+        | value `Set.member` seen = Just value
+        | otherwise = go (Set.insert value seen) rest