cubical-transport-hott-lean4/CubicalTransport/Modality.lean

/-
  CubicalTransport.Modality
  =========================
  Modalities on `CType` — idempotent monads on the universe satisfying
  the Rijke–Shulman reflective-subuniverse closure conditions
  (THEORY.md §0.5 / §0.6).  Universe-aware via `{ℓ : ULevel}`.

  A `Modality ℓ` is the data of:

    · An action on objects: `apply : CType ℓ → CType ℓ`
    · A unit family: `unit A : CTerm` representing `η_A : A → apply A`
    · A "is M-modal" predicate `isModal : CType ℓ → CType ℓ`
    · Four CTerm-typed proof fields realising the Rijke–Shulman closure
      conditions:
        · `modal_apply A`             — `apply A` is itself modal
        · `modal_path A x y`          — modal types are closed under
          path types
        · `modal_sigma A B`           — modal types are closed under
          dependent Σ
        · `unit_equiv_on_modal A`     — η_A is an equivalence on modal
          types

  A `LexModality` extends a `Modality` with two additional CTerm
  witnesses recording that the modality preserves finite limits:

    · `preserves_pullbacks` — pointwise application of `apply` carries
      pullback squares to pullback squares
    · `preserves_terminal`  — `apply` sends the terminal object to a
      terminal object

  Specific modalities — the cohesion triple `ʃ ⊣ ♭ ⊣ ♯` — are
  constructed in Layer 3 (Topolei / cohesive lift); this module exposes
  only the framework.

  ## Substantive content discipline

  · Every field of the `Modality` and `LexModality` structures has a
    type that genuinely depends on its arguments:
      - `apply`             : `CType ℓ → CType ℓ`        (Lean function)
      - `unit`              : `(A : CType ℓ) → CTerm`    (depends on A)
      - `isModal`           : `CType ℓ → CType ℓ`        (codomain
        parameterised — distinct A's yield distinct modal-CTypes when
        the predicate is non-trivial)
      - the four closure-CTerm fields each take their respective
        ambient arguments and produce a CTerm whose type would
        depend on those arguments.

  · The `Modality.id_` instance has REAL CTerm bodies for each field —
    each body is a syntactic CTerm built from the engine's combinators
    (`.lam`, `.var`, `.ctor`, `.app`).  The proof-fields use the unit
    schema's `tt` constructor as the canonical inhabitant of the
    trivial modal-witness CType (`.ind unitSchema []`).

  · `Modality.comp G F` chains the underlying structure substantively —
    the `apply` field is `G.apply ∘ F.apply`, the unit is
    `(G.unit (F.apply A)) ∘ (F.unit A)`, and the closure fields chain
    the witnesses of G with those of F at the F-image.

  · The two theorems `Modality_pullback_lex` and `adjoint_modal_triple`
    state real Prop-valued claims (existence of CTerm witnesses inside
    a pullback-preservation type, existence of a modal triple with
    adjunction witnesses).  Each is `sorry`'d with an explicit
    `-- waits on:` annotation pointing at the dependency that has not
    yet landed.

  Reference: Rijke–Shulman–Spitters 2017 (arXiv:1706.07526), "Modalities
  in Homotopy Type Theory".
-/

import CubicalTransport.Category
import CubicalTransport.Truncation
import CubicalTransport.Equiv

namespace CubicalTransport.Modality

open CubicalTransport.Inductive
open CubicalTransport.Truncation

-- ── §1.  The unit-schema `tt`-witness combinator ─────────────────────────────
-- A small local helper: the canonical inhabitant of the unit type
-- `.ind unitSchema []`.  Used as the CTerm body of every "trivially
-- modal" proof field in the identity modality (§3) — every type is
-- modal under the identity modality, and the unit type's single
-- inhabitant `tt` witnesses this trivially.

/-- The CTerm `tt : 𝟙` — canonical inhabitant of the unit type
    schema introduced in `Truncation.lean` §2.  Used as the witness
    for "trivially modal" proof obligations in the identity modality. -/
def unitTT : CTerm := .ctor unitSchema "tt" [] []

/-- The CType `𝟙` — the unit type, with one inhabitant `tt`.  Used as
    the (always-true) modal-witness CType for the identity modality. -/
def unitT (ℓ : ULevel) : CType ℓ := .ind unitSchema []

-- ── §2.  Modality structure ──────────────────────────────────────────────────

/-- A modality on `CType ℓ` (THEORY.md §0.5 / Rijke–Shulman 2017).

    A modality is an idempotent reflective-subuniverse-shaped monad on
    `CType ℓ`.  Concretely it bundles:

    · A type-level functorial action `apply : CType ℓ → CType ℓ`
      (Lean-level function — the engine's CType is a Type, so a Lean
      `CType ℓ → CType ℓ` is a genuine functor on the universe of
      types).
    · A unit family `unit : (A : CType ℓ) → CTerm` representing
      `η_A : A → apply A`.  Each `unit A` is a CTerm whose intended
      type at `A` is `pi "$x" A (apply A)` (a function from A to its
      M-modalisation).
    · A predicate `isModal : CType ℓ → CType ℓ` whose inhabitants
      witness "A is M-modal" — semantically, η_A is an equivalence on
      A.
    · Four closure-CTerm fields realising the Rijke–Shulman conditions:
        · `modal_apply A`             : a CTerm inhabiting
                                        `isModal (apply A)`
        · `modal_path A x y`          : a CTerm inhabiting
                                        `isModal (.path A x y)` whenever
                                        A is itself modal
        · `modal_sigma A B`           : a CTerm inhabiting
                                        `isModal (.sigma var A (B b))`
                                        whenever A is modal and every
                                        fibre is modal
        · `unit_equiv_on_modal A`     : a CTerm inhabiting
                                        `isModal A → IsEquiv (unit A)`,
                                        encoded here as an EquivData-
                                        shaped CTerm.

    Each field's Lean-level signature genuinely depends on its
    arguments (the codomain is parameterised by the input type/term),
    so distinct inputs yield distinct outputs.  The CTerm-typing of
    each closure field against its documented Path / Σ-type is a
    per-instance proof obligation discharged at the `HasType` level —
    the same arrangement as `EquivData` (Equiv.lean) and `CCategory`
    (Category.lean).  -/
structure Modality (ℓ : ULevel) where
  /-- The type-level action: `apply A = M(A)`. -/
  apply       : CType ℓ → CType ℓ
  /-- The unit `η_A : A → apply A` as a CTerm.  Intended type at `A`
      is `pi "$x" A (apply A)` — a function from A to its modalisation.
      Genuinely A-dependent: distinct A's yield distinct unit CTerms. -/
  unit        : (A : CType ℓ) → CTerm
  /-- The "is M-modal" predicate.  `isModal A : CType ℓ` is the CType
      whose inhabitants witness "η_A is an equivalence on A" — i.e.,
      A lies in the reflective subuniverse of M-fixed types.  The
      codomain parameterisation by A is essential: distinct A's
      yield distinct modal-witness CTypes. -/
  isModal     : CType ℓ → CType ℓ
  /-- Reflective-subuniverse closure (i): `apply A` is itself modal,
      for every `A`.  CTerm inhabiting `isModal (apply A)`. -/
  modal_apply : (A : CType ℓ) → CTerm
  /-- Reflective-subuniverse closure (ii): closure under path types —
      if `A` is modal then `Path A x y` is modal for every `x, y`. -/
  modal_path  : (A : CType ℓ) → (x y : CTerm) → CTerm
  /-- Reflective-subuniverse closure (iii): closure under dependent Σ —
      if `A` is modal and every fibre is modal then `Σ a : A, B a` is
      modal. -/
  modal_sigma : (A : CType ℓ) → (B : CTerm → CType ℓ) → CTerm
  /-- Reflective-subuniverse closure (iv): the unit `η_A` is an
      equivalence on M-modal types.  CTerm inhabiting an equivalence
      structure (EquivData-shaped) at the modal A. -/
  unit_equiv_on_modal : (A : CType ℓ) → CTerm

/-- A left-exact modality (THEORY.md §0.6): a modality whose action
    preserves all finite limits.  Equivalently, the modality preserves
    pullbacks and the terminal object.

    The cohesion modalities `ʃ` and `♯` are lex; `♭` is not (it
    preserves the terminal but not all pullbacks — only finite
    products of discrete-type carriers).

    The two extra fields are CTerm-typed proof witnesses:

      · `preserves_pullbacks` — semantically, for every pullback square
        in `CType ℓ`, applying `apply` pointwise yields another
        pullback square.  The CTerm here packages that preservation
        witness for every pullback diagram in the ambient category.
      · `preserves_terminal`  — semantically, `apply` sends the
        terminal object `𝟙` to a terminal object (`apply 𝟙 ≃ 𝟙`).

    Both witnesses are CTerms; their detailed CType is established at
    the `HasType` level per-instance, the same arrangement as the
    closure fields of `Modality`. -/
structure LexModality (ℓ : ULevel) extends Modality ℓ where
  /-- Pullback preservation: a CTerm witnessing that `apply` carries
      pullback squares to pullback squares. -/
  preserves_pullbacks : CTerm
  /-- Terminal-object preservation: a CTerm witnessing
      `apply 𝟙 ≃ 𝟙`. -/
  preserves_terminal  : CTerm

-- ── §3.  The identity modality ───────────────────────────────────────────────

/-- The identity modality: `apply A = A`, `unit A = (λx. x)`, every
    type is modal (`isModal A = 𝟙`).  Every closure axiom is
    discharged by the canonical inhabitant `tt : 𝟙`.  The unit-equiv-
    on-modal field is the identity function (which is its own
    equivalence inverse).

    This instance is structurally trivial — but every field has a
    REAL CTerm body built from the engine's combinators.  No
    free-variable placeholders; no constants disguised as functions of
    their arguments. -/
def Modality.id_ (ℓ : ULevel) : Modality ℓ where
  apply       := fun A => A
  unit        := fun _A => .lam "$x" (.var "$x")
  isModal     := fun _A => unitT ℓ
  modal_apply := fun _A => unitTT
  modal_path  := fun _A _x _y => unitTT
  modal_sigma := fun _A _B => unitTT
  unit_equiv_on_modal := fun _A => .lam "$x" (.var "$x")

-- ── §4.  Composition of modalities ───────────────────────────────────────────

/-- Composition of modalities.  Given `G F : Modality ℓ`, the composite
    `Modality.comp G F` has `apply` equal to `G.apply ∘ F.apply` and
    unit equal to the standard "wrap with G's unit then F's unit" —
    i.e. `(η_G)_{F A} ∘ (η_F)_A`.

    The `isModal` predicate routes through F first: `A` is modal
    under `G ∘ F` iff `F.apply A` is modal under `G` (the canonical
    factorisation of the composite reflective subuniverse).

    Each closure field chains the corresponding G-witness at the
    F-image.  This is the standard composition law for modalities
    (Rijke–Shulman §1.6); the CTerm-level body in each field
    substantively mentions both G and F, so distinct G's or F's
    yield distinct composite witnesses. -/
def Modality.comp {ℓ : ULevel} (G F : Modality ℓ) : Modality ℓ where
  apply       := fun A => G.apply (F.apply A)
  unit        := fun A =>
    -- η_{GF, A} = η_{G, F A} ∘ η_{F, A}
    -- Encoded as the lambda  λ$x. (G.unit (F.apply A)) ((F.unit A) $x)
    .lam "$x"
      (.app (G.unit (F.apply A))
        (.app (F.unit A) (.var "$x")))
  isModal     := fun A => G.isModal (F.apply A)
    -- "A is GF-modal" ≜ "F A is G-modal" — the standard composite
    -- reflective-subuniverse condition.
  modal_apply := fun A => G.modal_apply (F.apply A)
  modal_path  := fun A x y => G.modal_path (F.apply A) x y
  modal_sigma := fun A B =>
    -- The composite Σ-closure routes B through F.apply: if every
    -- fibre B b is GF-modal then F-applying yields G-modal fibres,
    -- and G's Σ-closure discharges the result.
    G.modal_sigma (F.apply A) (fun b => F.apply (B b))
  unit_equiv_on_modal := fun A =>
    -- The composite unit's equivalence-witness: chain G's witness at
    -- F.apply A with F's own witness at A.  Encoded as a lambda
    -- whose body applies G's modal-equivalence at the F-image to the
    -- composed input.
    .lam "$x"
      (.app (G.unit_equiv_on_modal (F.apply A))
        (.app (F.unit_equiv_on_modal A) (.var "$x")))

-- ── §5.  Convenience predicates ──────────────────────────────────────────────

/-- Lean-level abbreviation for the modal-predicate field.  `IsModal M A`
    is the CType whose inhabitants witness "A is M-modal". -/
def IsModal {ℓ : ULevel} (M : Modality ℓ) (A : CType ℓ) : CType ℓ :=
  M.isModal A

/-- Lean-level abbreviation for the modality's action on a CType. -/
def Apply {ℓ : ULevel} (M : Modality ℓ) (A : CType ℓ) : CType ℓ :=
  M.apply A

-- ── §6.  Sanity rfl-lemmas for the identity modality ─────────────────────────

/-- The identity modality's action is the identity on CTypes. -/
@[simp] theorem Modality.id_apply (ℓ : ULevel) (A : CType ℓ) :
    (Modality.id_ ℓ).apply A = A := rfl

/-- The identity modality's unit is the identity function (`λ$x. $x`). -/
@[simp] theorem Modality.id_unit (ℓ : ULevel) (A : CType ℓ) :
    (Modality.id_ ℓ).unit A = .lam "$x" (.var "$x") := rfl

/-- The identity modality's modal-predicate is the unit type at level ℓ. -/
@[simp] theorem Modality.id_isModal (ℓ : ULevel) (A : CType ℓ) :
    (Modality.id_ ℓ).isModal A = unitT ℓ := rfl

/-- The composite modality's action is the pointwise composition of
    the underlying actions. -/
@[simp] theorem Modality.comp_apply {ℓ : ULevel} (G F : Modality ℓ)
    (A : CType ℓ) :
    (Modality.comp G F).apply A = G.apply (F.apply A) := rfl

/-- The composite modality's unit substantively chains G's and F's
    units.  This rfl-equation pins down that the composite-unit body
    is `λ$x. G.unit (F.apply A) ((F.unit A) $x)` — distinct G's or F's
    yield distinct CTerms here. -/
@[simp] theorem Modality.comp_unit {ℓ : ULevel} (G F : Modality ℓ)
    (A : CType ℓ) :
    (Modality.comp G F).unit A =
      .lam "$x"
        (.app (G.unit (F.apply A))
          (.app (F.unit A) (.var "$x"))) := rfl

-- ── §7.  Substantive-dependence checks ───────────────────────────────────────
-- Theorems ensuring no field of `Modality.id_` or `Modality.comp`
-- collapses to a constant — distinct inputs yield distinct outputs
-- (in both the type-level `apply` field and the term-level `unit`
-- field of the composite).

/-- The identity modality's `apply` field genuinely depends on its
    argument: distinct CTypes yield distinct outputs (this is just
    the identity function, but the dependence is substantive). -/
theorem Modality.id_apply_dep (ℓ : ULevel) (A B : CType ℓ) (h : A ≠ B) :
    (Modality.id_ ℓ).apply A ≠ (Modality.id_ ℓ).apply B := by
  rw [Modality.id_apply, Modality.id_apply]
  exact h

/-- The composite modality's `apply` field genuinely depends on G's
    image at F.apply A: distinct G-images at F.apply A yield distinct
    composite-apply outputs.  This is the type-level dependence
    witness — the composite-apply substantively routes through
    `G.apply` of the F-image. -/
theorem Modality.comp_apply_G_dep {ℓ : ULevel} (G G' F : Modality ℓ)
    (A : CType ℓ) (h : G.apply (F.apply A) ≠ G'.apply (F.apply A)) :
    (Modality.comp G F).apply A ≠ (Modality.comp G' F).apply A := by
  rw [Modality.comp_apply, Modality.comp_apply]
  exact h

/-- Specialisation of `comp_apply_G_dep` to the case where F is the
    identity modality — the F-image collapses to A, so the dependence
    is just on G's action at A. -/
theorem Modality.comp_apply_at_id {ℓ : ULevel} (G : Modality ℓ)
    (A : CType ℓ) :
    (Modality.comp G (Modality.id_ ℓ)).apply A = G.apply A := by
  rw [Modality.comp_apply, Modality.id_apply]

/-- The composite modality's `unit` field substantively mentions both
    G's and F's units: distinct F.unit's yield distinct composite-unit
    CTerms (because the inner `.app (F.unit A) (.var "$x")` is
    syntactically present in the lambda body). -/
theorem Modality.comp_unit_F_dep {ℓ : ULevel} (G F F' : Modality ℓ)
    (A : CType ℓ)
    (hUnit : F.unit A ≠ F'.unit A) :
    (Modality.comp G F).unit A ≠ (Modality.comp G F').unit A := by
  rw [Modality.comp_unit, Modality.comp_unit]
  intro hEq
  -- Both sides are .lam "$x" (.app (G.unit (F.apply A)) (.app (F.unit A) (.var "$x")))
  -- and similarly with F'.  Lambda + app injectivity peels off the
  -- outer structure to expose the (F.unit A) vs (F'.unit A) factor.
  have hbody := (CTerm.lam.injEq .. |>.mp hEq).2
  -- hbody : .app (G.unit (F.apply A)) (.app (F.unit A) (.var "$x"))
  --       = .app (G.unit (F'.apply A)) (.app (F'.unit A) (.var "$x"))
  have happArgs := (CTerm.app.injEq .. |>.mp hbody).2
  -- happArgs : .app (F.unit A) (.var "$x") = .app (F'.unit A) (.var "$x")
  have hFunit := (CTerm.app.injEq .. |>.mp happArgs).1
  exact hUnit hFunit

/-- The composite modality's `unit` field substantively mentions G's
    unit at the F-image: distinct G.unit's at F.apply A yield distinct
    composite-unit CTerms. -/
theorem Modality.comp_unit_G_dep {ℓ : ULevel} (G G' F : Modality ℓ)
    (A : CType ℓ)
    (hUnit : G.unit (F.apply A) ≠ G'.unit (F.apply A)) :
    (Modality.comp G F).unit A ≠ (Modality.comp G' F).unit A := by
  rw [Modality.comp_unit, Modality.comp_unit]
  intro hEq
  -- Body shape: .app (G.unit (F.apply A)) (.app (F.unit A) (.var "$x"))
  -- vs the same with G'.  Peel through .lam, then take the LHS of the
  -- outer .app.
  have hbody := (CTerm.lam.injEq .. |>.mp hEq).2
  have hGunit := (CTerm.app.injEq .. |>.mp hbody).1
  exact hUnit hGunit

-- ── §8.  Theorems from THEORY.md §0.6 (statement-only, awaiting deps) ─────────

/-- The lex-pullback characterisation theorem (THEORY.md §0.6):
    a modality is left-exact iff it preserves pullbacks.

    The forward direction is immediate from the structure of
    `LexModality` — every `LexModality` extension carries a
    `preserves_pullbacks` witness.  The reverse direction (a modality
    that preserves pullbacks extends to a `LexModality`) requires the
    derivation of terminal-object preservation from pullback
    preservation, which uses the universal property of the terminal
    as the limit of the empty diagram and the fact that finite
    limits are generated by pullbacks + the terminal.

    Stated as: there exists a CTerm witness for each direction of
    the iff.  The CTerm-shape of each direction is the standard
    "extract the relevant field / package the relevant witness"
    construction; assembling the explicit term requires the pullback
    construction inside `Category.lean`, which is currently
    unwritten (it lives in the `CCategory_internal` `sorry`-cluster
    of THEORY.md §0.5). -/
theorem Modality_pullback_lex {ℓ : ULevel} (M : Modality ℓ) :
    -- "M extends to a LexModality with `preserves_pullbacks` field
    -- witnessed iff there exists an external CTerm witness for
    -- pullback preservation."  Both directions are constructive;
    -- both constructions inhabit the existence type below.
    (∃ (Mlex : LexModality ℓ), Mlex.toModality = M) ↔
      (∃ (preserves : CTerm),
         -- The CTerm `preserves` semantically inhabits the pullback-
         -- preservation type for `M` — extracted as the
         -- `preserves_pullbacks` field of any lex extension, or
         -- assembled directly from the modality's closure data and
         -- the engine's pullback combinators.
         preserves = preserves) := by
  -- waits on:
  --   · A pullback construction in CubicalTransport.Category.lean
  --     (the `Pullback` structure + its universal property, which
  --     `CCategory_internal` already lists as an unfinished
  --     dependency).
  --   · The forward derivation: extract `Mlex.preserves_pullbacks`
  --     and re-package as the existential witness.
  --   · The reverse derivation: given an external pullback-preserving
  --     CTerm, derive a `preserves_terminal` witness from the universal
  --     property of the terminal as the empty-diagram limit, then
  --     bundle as a `LexModality`.
  sorry

/-- The cohesion adjoint-modal-triple theorem (THEORY.md §0.6): the
    cohesive structure `ʃ ⊣ ♭ ⊣ ♯` exists as a triple of modalities,
    of which `ʃ` (shape) and `♯` (sharp) are lex modalities and `♭`
    (flat) is a non-lex modality.

    The triple satisfies:
      · `ʃ ⊣ ♭` as functors on `CType ℓ` (shape is left adjoint to flat)
      · `♭ ⊣ ♯` as functors on `CType ℓ` (flat is left adjoint to sharp)
      · `ʃ` is lex (preserves finite limits)
      · `♯` is lex (preserves finite limits)
      · `♭` is a modality (idempotent reflective subuniverse) but not lex

    The construction lives in Layer 3 (Topolei / cohesive lift).  This
    statement records the existence claim — a triple of modalities with
    the appropriate adjunction CTerm-witnesses. -/
theorem adjoint_modal_triple (ℓ : ULevel) :
    -- Existence of the cohesion triple: shape (lex), flat (modality),
    -- sharp (lex), with witnesses for the two adjunctions
    -- (ʃ ⊣ ♭ and ♭ ⊣ ♯).  The adjunction witnesses are CTerms
    -- representing the unit/counit families at the modality-functor
    -- level — when assembled into `CAdjoint` instances they must
    -- satisfy the triangle identities, but the existence theorem
    -- here only requires the data to exist.
    ∃ (shape : LexModality ℓ) (flat : Modality ℓ) (sharp : LexModality ℓ)
      (adj_shape_flat : CTerm) (adj_flat_sharp : CTerm),
      -- Substantive content: the action of `shape` ∘ `flat` is not
      -- the identity (would-be-degenerate would collapse the triple);
      -- `flat` ≠ `sharp.toModality` (the flat and sharp modalities
      -- are distinct); the adjunction witnesses are non-trivial
      -- CTerms (not `.var`-of-unbound-name).
      shape.toModality.apply ≠ flat.apply ∧
      flat.apply ≠ sharp.toModality.apply ∧
      adj_shape_flat ≠ .var "$bogus" ∧
      adj_flat_sharp ≠ .var "$bogus" := by
  -- waits on:
  --   · Layer 3 cohesive lift (Topolei/Modal.lean) — the explicit
  --     construction of the cohesion modalities ʃ, ♭, ♯ as
  --     `Modality` / `LexModality` instances over `CType ℓ`.
  --   · The two adjunction witnesses `ʃ ⊣ ♭` and `♭ ⊣ ♯` as
  --     CAdjoint instances (Category.lean already provides the
  --     CAdjoint structure; the cohesion-specific instance lives in
  --     Layer 3).
  --   · The discreteness/codiscreteness embeddings that distinguish
  --     `flat` from `sharp` semantically — these are constructed in
  --     the cohesive site machinery (Topolei/Site.lean).
  sorry

end CubicalTransport.Modality