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

--------------------------------------------------------------------------------
-- Riehl–Shulman's structural lemmas on extension types (RS17 §4), as strict
-- isomorphisms in the framework.  Section 3.
--
-- These are pure strict-fibre facts: no fibrancy or cofibrancy is used.  Every
-- round-trip bottoms out in `ext-≡ reflᵉ` (the underlying sections agree
-- definitionally, by β/η) because the boundary witnesses live in a strict
-- proposition (UIPᵉ).
--------------------------------------------------------------------------------

module Extension.RS where

open import Extension.Prelude
open import Extension.Core

private
  variable
    ℓΦ ℓΨ ℓΩ ℓA ℓX ℓY : Level

--------------------------------------------------------------------------------
-- RS 4.1 : extension commutes with Π  (Lemma 3.4).
--
--   Extᵢ(λψ. Πₓ Y(ψ,x) , f)  ≅  Πₓ Extᵢ(λψ. Y(ψ,x) , λφ. f(φ,x))
--
-- Here X does not depend on ψ.
--------------------------------------------------------------------------------

module _ {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ)
         (X : UUᵉ ℓX) (Y : Ψ → X → UUᵉ ℓY)
         (f : (φ : Φ) (x : X) → Y (i φ) x)
       where

  private
    LHS : UUᵉ (ℓΦ ⊔ ℓΨ ⊔ ℓX ⊔ ℓY)
    LHS = Ext i (λ ψ → (x : X) → Y ψ x) f

    RHS : UUᵉ (ℓΦ ⊔ ℓΨ ⊔ ℓX ⊔ ℓY)
    RHS = (x : X) → Ext i (λ ψ → Y ψ x) (λ φ → f φ x)

    to : LHS → RHS
    to (g ,ᵉ p) x = (λ ψ → g ψ x) ,ᵉ exo-ap (λ h φ → h φ x) p

    from : RHS → LHS
    from k = (λ ψ x → pr1ᵉ (k x) ψ)
           ,ᵉ funextᵉ (λ φ → funextᵉ (λ x → happlyᵉ (pr2ᵉ (k x)) φ))

    from-to : (e : LHS) → from (to e) =ᵉ e
    from-to (g ,ᵉ p) = ext-≡ reflᵉ

    to-from : (k : RHS) → to (from k) =ᵉ k
    to-from k = funextᵉ (λ x → ext-≡ reflᵉ)

  RS41 : LHS ≅ RHS
  RS41 = to ,ᵉ (from ,ᵉ (from-to ,ᵉ to-from))

--------------------------------------------------------------------------------
-- RS 4.4 : composite of cofibrations  (Lemma 3.7).
--
-- For cofibrations  i : Φ ↪ Ψ,  j : Ψ ↪ Ω  and a family  A : Ω → UUᵉ,
--
--   Ext_{j∘i}(A , a)  ≅  Σ (f : Extᵢ(A∘j , a)). Ext_j(A , ext-app f).
--
-- Reading: to give a section on Ω restricting to `a` on Φ is to give its
-- restriction to Ψ (which already restricts to `a` on Φ) together with a further
-- extension from Ψ to Ω.
--------------------------------------------------------------------------------

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

  private
    ji : Φ → Ω
    ji φ = j (i φ)

    LHS : UUᵉ (ℓΦ ⊔ ℓΩ ⊔ ℓA)
    LHS = Ext ji A a

    RHS : UUᵉ (ℓΦ ⊔ ℓΨ ⊔ ℓΩ ⊔ ℓA)
    RHS = Σᵉ (Ext i (λ ψ → A (j ψ)) a) (λ f → Ext j A (ext-app f))

    to : LHS → RHS
    to h = (restrict j (pr1ᵉ h) ,ᵉ pr2ᵉ h) ,ᵉ (pr1ᵉ h ,ᵉ reflᵉ)

    from : RHS → LHS
    from (f ,ᵉ g) =
      pr1ᵉ g ,ᵉ exo-concat (exo-ap (restrict i {A = λ ψ → A (j ψ)}) (pr2ᵉ g)) (pr2ᵉ f)

    from-to : (h : LHS) → from (to h) =ᵉ h
    from-to h = ext-≡ reflᵉ

    to-from : (fg : RHS) → to (from fg) =ᵉ fg
    to-from (f ,ᵉ g) =
      dep-pair-=ᵉ _ _
        ( ext-≡ (pr2ᵉ g)
        ,ᵉ ext-≡ (pr1ᵉ-exo-tr-const (ext-≡ (pr2ᵉ g)) (pr1ᵉ g ,ᵉ reflᵉ)) )

  RS44 : LHS ≅ RHS
  RS44 = to ,ᵉ (from ,ᵉ (from-to ,ᵉ to-from))

--------------------------------------------------------------------------------
-- RS 4.3 : extension into Σ  (Lemma 3.6).
--
--   Extᵢ(λψ. Σ_{x:X ψ} Y(ψ,x) , (a,b))  ≅  Σ (f : Extᵢ(X,a)). Extᵢ(λψ. Y(ψ, f ψ), b)
--
-- The boundary datum of the inner extension type must be `b` transported along
-- the (strict) boundary  f∘i =ˢ a,  because our strict equality is propositional
-- rather than judgmental (see README).  This is the transport bookkeeping the
-- paper's proof performs implicitly.
--------------------------------------------------------------------------------

module _ {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ)
         (X : Ψ → UUᵉ ℓX) (Y : (ψ : Ψ) → X ψ → UUᵉ ℓY)
         (a : (φ : Φ) → X (i φ)) (b : (φ : Φ) → Y (i φ) (a φ))
       where

  private
    LHS : UUᵉ (ℓΦ ⊔ ℓΨ ⊔ ℓX ⊔ ℓY)
    LHS = Ext i (λ ψ → Σᵉ (X ψ) (Y ψ)) (λ φ → a φ ,ᵉ b φ)

    -- boundary datum of the second factor, transported along f's boundary
    bdry : (f : Ext i X a) → (φ : Φ) → Y (i φ) (ext-app f (i φ))
    bdry f φ = exo-tr (Y (i φ)) (exo-inv (ext-bdry f φ)) (b φ)

    RHS : UUᵉ (ℓΦ ⊔ ℓΨ ⊔ ℓX ⊔ ℓY)
    RHS = Σᵉ (Ext i X a) (λ f → Ext i (λ ψ → Y ψ (ext-app f ψ)) (bdry f))

    to : LHS → RHS
    to (h ,ᵉ p) = f ,ᵉ ((λ ψ → pr2ᵉ (h ψ)) ,ᵉ funextᵉ gbdry)
      where
      f : Ext i X a
      f = (λ ψ → pr1ᵉ (h ψ)) ,ᵉ exo-ap (λ s φ → pr1ᵉ (s φ)) p
      gbdry : (φ : Φ) → pr2ᵉ (h (i φ)) =ᵉ bdry f φ
      gbdry φ = exo-concat (move-tr (pr1ᵉ dp) (pr2ᵉ dp))
                           (exo-ap (λ q → exo-tr (Y (i φ)) (exo-inv q) (b φ))
                                   (UIPᵉ (pr1ᵉ dp) (ext-bdry f φ)))
        where dp = inv-dep-pair-=ᵉ (h (i φ)) (a φ ,ᵉ b φ) (happlyᵉ p φ)

    from : RHS → LHS
    from (f ,ᵉ g) = (λ ψ → pr1ᵉ f ψ ,ᵉ pr1ᵉ g ψ) ,ᵉ funextᵉ hbdry
      where
      hbdry : (φ : Φ) → (pr1ᵉ f (i φ) ,ᵉ pr1ᵉ g (i φ)) =ᵉ (a φ ,ᵉ b φ)
      hbdry φ = dep-pair-=ᵉ _ _
                  (ext-bdry f φ ,ᵉ move-tr' (ext-bdry f φ) (ext-bdry g φ))

    from-to : (e : LHS) → from (to e) =ᵉ e
    from-to (h ,ᵉ p) = ext-≡ reflᵉ

    to-from : (fg : RHS) → to (from fg) =ᵉ fg
    to-from (f ,ᵉ g) = dep-pair-=ᵉ _ _ (ext-≡ reflᵉ ,ᵉ ext-≡ Q)
      where
      ef : pr1ᵉ (to (from (f ,ᵉ g))) =ᵉ f
      ef = ext-≡ reflᵉ
      g₂ = pr2ᵉ (to (from (f ,ᵉ g)))
      -- pr1ᵉ of the transported 2nd factor equals pr1ᵉ g: transport in the
      -- Ext-family reduces to transport of the underlying section, and that
      -- transport only changes the boundary datum (ext-app is unchanged), so it
      -- is a semantically-constant transport, killed by UIPᵉ.
      Q : pr1ᵉ (exo-tr (λ f' → Ext i (λ ψ → Y ψ (ext-app f' ψ)) (bdry f')) ef g₂)
        =ᵉ pr1ᵉ g
      Q = exo-concat (pr1ᵉ-exo-tr-gen ef g₂)
                     (exo-concat (exo-tr-ap' ext-app {P = λ s → (ψ : Ψ) → Y ψ (s ψ)} ef)
                                 (exo-ap-tr (UIPᵉ (exo-ap ext-app ef) reflᵉ)))

  RS43 : LHS ≅ RHS
  RS43 = to ,ᵉ (from ,ᵉ (from-to ,ᵉ to-from))

{- 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

-}