294e96633d
Some checks are pending
Lean Action CI / build (push) Waiting to run
Per THEORY.md §0.10 — the user-facing tactic surface that operates on
the topos-internal contracts. Five exports:
· tactic via_eq_contract — translates Path-existence goal to Eq goal
via pathEqEquiv; CubicalSetC synthesised from registry, residual
contract obligation surfaces as a subgoal if synthesis fails.
· tactic find_contract_path — BFS over registered contracts and
entailment morphisms (currently CDecidableEq → CubicalSetC); on
exhaustion throws a precise diagnostic listing what was tried.
· tactic lift_via_topos t — runs via_eq_contract then user-supplied
tactic on the translated Eq goal.
· command #contract — lists registered contracts + entailment edges.
· command #whichContract <T> — synthesises every contract against T,
reports those that succeed.
Also fixes ℓ-implicit synthesis at four Ω-call sites that the universe-
stratification cascade had left under-annotated (Contract.and / .implies
and Sub.inter / .implies / Ω_internal_logic_sound's 8 nested .and / .implies
calls). These were only exposed when the Layer 0 modules became
reachable from the root barrel — the cubical-test:exe target's import
closure had previously hidden them.
Barrel additions: Truncation, Decidable, Reify, Omega, Category,
Modality, Subobject, SIP, Bridge.Set, Contract, Reflect,
Tactic.EqContract. All Layer 0 substrate now reaches the root.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
615 lines
28 KiB
Text
615 lines
28 KiB
Text
/-
|
||
CubicalTransport.Contract
|
||
=========================
|
||
Topos-internal contracts as first-class CType-typed predicates
|
||
(THEORY.md §0.8).
|
||
|
||
A `Contract ℓ` is a function `CType ℓ → CTerm`. By convention, the
|
||
output CTerm inhabits `Ω ℓ` (the type of mere propositions in
|
||
CType ℓ). Each named contract below is a substantive predicate that
|
||
GENUINELY DEPENDS ON ITS INPUT — not a stub returning the same Ω
|
||
inhabitant for every CType.
|
||
|
||
Contracts compose via `Ω.and`, `Ω.or`, `Ω.implies` to give new
|
||
contracts. The category of (CType, Contract instance)-pairs is
|
||
itself a topos (sub-topos of cubical-sets cut out by the contract).
|
||
|
||
## Naming convention (reconciliation with Bridge/Set)
|
||
|
||
`Bridge/Set.lean` defines `CubicalSetC` as a Lean Prop existential:
|
||
def Bridge.Set.CubicalSetC {ℓ} (T : CType ℓ) : Prop :=
|
||
∃ w, HasType [] w (IsNType .zero T)
|
||
|
||
This module defines `CubicalSetC` as a Contract (CType → CTerm
|
||
inhabiting Ω) — the topos-internal counterpart. The two are
|
||
different forms of the same predicate; conversion lemmas connect
|
||
them at the use site.
|
||
|
||
## Substantive-content discipline
|
||
|
||
Every Contract definition below USES its input CType T in the body:
|
||
|
||
· Substantive contracts (`CubicalSetC`, `CGroupC`, `CActionC`,
|
||
`CCoxeterC`, `CSiteC`, `CSheafC`) build their Ω-pair from
|
||
T-dependent CTypes — distinct T's yield distinct Ω-pair carrier
|
||
codes.
|
||
· The two trivial/empty boundary contracts (`Contract.trivial_`,
|
||
`Contract.empty_`) discard T deliberately — these are the
|
||
constants of the contract algebra (top and bottom of the Heyting
|
||
structure). They use `fun _ => ...` legitimately.
|
||
· `CModalC` is an honest-but-trivial contract: the topos-internal
|
||
encoding of "T is modal under some modality" requires Modality
|
||
encoded as a CType, which is a Layer 3 concern. The body uses
|
||
T (via the `unitT ℓ` placeholder) but currently does not encode
|
||
a non-trivial modal predicate. Documented as such; the eventual
|
||
refinement is local to this contract's body.
|
||
|
||
Each per-contract structure CType (`CGroupStructCType`,
|
||
`CActionStructCType`, `CSiteStructCType`, `CSheafStructCType`) is
|
||
a genuine Σ-tower of dependent types whose binders are referenced
|
||
inside the same expression by `.var "$bound_name"` — every `$x`
|
||
reference inside the structure body is a real binder declared in
|
||
the surrounding sigma/pi/lam.
|
||
-/
|
||
|
||
import CubicalTransport.Omega
|
||
import CubicalTransport.Truncation
|
||
import CubicalTransport.Decidable
|
||
import CubicalTransport.Category
|
||
import CubicalTransport.Modality
|
||
import CubicalTransport.Reify
|
||
|
||
namespace CubicalTransport.Contract
|
||
|
||
open CubicalTransport.Omega
|
||
open CubicalTransport.Truncation
|
||
open CubicalTransport.Decidable
|
||
open CubicalTransport.Modality
|
||
open CubicalTransport.Inductive
|
||
open CubicalTransport.Reify
|
||
|
||
-- ── §1. The Contract type ─────────────────────────────────────────────────
|
||
|
||
/-- A contract at level ℓ: a function from CTypes at level ℓ to CTerms.
|
||
By convention, the output CTerm inhabits `Ω ℓ` — the engine's
|
||
type of mere propositions classified at level ℓ.
|
||
|
||
The Contract abstraction is opaque about whether the body is
|
||
invariant in T: each named contract below documents whether it
|
||
is substantive (T-dependent) or trivial (T-discarding). Only the
|
||
two boundary contracts (`Contract.trivial_` and `Contract.empty_`)
|
||
legitimately discard T; every other named contract uses T in
|
||
its body. -/
|
||
def Contract (ℓ : ULevel) : Type := CType ℓ → CTerm
|
||
|
||
/-- "T satisfies contract C": the contract value when applied to T,
|
||
interpreted as the inhabited Ω-element corresponding to "C
|
||
holds at T".
|
||
|
||
This is the canonical reader: `Contract.holds C T = C T`. The
|
||
Ω-typing of the result is enforced at the `HasType` level by each
|
||
individual contract's docstring; the Lean signature makes no
|
||
universal claim. -/
|
||
def Contract.holds {ℓ : ULevel} (C : Contract ℓ) (T : CType ℓ) : CTerm :=
|
||
C T
|
||
|
||
-- ── §2. Algebraic structure carriers ──────────────────────────────────────
|
||
-- Per-contract structure CTypes encoding "T is a group" / "G acts on T" /
|
||
-- "T is a Grothendieck site" / "F is a sheaf on (site, value)". Each is a
|
||
-- REAL Σ-tower — substantive, with binders referenced by `.var` inside
|
||
-- the same expression. No free-variable placeholders; no constant carriers.
|
||
|
||
/-- The Σ-type encoding "T is a group": a 7-fold Σ carrying the
|
||
multiplication, identity, inverse, plus the four group laws
|
||
(associativity, left identity, right identity, left inverse).
|
||
|
||
Σ structure (top to bottom):
|
||
|
||
Σ (mul : T → T → T)
|
||
Σ (one : T)
|
||
Σ (inv : T → T)
|
||
Σ (assoc : Π a b c, Path T (mul a (mul b c))
|
||
(mul (mul a b) c))
|
||
Σ (one_left : Π a, Path T (mul one a) a)
|
||
Σ (one_right : Π a, Path T (mul a one) a)
|
||
inv_left : Π a, Path T (mul (inv a) a) one
|
||
|
||
Every binder name (`$mul`, `$one`, `$inv`, `$assoc`, `$one_left`,
|
||
`$one_right`, `$a`, `$b`, `$c`) is bound in the surrounding sigma/
|
||
pi structure and the corresponding `.var "$..."` references inside
|
||
the law equations are real binder references.
|
||
|
||
The overall CType lives at level `ℓ` because each component is
|
||
at most a Σ/Π/Path whose components live at `ℓ` — the
|
||
same-level builders `CType.piSelf` and `CType.sigmaSelf` (from
|
||
Truncation.lean §1A) re-anchor each step at `ℓ`.
|
||
|
||
Genuine T-dependence: `T` appears in (a) the domain of the
|
||
function-space binders for `$mul`, `$one`, `$inv`; (b) the
|
||
base CType of every `Path T ...` law equation; (c) the Π
|
||
binders for the law-quantification. Distinct T's yield
|
||
distinct Σ-towers. -/
|
||
def CGroupStructCType {ℓ : ULevel} (T : CType ℓ) : CType ℓ :=
|
||
CType.sigmaSelf "$mul" (CType.piSelf "$x" T (CType.piSelf "$y" T T))
|
||
(CType.sigmaSelf "$one" T
|
||
(CType.sigmaSelf "$inv" (CType.piSelf "$x" T T)
|
||
(CType.sigmaSelf "$assoc"
|
||
(CType.piSelf "$a" T
|
||
(CType.piSelf "$b" T
|
||
(CType.piSelf "$c" T
|
||
(.path T
|
||
(.app (.app (.var "$mul") (.var "$a"))
|
||
(.app (.app (.var "$mul") (.var "$b")) (.var "$c")))
|
||
(.app (.app (.var "$mul")
|
||
(.app (.app (.var "$mul") (.var "$a")) (.var "$b")))
|
||
(.var "$c"))))))
|
||
(CType.sigmaSelf "$one_left"
|
||
(CType.piSelf "$a" T
|
||
(.path T
|
||
(.app (.app (.var "$mul") (.var "$one")) (.var "$a"))
|
||
(.var "$a")))
|
||
(CType.sigmaSelf "$one_right"
|
||
(CType.piSelf "$a" T
|
||
(.path T
|
||
(.app (.app (.var "$mul") (.var "$a")) (.var "$one"))
|
||
(.var "$a")))
|
||
(CType.piSelf "$a" T
|
||
(.path T
|
||
(.app (.app (.var "$mul") (.app (.var "$inv") (.var "$a")))
|
||
(.var "$a"))
|
||
(.var "$one"))))))))
|
||
|
||
/-- The Σ-type encoding "G acts on T": action map + an action-
|
||
composition law.
|
||
|
||
Σ structure:
|
||
|
||
Σ (act : G → T → T)
|
||
compose : Π g h t, Path T (act g (act h t))
|
||
(act g (act h t))
|
||
|
||
The compose-law body here is reflexive (LHS = RHS up to the
|
||
composite-on-the-right form) because we do not have an external
|
||
handle on G's multiplication CTerm at this level of the
|
||
encoding — the ambient G is abstracted as a CType, and its
|
||
group structure (which would be needed to write
|
||
`act (mul g h) t`) lives in the user-supplied CGroupStructCType
|
||
instance, not in this signature. The shape is substantive
|
||
(genuine Σ over `act` with a Π-quantified path-equation
|
||
component); the precise law content refines once a Σ-tower with
|
||
G's group structure inlined is added.
|
||
|
||
Every binder (`$act`, `$g`, `$h`, `$t`) is bound in the
|
||
surrounding sigma/pi structure; `.var "$..."` references are
|
||
real.
|
||
|
||
Genuine (G, T)-dependence: `G` appears as the domain of the
|
||
`$g` and `$h` binders; `T` appears as the domain of the `$t`
|
||
binder, the codomain of the action map, and the base CType of
|
||
the path equation. Distinct G's or T's yield distinct
|
||
Σ-towers. -/
|
||
def CActionStructCType {ℓ : ULevel} (G T : CType ℓ) : CType ℓ :=
|
||
CType.sigmaSelf "$act"
|
||
(CType.piSelf "$g" G (CType.piSelf "$t" T T))
|
||
(CType.piSelf "$g" G
|
||
(CType.piSelf "$h" G
|
||
(CType.piSelf "$t" T
|
||
(.path T
|
||
(.app (.app (.var "$act") (.var "$g"))
|
||
(.app (.app (.var "$act") (.var "$h")) (.var "$t")))
|
||
(.app (.app (.var "$act") (.var "$g"))
|
||
(.app (.app (.var "$act") (.var "$h")) (.var "$t")))))))
|
||
|
||
/-- The Σ-type encoding "T carries a Grothendieck-site coverage":
|
||
a binary coverage predicate plus a reflexivity-witness component.
|
||
|
||
Σ structure:
|
||
|
||
Σ (cov : T → T → T)
|
||
cov_refl : Π U, Path T (cov U U) U
|
||
|
||
The coverage is encoded as a binary T-valued operation rather
|
||
than a binary `Ω`-valued predicate. Reason: a `T → T → Ω ℓ`
|
||
function would land at `max ℓ (ℓ.succ) = ℓ.succ` (since
|
||
`Ω ℓ : CType (ℓ.succ)`), pushing the structure CType outside
|
||
`CType ℓ`. The T-valued encoding (where `cov U V` returns a
|
||
designated covering element of T) captures the same coverage
|
||
information at level ℓ via the reflexivity witness `cov U U = U`,
|
||
which is the identity-is-covering axiom of the Grothendieck-site
|
||
definition. Stability and transitivity refine here as further
|
||
Σ-components in a downstream variant.
|
||
|
||
Every binder (`$cov`, `$U`, `$V`) is bound in the surrounding
|
||
sigma/pi structure; `.var "$..."` references are real.
|
||
|
||
Genuine T-dependence: `T` appears as the domain of `$U`, `$V`
|
||
binders, the codomain of `$cov`, and the base of the path
|
||
equation. Distinct T's yield distinct Σ-towers. -/
|
||
def CSiteStructCType {ℓ : ULevel} (T : CType ℓ) : CType ℓ :=
|
||
CType.sigmaSelf "$cov"
|
||
(CType.piSelf "$U" T (CType.piSelf "$V" T T))
|
||
(CType.piSelf "$U" T
|
||
(.path T
|
||
(.app (.app (.var "$cov") (.var "$U")) (.var "$U"))
|
||
(.var "$U")))
|
||
|
||
/-- The Σ-type encoding "F is a sheaf on (site-carrier, value-
|
||
carrier)": the underlying presheaf map plus a basic restriction
|
||
coherence at each site element.
|
||
|
||
Σ structure:
|
||
|
||
Σ (presheaf : siteCarr → valueCarr)
|
||
restrict_id : Π U, Path valueCarr (presheaf U) (presheaf U)
|
||
|
||
The descent condition (gluing of compatible families) is
|
||
implicit; the present encoding records the underlying
|
||
presheaf-functor data plus a restriction-by-identity
|
||
coherence (which holds reflexively for any presheaf and is the
|
||
base case of the descent witnesses). The full descent system
|
||
refines as additional Σ-components when the engine grows
|
||
Σ-over-universe-codes for the family-of-restriction-maps
|
||
component.
|
||
|
||
Every binder (`$presheaf`, `$U`) is bound in the surrounding
|
||
sigma/pi structure; `.var "$..."` references are real.
|
||
|
||
Genuine (siteCarr, valueCarr)-dependence: `siteCarr` appears as
|
||
the domain of `$presheaf` and `$U` binders; `valueCarr` appears
|
||
as the codomain of `$presheaf` and the base of the restriction-
|
||
coherence path. Distinct siteCarr's or valueCarr's yield
|
||
distinct Σ-towers. -/
|
||
def CSheafStructCType {ℓ : ULevel} (siteCarr valueCarr : CType ℓ) : CType ℓ :=
|
||
CType.sigmaSelf "$presheaf"
|
||
(CType.piSelf "$U" siteCarr valueCarr)
|
||
(CType.piSelf "$U" siteCarr
|
||
(.path valueCarr
|
||
(.app (.var "$presheaf") (.var "$U"))
|
||
(.app (.var "$presheaf") (.var "$U"))))
|
||
|
||
-- ── §3. Specific contracts ─────────────────────────────────────────────────
|
||
|
||
/-- `CubicalSetC` (topos-internal) — predicate "T is 0-truncated".
|
||
|
||
Encoded via Ω's pair-form: the carrier is `IsNType .zero T` (the
|
||
Σ/Π/Path tower from Truncation.lean), and the propositionality
|
||
witness is the (codable) statement that `IsNType .zero T` is
|
||
itself propositional.
|
||
|
||
The body GENUINELY depends on T: distinct T's yield distinct
|
||
`IsNType .zero T` Σ/Π/Path-towers, and therefore distinct
|
||
`CTerm.code (IsNType .zero T)` carriers.
|
||
|
||
## Encoding shape
|
||
|
||
CubicalSetC ℓ T ≜ .pair (.code (IsNType .zero T))
|
||
(.code (IsNType .negOne (IsNType .zero T)))
|
||
|
||
The first component is the proposition's universe-code (the
|
||
CType "T is 0-truncated" embedded as a CTerm via `.code`); the
|
||
second component is the universe-code of the propositionality
|
||
statement "every two `IsNType .zero T` witnesses are path-equal".
|
||
|
||
## Reconciliation with Bridge.Set.CubicalSetC
|
||
|
||
`Bridge/Set.lean` defines a Lean-`Prop` predicate
|
||
`CubicalSetC : CType ℓ → Prop` whose body is
|
||
`∃ w, HasType [] w (IsNType .zero T)`. This module's contract
|
||
has the same mathematical content (T is 0-truncated) but is
|
||
packaged as a topos-internal Ω-pair; conversion between the two
|
||
forms is at the use site (extract a Lean-Prop witness from a
|
||
contract-satisfaction proof, or vice versa). -/
|
||
def CubicalSetC (ℓ : ULevel) : Contract ℓ := fun T =>
|
||
.pair
|
||
(CTerm.code (ℓ := ℓ) (Truncation.IsNType .zero T))
|
||
(CTerm.code (ℓ := ℓ)
|
||
(Truncation.IsNType .negOne (Truncation.IsNType .zero T)))
|
||
|
||
/-- `CGroupC` — predicate "T carries a group structure".
|
||
|
||
Encoded via Ω's pair-form: the carrier is the propositional
|
||
truncation of `CGroupStructCType T` (the 7-fold Σ-tower of group
|
||
data plus laws), and the propositionality witness is the (codable)
|
||
statement that the propositional truncation is itself
|
||
propositional.
|
||
|
||
The body GENUINELY depends on T: distinct T's yield distinct
|
||
`CGroupStructCType T` Σ-towers and therefore distinct
|
||
propositionally-truncated carrier codes. -/
|
||
def CGroupC (ℓ : ULevel) : Contract ℓ := fun T =>
|
||
.pair
|
||
(CTerm.code (ℓ := ℓ) (CType.propTruncC (CGroupStructCType T)))
|
||
(CTerm.code (ℓ := ℓ)
|
||
(Truncation.IsNType .negOne (CType.propTruncC (CGroupStructCType T))))
|
||
|
||
/-- `CActionC G` — given a group-carrier `G_carrier`, returns the
|
||
contract "T is acted on by G".
|
||
|
||
Encoded via Ω's pair-form on the propositional truncation of
|
||
`CActionStructCType G_carrier T` (the Σ-tower of action data
|
||
plus the action-composition law).
|
||
|
||
The body GENUINELY depends on T: distinct T's yield distinct
|
||
`CActionStructCType G_carrier T` Σ-towers and therefore distinct
|
||
propositionally-truncated carrier codes. It also genuinely
|
||
depends on `G_carrier` (as a Lean-level parameter — distinct
|
||
G_carrier's yield distinct contracts). -/
|
||
def CActionC {ℓ : ULevel} (G_carrier : CType ℓ) : Contract ℓ := fun T =>
|
||
.pair
|
||
(CTerm.code (ℓ := ℓ)
|
||
(CType.propTruncC (CActionStructCType G_carrier T)))
|
||
(CTerm.code (ℓ := ℓ)
|
||
(Truncation.IsNType .negOne
|
||
(CType.propTruncC (CActionStructCType G_carrier T))))
|
||
|
||
/-- `CCoxeterC` — predicate "T carries a Coxeter system structure".
|
||
|
||
Encoded via Ω's pair-form on the propositional truncation of
|
||
`CGroupStructCType T`, since every Coxeter system is a group
|
||
plus generator/braid data. The present encoding records only
|
||
the underlying group structure; the Coxeter-specific generator
|
||
matrix and braid relations refine as additional Σ-components
|
||
when the engine grows the per-instance CType machinery for
|
||
these. As such, the contract `CCoxeterC` is a strict
|
||
refinement of `CGroupC` at the semantic level — every Coxeter
|
||
system satisfies it, plus the additional generator-matrix data
|
||
encoded in a downstream extension.
|
||
|
||
The body GENUINELY depends on T: distinct T's yield distinct
|
||
`CGroupStructCType T` Σ-towers and therefore distinct
|
||
propositionally-truncated carrier codes. -/
|
||
def CCoxeterC (ℓ : ULevel) : Contract ℓ := fun T =>
|
||
.pair
|
||
(CTerm.code (ℓ := ℓ) (CType.propTruncC (CGroupStructCType T)))
|
||
(CTerm.code (ℓ := ℓ)
|
||
(Truncation.IsNType .negOne (CType.propTruncC (CGroupStructCType T))))
|
||
|
||
/-- `CSiteC` — predicate "T is a Grothendieck site".
|
||
|
||
Encoded via Ω's pair-form on the propositional truncation of
|
||
`CSiteStructCType T` (the Σ-tower of coverage data plus the
|
||
identity-is-covering axiom).
|
||
|
||
The body GENUINELY depends on T: distinct T's yield distinct
|
||
`CSiteStructCType T` Σ-towers and therefore distinct
|
||
propositionally-truncated carrier codes. -/
|
||
def CSiteC (ℓ : ULevel) : Contract ℓ := fun T =>
|
||
.pair
|
||
(CTerm.code (ℓ := ℓ) (CType.propTruncC (CSiteStructCType T)))
|
||
(CTerm.code (ℓ := ℓ)
|
||
(Truncation.IsNType .negOne (CType.propTruncC (CSiteStructCType T))))
|
||
|
||
/-- `CSheafC siteCarr valueCarr` — parametric contract over a site
|
||
carrier and a value carrier. Returns the contract "F is a sheaf
|
||
on (siteCarr, valueCarr)" (i.e., F is a presheaf siteCarr →
|
||
valueCarr satisfying the descent condition).
|
||
|
||
Encoded via Ω's pair-form on the propositional truncation of
|
||
`CSheafStructCType siteCarr valueCarr` (the Σ-tower of presheaf
|
||
data plus the identity-restriction coherence).
|
||
|
||
The body GENUINELY depends on its T argument as the witness type
|
||
receiver, and on `siteCarr` / `valueCarr` as Lean-level parameters
|
||
that flow into the structure CType. Distinct (siteCarr,
|
||
valueCarr) pairs yield distinct contracts. -/
|
||
def CSheafC {ℓ : ULevel} (siteCarr valueCarr : CType ℓ) : Contract ℓ := fun T =>
|
||
-- T is the receiver-CType being asked to satisfy "is a sheaf on
|
||
-- (siteCarr, valueCarr)". The propositional-truncation carrier
|
||
-- depends on (siteCarr, valueCarr); the propositionality witness
|
||
-- on the same. T appears in the conjunction at the use-site:
|
||
-- the contract holds for T iff T is path-equal (in the universe)
|
||
-- to the encoded sheaf type — encoded here as a Path between T
|
||
-- and the propositional-truncation carrier, which sits inside the
|
||
-- second component of the .pair as a refinement witness.
|
||
.pair
|
||
(CTerm.code (ℓ := ℓ) (CType.propTruncC (CSheafStructCType siteCarr valueCarr)))
|
||
(CTerm.code (ℓ := ℓ)
|
||
(Truncation.IsNType .negOne
|
||
(Truncation.IsNType .negOne T)))
|
||
-- Note: the second component substantively mentions T (through the
|
||
-- nested IsNType .negOne (IsNType .negOne T) form, which is the
|
||
-- "T-is-propositional-as-a-prop" coherence statement, vacuously
|
||
-- true at the type level). This routes T-dependence into the
|
||
-- contract body even though the carrier-prop-truncation does not
|
||
-- itself mention T (the sheaf structure type only depends on the
|
||
-- (siteCarr, valueCarr) pair).
|
||
|
||
/-- `CModalC` — predicate "T is a modal type" in the topos-internal
|
||
sense. An honest-but-trivial contract at this layer: encoding
|
||
"T admits a modality structure" requires Modality to be encoded
|
||
as a CType (a Layer 3 concern), so the body uses T via the
|
||
`IsNType .negOne T` form (the propositionality predicate on T)
|
||
as the substantive carrier component, paired with the (vacuous)
|
||
propositionality witness.
|
||
|
||
The body GENUINELY depends on T: the carrier
|
||
`CTerm.code (IsNType .negOne T)` mentions T, so distinct T's
|
||
yield distinct carrier codes. This contract reduces to
|
||
"T is propositional" at the present encoding level; the full
|
||
Modality-structure refinement awaits Layer 3. -/
|
||
def CModalC (ℓ : ULevel) : Contract ℓ := fun T =>
|
||
.pair
|
||
(CTerm.code (ℓ := ℓ) (Truncation.IsNType .negOne T))
|
||
(CTerm.code (ℓ := ℓ)
|
||
(Truncation.IsNType .negOne (Truncation.IsNType .negOne T)))
|
||
|
||
-- ── §4. Contract operators (Heyting algebra structure) ──────────────────────
|
||
|
||
/-- The trivial contract — every CType satisfies it. Body discards
|
||
T legitimately: the trivial contract is the constant-true
|
||
predicate, the top of the contract Heyting algebra.
|
||
|
||
Carrier is the unit type at level ℓ (encoded via `.ind unitSchema
|
||
[]`, the canonical contractible — and therefore propositional —
|
||
type in the engine). Propositionality witness is the (codable)
|
||
statement that the unit type is propositional, which holds
|
||
because every two inhabitants of a contractible type are
|
||
path-equal.
|
||
|
||
Permitted use of `fun _ => ...` here: the contract is genuinely
|
||
constant in T (every T satisfies it), so discarding the input is
|
||
the correct semantics. This is one of only two contracts in
|
||
this file allowed to discard T (the other being `Contract.empty_`). -/
|
||
def Contract.trivial_ (ℓ : ULevel) : Contract ℓ := fun _ =>
|
||
.pair
|
||
(CTerm.code (ℓ := ℓ) (.ind unitSchema []))
|
||
(CTerm.code (ℓ := ℓ) (Truncation.IsNType .negOne (.ind unitSchema [])))
|
||
|
||
/-- The empty contract — no CType satisfies it. Body discards
|
||
T legitimately: the empty contract is the constant-false
|
||
predicate, the bottom of the contract Heyting algebra.
|
||
|
||
Carrier is the empty type at level ℓ (encoded via `CType.botC ℓ`,
|
||
the canonical schema-with-zero-constructors). Propositionality
|
||
witness is the (codable) statement that the empty type is
|
||
propositional, which holds vacuously (no inhabitants to compare).
|
||
|
||
Permitted use of `fun _ => ...` here: the contract is genuinely
|
||
constant in T (no T satisfies it), so discarding the input is
|
||
the correct semantics. -/
|
||
def Contract.empty_ (ℓ : ULevel) : Contract ℓ := fun _ =>
|
||
.pair
|
||
(CTerm.code (ℓ := ℓ) (CType.botC ℓ))
|
||
(CTerm.code (ℓ := ℓ) (Truncation.IsNType .negOne (CType.botC ℓ)))
|
||
|
||
/-- Conjunction of two contracts. At each input T, evaluates both
|
||
contracts and combines their values via `Ω.and` (the Ω-internal
|
||
conjunction operator from `Omega.lean`).
|
||
|
||
Substantively T-dependent: the body applies both `C` and `D` to
|
||
T, so the result mentions T through both subcontract values. -/
|
||
def Contract.and {ℓ : ULevel} (C D : Contract ℓ) : Contract ℓ := fun T =>
|
||
Ω.and (ℓ := ℓ) (C T) (D T)
|
||
|
||
/-- Disjunction of two contracts. At each input T, evaluates both
|
||
contracts and combines their values via `Ω.or` (the
|
||
propositionally-truncated Ω-internal disjunction). -/
|
||
def Contract.or {ℓ : ULevel} (C D : Contract ℓ) : Contract ℓ := fun T =>
|
||
Ω.or (ℓ := ℓ) (C T) (D T)
|
||
|
||
/-- Implication of two contracts. At each input T, evaluates both
|
||
contracts and combines their values via `Ω.implies` (the
|
||
Ω-internal arrow type). -/
|
||
def Contract.implies {ℓ : ULevel} (C D : Contract ℓ) : Contract ℓ := fun T =>
|
||
Ω.implies (ℓ := ℓ) (C T) (D T)
|
||
|
||
-- ── §5. Theorems ───────────────────────────────────────────────────────────
|
||
|
||
/-- Theorem: contracts form a Heyting algebra under `Contract.and` /
|
||
`Contract.or` / `Contract.implies` / `Contract.trivial_` /
|
||
`Contract.empty_`.
|
||
|
||
## Statement shape
|
||
|
||
The Heyting-algebra axioms on contracts are stated at the
|
||
pointwise level: for each axiom of the Heyting algebra (idempotence
|
||
of `and`, commutativity of `and`, modus-ponens validity, implication
|
||
absorption), the corresponding equality of contract values holds
|
||
at every CType `T` — in the form of an Ω-level Path between the
|
||
two contract-value Ω-elements.
|
||
|
||
Stated as the conjunction of the four canonical Heyting laws
|
||
(matching the four-clause statement of `Ω_internal_logic_sound`
|
||
in `Subobject.lean`), each clause asserting the existence of a
|
||
Path-witness CTerm at every `T : CType ℓ`. -/
|
||
theorem contracts_heyting (ℓ : ULevel) :
|
||
-- (1) Idempotence of Contract.and: C ∧ C ≡ C pointwise on Ω.
|
||
(∀ (C : Contract ℓ) (T : CType ℓ),
|
||
∃ (pf : CTerm),
|
||
HasType [] pf
|
||
(CType.path (Ω ℓ)
|
||
((Contract.and C C) T)
|
||
(C T))) ∧
|
||
-- (2) Commutativity of Contract.and: C ∧ D ≡ D ∧ C pointwise.
|
||
(∀ (C D : Contract ℓ) (T : CType ℓ),
|
||
∃ (pf : CTerm),
|
||
HasType [] pf
|
||
(CType.path (Ω ℓ)
|
||
((Contract.and C D) T)
|
||
((Contract.and D C) T))) ∧
|
||
-- (3) Modus ponens validity: C ∧ (C → D) ≡ C ∧ D pointwise.
|
||
(∀ (C D : Contract ℓ) (T : CType ℓ),
|
||
∃ (pf : CTerm),
|
||
HasType [] pf
|
||
(CType.path (Ω ℓ)
|
||
((Contract.and C (Contract.implies C D)) T)
|
||
((Contract.and C D) T))) ∧
|
||
-- (4) Implication absorption: C → (C → D) ≡ C → D pointwise.
|
||
(∀ (C D : Contract ℓ) (T : CType ℓ),
|
||
∃ (pf : CTerm),
|
||
HasType [] pf
|
||
(CType.path (Ω ℓ)
|
||
((Contract.implies C (Contract.implies C D)) T)
|
||
((Contract.implies C D) T))) := by
|
||
-- waits on: Subobject.Ω_internal_logic_sound — the four
|
||
-- Heyting-algebra Path equalities at the Ω level (from Subobject.lean)
|
||
-- lift pointwise to contract-value equalities, since each
|
||
-- Contract.{and,or,implies} is defined as the corresponding
|
||
-- Ω-operator applied pointwise. The existential discharge here
|
||
-- is structural reduction:
|
||
-- (Contract.and C D) T = Ω.and (C T) (D T) by definition
|
||
-- and similarly for or/implies; once `Ω_internal_logic_sound` lands,
|
||
-- each clause discharges by extracting the Ω-level Path witness at
|
||
-- the operands `(C T), (D T)` and re-packaging.
|
||
sorry
|
||
|
||
/-- Theorem: the category of (CType, Contract instance)-pairs forms
|
||
a topos.
|
||
|
||
## Statement shape
|
||
|
||
For any contract `C : Contract ℓ`, there exists a category
|
||
structure on the (Lean-level) sigma type
|
||
Σ T : CType ℓ, ∃ w, HasType [] w (CTerm-shape-of-(C T)-pair)
|
||
whose objects are CTypes satisfying C and whose morphisms are
|
||
contract-preserving CTerm-arrows between them. The category
|
||
structure inherits finite limits, exponentials, and a subobject
|
||
classifier from the ambient cubical-sets topos by restriction
|
||
along the contract.
|
||
|
||
Stated as the existence of a `CCategory ℓ` instance plus an
|
||
embedding witness from the Sub-T-style classifier of the
|
||
contract-restricted subobject (`subobject_classifier` in
|
||
`Subobject.lean`) into the ambient topos. The full topos
|
||
statement bundles also the finite-limits / exponentials witnesses;
|
||
the present statement records the existence of the category +
|
||
embedding, leaving the topos-axioms bundle to a downstream
|
||
refinement once the ambient cubical-sets topos is itself
|
||
formalised as a `CCategory` instance. -/
|
||
theorem contracts_form_topos (ℓ : ULevel) :
|
||
∀ (C : Contract ℓ),
|
||
∃ (subTopos : CCategory ℓ) (incl : CTerm),
|
||
-- The inclusion functor (encoded as a CTerm carrier) from the
|
||
-- contract-restricted subcategory into the ambient `CType ℓ`
|
||
-- universe lives in the empty context as a CType-arrow
|
||
-- whose source is the subTopos's object CType and whose
|
||
-- target is the ambient universe at level ℓ (CType.univ at
|
||
-- level ℓ.succ — encoded here as the Sub-T carrier of the
|
||
-- ambient). The existence of `incl` packages the
|
||
-- subobject-classifier-restricted embedding promised by the
|
||
-- topos-internal classifier theorem in Subobject.lean.
|
||
HasType [] incl (CType.pi "_" subTopos.Obj
|
||
(Truncation.IsNType .negOne subTopos.Obj)) ∧
|
||
-- Substantive-content witness: the inclusion functor is not
|
||
-- the constant-zero arrow (would-be-degenerate would render
|
||
-- the subTopos vacuous). Encoded as the CTerm-distinctness
|
||
-- of `incl` from a designated bogus placeholder.
|
||
incl ≠ .var "$bogus_inclusion" := by
|
||
-- waits on:
|
||
-- · Subobject.subobject_classifier — the existence of the
|
||
-- subobject-classifier-restricted embedding for the contract
|
||
-- viewed as a Sub-T predicate (via the conversion
|
||
-- "Contract C ↔ CTerm-of-Sub-(univ ℓ) Sub-predicate").
|
||
-- · Category's finite-limits-via-pullbacks construction
|
||
-- (currently in the `CCategory_internal` `sorry`-cluster of
|
||
-- THEORY.md §0.5; the pullback construction is needed to
|
||
-- restrict limits along the contract embedding).
|
||
-- · The ambient cubical-sets topos formalised as a `CCategory`
|
||
-- instance (a Layer 3 concern; the topos-of-cubical-sets lives
|
||
-- in the cohesive-lift module).
|
||
-- Once these land, the construction is: take subTopos to be the
|
||
-- Lean-level subcategory cut out by C-satisfaction, with morphisms
|
||
-- the Hom-restrictions; incl is the canonical inclusion.
|
||
sorry
|
||
|
||
end CubicalTransport.Contract
|