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

--------------------------------------------------------------------------------
-- The extension type and its rules (Riehl–Shulman, Fig. 4).
--
-- Definition 3.1 and Lemma 3.2.
--
-- An (abstract) 2LTT cofibration is just an exo-map  i : Φ → Ψ.  The extension
-- type of a family  A : Ψ → UUᵉ  along  i,  with boundary datum
-- a : Πφ. A (i φ),  is the *strict fibre* of the restriction map
--
--        i* : (Πψ. A ψ) → (Πφ. A (i φ)),   f ↦ f ∘ i
--
-- over  a.  The whole point of the paper is that this is *definable* in 2LTT and
-- that all the RS rules are theorems with the boundary holding *strictly*.
--
-- We work with a general exo family  A : Ψ → UUᵉ.  The paper states everything
-- for a fibrant family  A₀ : Ψ → UU;  that is the special case  A ≔ λ ψ. C (A₀ ψ)
-- (with  a ≔ λ φ. c (a₀ φ)),  obtained by the coercion  C.  Stating the rules at
-- the exo level makes precise that nothing here uses fibrancy or cofibrancy:
-- the definition and all six rules (form / intro / eval / bdry / β / η) are pure
-- strict-fibre facts, and β, η even hold definitionally (they are `reflᵉ`).
--------------------------------------------------------------------------------

module Extension.Core where

open import Extension.Prelude

private
  variable
    ℓΦ ℓΨ ℓA : Level

--------------------------------------------------------------------------------
-- Restriction along a cofibration and the extension type.
--------------------------------------------------------------------------------

-- Restriction  f ↦ f ∘ i  of a total section to the subshape.
restrict : {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) {A : Ψ → UUᵉ ℓA}
         → ((ψ : Ψ) → A ψ) → ((φ : Φ) → A (i φ))
restrict i f φ = f (i φ)

-- Strict contractibility (a centre with a strict contraction).  The strict/exo
-- analogue of `is-contr`.
is-contrᵉ : {ℓ : Level} → UUᵉ ℓ → UUᵉ ℓ
is-contrᵉ X = Σᵉ X (λ x₀ → (x : X) → x₀ =ᵉ x)

-- Definition 3.1:  Extᵢ(A , a) ≔ Σ (f : Πψ.A ψ). (f ∘ i =ˢ a).
Ext : {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ}
    → (i : Φ → Ψ) (A : Ψ → UUᵉ ℓA) (a : (φ : Φ) → A (i φ))
    → UUᵉ (ℓΦ ⊔ ℓΨ ⊔ ℓA)
Ext i A a = Σᵉ ((ψ : _) → A ψ) (λ f → restrict i f =ᵉ a)

--------------------------------------------------------------------------------
-- The rules of RS Fig. 4 (Lemma 3.2).
--------------------------------------------------------------------------------

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

  -- (form) is the definition of `Ext` above.

  -- (intro)  a total section that strictly restricts to `a` gives an element.
  ext-λ : (b : (ψ : Ψ) → A ψ) → restrict i b =ᵉ a → Ext i A a
  ext-λ b p = b ,ᵉ p

  -- (eval)  an element evaluates like a (dependent) function on all of Ψ.
  ext-app : Ext i A a → (ψ : Ψ) → A ψ
  ext-app f ψ = pr1ᵉ f ψ

  -- (bdry)  on the subshape the evaluation *strictly* equals the datum `a`.
  ext-bdry : (f : Ext i A a) (φ : Φ) → ext-app f (i φ) =ᵉ a φ
  ext-bdry f = happlyᵉ (pr2ᵉ f)

  -- (β)  holds strictly, in fact definitionally.
  ext-β : (b : (ψ : Ψ) → A ψ) (p : restrict i b =ᵉ a) (ψ : Ψ)
        → ext-app (ext-λ b p) ψ =ᵉ b ψ
  ext-β b p ψ = reflᵉ

  -- (η)  holds strictly, in fact definitionally.
  ext-η : (f : Ext i A a) → f =ᵉ ext-λ (λ ψ → ext-app f ψ) (pr2ᵉ f)
  ext-η f = reflᵉ

  -- Extensionality of the *encoding*: two extensions with strictly equal
  -- underlying sections are strictly equal (the boundary witness is a strict
  -- proposition by UIPᵉ).  Used pervasively for the RS iso lemmas.
  ext-≡ : {f g : Ext i A a} → pr1ᵉ f =ᵉ pr1ᵉ g → f =ᵉ g
  ext-≡ {f} {g} q = dep-pair-=ᵉ f g (q ,ᵉ UIPᵉ _ _)

record ExtensionRules
    {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ}
    (i : Φ → Ψ) (A : Ψ → UUᵉ ℓA) (a : (φ : Φ) → A (i φ))
    : UUᵉ (ℓΦ ⊔ ℓΨ ⊔ ℓA) where
  field
    intro : (b : (ψ : Ψ) → A ψ) → restrict i b =ᵉ a → Ext i A a
    eval : Ext i A a → (ψ : Ψ) → A ψ
    bdry : (f : Ext i A a) (φ : Φ) → eval f (i φ) =ᵉ a φ
    β : (b : (ψ : Ψ) → A ψ) (p : restrict i b =ᵉ a) (ψ : Ψ)
      → eval (intro b p) ψ =ᵉ b ψ
    η : (f : Ext i A a)
      → f =ᵉ intro (λ ψ → eval f ψ) (funextᵉ (bdry f))

extension-rules :
    {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ}
    {i : Φ → Ψ} {A : Ψ → UUᵉ ℓA} {a : (φ : Φ) → A (i φ)}
  → ExtensionRules i A a
extension-rules = record
  { intro = ext-λ
  ; eval = ext-app
  ; bdry = ext-bdry
  ; β = ext-β
  ; η = λ f → ext-≡ reflᵉ
  }

--------------------------------------------------------------------------------
-- A transport helper used for the iterated-extension iso lemmas (RS 4.3, 4.4).
-- Transporting in a Σᵉ-family whose first component is constant does not move
-- the first projection.
--------------------------------------------------------------------------------

pr1ᵉ-exo-tr-const :
    {ℓ ℓ' ℓ'' : Level} {X : UUᵉ ℓ} {B : UUᵉ ℓ'} {Cf : X → B → UUᵉ ℓ''}
    {x y : X} (e : x =ᵉ y) (w : Σᵉ B (Cf x))
  → pr1ᵉ (exo-tr (λ z → Σᵉ B (Cf z)) e w) =ᵉ pr1ᵉ w
pr1ᵉ-exo-tr-const reflᵉ w = reflᵉ

-- pr1ᵉ commutes with transport in a Σᵉ-family (general form).
pr1ᵉ-exo-tr-gen :
    {ℓ ℓ' ℓ'' : Level} {A : UUᵉ ℓ} {B : A → UUᵉ ℓ'} {Cf : (x : A) → B x → UUᵉ ℓ''}
    {x y : A} (e : x =ᵉ y) (w : Σᵉ (B x) (Cf x))
  → pr1ᵉ (exo-tr (λ z → Σᵉ (B z) (Cf z)) e w) =ᵉ exo-tr B e (pr1ᵉ w)
pr1ᵉ-exo-tr-gen reflᵉ w = reflᵉ

-- Transport along a reindexing  f,  with independent levels and f explicit
-- (the library's exo-tr-ap forces dom/cod at one level and leaves f implicit).
exo-tr-ap' : {ℓA ℓB ℓP : Level} {A : UUᵉ ℓA} {B : UUᵉ ℓB} (f : A → B)
             {P : B → UUᵉ ℓP} {x y : A} (e : x =ᵉ y) {p : P (f x)}
           → exo-tr (λ z → P (f z)) e p =ᵉ exo-tr P (exo-ap f e) p
exo-tr-ap' f reflᵉ = reflᵉ

-- Moving a transport across a strict equality (both directions).
move-tr : {ℓ ℓ' : Level} {A : UUᵉ ℓ} {P : A → UUᵉ ℓ'} {x y : A} (p : x =ᵉ y)
          {u : P x} {v : P y} → exo-tr P p u =ᵉ v → u =ᵉ exo-tr P (exo-inv p) v
move-tr reflᵉ e = e

move-tr' : {ℓ ℓ' : Level} {A : UUᵉ ℓ} {P : A → UUᵉ ℓ'} {x y : A} (p : x =ᵉ y)
           {u : P x} {v : P y} → u =ᵉ exo-tr P (exo-inv p) v → exo-tr P p u =ᵉ v
move-tr' reflᵉ e = e

{- References:

  [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

-}