{-# OPTIONS --without-K --exact-split --two-level #-}

--------------------------------------------------------------------------------
-- Instances of the extension type.
--
-- The proposition-indexed calculus  { A ∣ φ ▷ u }  of Zhang and of the
-- controlled-unfolding calculus (Gratzer–Sterling–Angiuli–Coquand–Birkedal),
-- also Sterling's "extent" types.  Remark 3.3.
--
-- This is `Ext` specialised to the strict injection  φ → 1  of a strict
-- proposition φ into the (exo) terminal object.  Instantiating the general
-- extension type at this cofibration and a constant family recovers, on the
-- nose, the strict-fibre formula
--
--        { A ∣ φ ▷ u }  =  Σ (x : A). Π (p : φ). x =ˢ u p ,
--
-- and the rules of [Zhang, Fig. 2.1] (inS / outS / bdry / β) together with the
-- η-rule become instances of the RS Fig. 4 rules from `Extension.Core`.
--------------------------------------------------------------------------------

module Extension.Instances where

open import Extension.Prelude
open import Extension.Core

private
  variable
    ℓφ ℓA : Level

module _ (φ : UUᵉ ℓφ) (A : UUᵉ ℓA) (u : φ → A) where

  -- The unique (strict) map  φ → 1  is the cofibration we extend along.
  private
    ! : φ → ⊤ᵉ {ℓφ}
    ! _ = starᵉ

  -- { A ∣ φ ▷ u }  as an extension type along  φ → 1,  with A the
  -- constant family and u the partial element.
  PropExt : UUᵉ (ℓφ ⊔ ℓA)
  PropExt = Ext ! (λ _ → A) u

  -- The pointwise strict-fibre formula of the paper.
  PropExt-direct : UUᵉ (ℓφ ⊔ ℓA)
  PropExt-direct = Σᵉ A (λ x → (p : φ) → x =ᵉ u p)

  ------------------------------------------------------------------------------
  -- Zhang's rules on the pointwise formula (Fig. 2.1 + Ex. 2.6 for η).
  ------------------------------------------------------------------------------

  -- (intro)  v with a strict proof that it equals u under φ.
  inS : (v : A) → ((p : φ) → v =ᵉ u p) → PropExt-direct
  inS v e = v ,ᵉ e

  -- (elim)
  outS : PropExt-direct → A
  outS = pr1ᵉ

  -- (bdry)  outS agrees strictly with u whenever φ holds.
  bdryP : (w : PropExt-direct) (p : φ) → outS w =ᵉ u p
  bdryP = pr2ᵉ

  -- (β) and (η), both strict, in fact definitional.
  βP : (v : A) (e : (p : φ) → v =ᵉ u p) → outS (inS v e) =ᵉ v
  βP v e = reflᵉ

  ηP : (w : PropExt-direct) → w =ᵉ inS (outS w) (bdryP w)
  ηP w = reflᵉ

  ------------------------------------------------------------------------------
  -- The instance really is the paper's formula:  PropExt ≅ PropExt-direct.
  -- (Uses that the exo terminal 1 = ⊤ᵉ has definitional η, so f ≡ λ_. f ⋆.)
  ------------------------------------------------------------------------------

  private
    to : PropExt → PropExt-direct
    to (f ,ᵉ q) = f starᵉ ,ᵉ happlyᵉ q

    from : PropExt-direct → PropExt
    from (x ,ᵉ e) = (λ _ → x) ,ᵉ funextᵉ e

    from-to : (w : PropExt) → from (to w) =ᵉ w
    from-to (f ,ᵉ q) = ext-≡ reflᵉ

    to-from : (w : PropExt-direct) → to (from w) =ᵉ w
    to-from (x ,ᵉ e) = dep-pair-=ᵉ _ _ (reflᵉ ,ᵉ funextᵉ (λ p → UIPᵉ _ _))

  PropExt≅direct : PropExt ≅ PropExt-direct
  PropExt≅direct = to ,ᵉ (from ,ᵉ (from-to ,ᵉ to-from))

  record PropExtCalculus : UUᵉ (ℓφ ⊔ ℓA) where
    field
      presentation : PropExt ≅ PropExt-direct
      intro : (v : A) → ((p : φ) → v =ᵉ u p) → PropExt-direct
      elim : PropExt-direct → A
      boundary : (w : PropExt-direct) (p : φ) → elim w =ᵉ u p
      beta : (v : A) (e : (p : φ) → v =ᵉ u p)
        → elim (intro v e) =ᵉ v
      eta : (w : PropExt-direct)
        → w =ᵉ intro (elim w) (boundary w)

  prop-ext-calculus : PropExtCalculus
  prop-ext-calculus = record
    { presentation = PropExt≅direct
    ; intro = inS
    ; elim = outS
    ; boundary = bdryP
    ; beta = βP
    ; eta = ηP
    }

--------------------------------------------------------------------------------
-- Every extension type is a product, fibrewise over the codomain, of extension
-- types along maps into 1: over ψ the index is the strict fibre of i and the
-- partial element is the boundary datum transported into it.  The index is a
-- type, not in general a proposition, as in the several-clauses case above.
--------------------------------------------------------------------------------

private
  variable
    ℓΦ ℓΨ : Level

-- The strict fibre of i over ψ: "ψ lies in the image of i".
im : {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) → Ψ → UUᵉ (ℓΦ ⊔ ℓΨ)
im {Φ = Φ} i ψ = Σᵉ Φ (λ φ → i φ =ᵉ ψ)

-- The indices are strict propositions exactly when i is injective.  Subshape
-- inclusions and the extents of face formulas are; being a cofibration does not
-- make a map injective.
im-is-prop : {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ)
           → ((φ φ' : Φ) → i φ =ᵉ i φ' → φ =ᵉ φ')
           → (ψ : Ψ) (z z' : im i ψ) → z =ᵉ z'
im-is-prop i inj _ (φ ,ᵉ reflᵉ) (φ' ,ᵉ p') =
  dep-pair-=ᵉ _ _ (exo-inv (inj φ' φ p') ,ᵉ UIPᵉ _ _)

module _ {ℓA : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ}
         (i : Φ → Ψ) (A : Ψ → UUᵉ ℓA) (a : (φ : Φ) → A (i φ)) where

  -- The boundary datum, transported into the fibre over ψ.
  im-bdry : (ψ : Ψ) → im i ψ → A ψ
  im-bdry ψ (φ ,ᵉ p) = exo-tr A p (a φ)

  private
    key : (s : (ψ : Ψ) → A ψ) → restrict i s =ᵉ a
        → (ψ : Ψ) (z : im i ψ) → s ψ =ᵉ im-bdry ψ z
    key s e _ (φ ,ᵉ reflᵉ) = happlyᵉ e φ

    to : Ext i A a → ((ψ : Ψ) → PropExt-direct (im i ψ) (A ψ) (im-bdry ψ))
    to (s ,ᵉ e) ψ = s ψ ,ᵉ key s e ψ

    from : ((ψ : Ψ) → PropExt-direct (im i ψ) (A ψ) (im-bdry ψ)) → Ext i A a
    from t = (λ ψ → pr1ᵉ (t ψ)) ,ᵉ funextᵉ (λ φ → pr2ᵉ (t (i φ)) (φ ,ᵉ reflᵉ))

    from-to : (w : Ext i A a) → from (to w) =ᵉ w
    from-to w = ext-≡ reflᵉ

    to-from : (t : (ψ : Ψ) → PropExt-direct (im i ψ) (A ψ) (im-bdry ψ))
            → to (from t) =ᵉ t
    to-from t = funextᵉ (λ ψ → dep-pair-=ᵉ _ _ (reflᵉ ,ᵉ funextᵉ (λ z → UIPᵉ _ _)))

  fibrewise-decomposition
    : Ext i A a ≅ ((ψ : Ψ) → PropExt-direct (im i ψ) (A ψ) (im-bdry ψ))
  fibrewise-decomposition = to ,ᵉ (from ,ᵉ (from-to ,ᵉ to-from))

{- References:

  [Zhang]      Tesla Zhang.  Three non-cubical applications of extension types.
               arXiv:2311.05658, 2023.

  [Sterling]   Jonathan Sterling.  First steps in synthetic Tait computability: the
               objective metatheory of cubical type theory.  PhD thesis, Carnegie
               Mellon University, 2021 (CMU-CS-21-142).
               Jonathan Sterling and Robert Harper.  Logical relations as types:
               proof-relevant parametricity for program modules.  Journal of the ACM
               68(6):1-47, 2021.  doi:10.1145/3474834

  [Gratzer et al.]
               Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand and
               Lars Birkedal.  Controlling unfolding in type theory.  Mathematical
               Structures in Computer Science 35:e38, 2025.
               doi:10.1017/S0960129525100327

  [RS]         Emily Riehl and Michael Shulman.  A type theory for synthetic
               ∞-categories.  Higher Structures 1(1):147-224, 2017.
               doi:10.21136/hs.2017.06

-}