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

--------------------------------------------------------------------------------
-- RS 4.8 for the extension type, homotopy form.
-- Lemma 3.13 / Lemma 3.13(1).
--
--   For f, g : ⟨Extᵢ(A,a)⟩ (fibrant match), the comparison map
--     happly : (f = g) → ⟨Extᵢ(λψ. fψ = gψ, λφ.refl)⟩
--   is an equivalence.
--
-- Proof (the paper's, made formal).  Fix f.  By the fundamental theorem of
-- identity types (`FundamentalId.fundamental-id`) it suffices that the fibrewise
-- map has a contractible total space, i.e. that
--     Σ (g). ⟨Extᵢ(λψ. fψ = gψ, refl)⟩          (†)
-- is contractible.  By `isFibrant-Σ` the match of the base `Extᵢ(A,a)` carries
-- (†) as `fibrant-match (isFibrant-Σ Wf QF)`, whose underlying exo type is, by
-- RS 4.3 (`RS.RS43`), the extension type `Extᵢ(λψ. Σ_{y}(fψ = y), (a,b))`.  Each
-- fibre `Σ_{y}(fψ = y)` is a based-path singleton, hence contractible, so that
-- extension type has a contractible match by relative funext (`RelFunext`,
-- i.e. RS 4.6).  The family mismatch between `Σᵉ(C·)(C·)` and `C(Σ··)` is bridged
-- by `exo-Σᵉ-equiv` + the family congruence `ExtFamIso.Ext-fam-≅`, and the
-- (propositional, not judgmental) boundary is realigned by `Ext-bdry-≅`.
--------------------------------------------------------------------------------

module Extension.RS48Ext where

open import Extension.Prelude
open import Extension.Core
open import Extension.CofibFibration
open import Extension.RS using (RS43)
open import Extension.ExtFamIso using (Ext-fam-≅)
open import Extension.RS46 using (Fib-iso-contr')
open import Extension.RelFunext using (satisfies-rel-funext)
open import Extension.FundamentalId using (fundamental-id)

private
  variable
    ℓ ℓΦ ℓΨ ℓA : Level

-- Identity isomorphism.
≅-id : {A : UUᵉ ℓ} → A ≅ A
≅-id = (λ x → x) ,ᵉ ((λ x → x) ,ᵉ ((λ _ → reflᵉ) ,ᵉ (λ _ → reflᵉ)))

-- Realign the boundary of an extension type along a strict equality of boundaries.
Ext-bdry-≅ : {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (A : Ψ → UUᵉ ℓA)
             {a a' : (φ : Φ) → A (i φ)} → a =ᵉ a' → Ext i A a ≅ Ext i A a'
Ext-bdry-≅ i A reflᵉ = ≅-id

-- A based-path singleton is contractible (inner HoTT).
sing-contr : {A : UU ℓ} (a₀ : A) → is-contr (Σ A (λ a → Id a₀ a))
sing-contr a₀ = (a₀ , refl) , (λ {(a , refl) → refl})

-- Transporting the canonical boundary path back along its own inverse gives refl.
tr-idpath-refl : {A : UU ℓ} {u v : C A} (e : u =ᵉ v)
  → exo-tr (λ w → C (Id (ic u) (ic w))) (exo-inv e) (c (=ᵉ-to-Id {a = ic u} {b = ic v} e))
    =ᵉ c (refl {x = ic u})
tr-idpath-refl reflᵉ = reflᵉ

--------------------------------------------------------------------------------

module _ {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
         (cof : is-cofib i ℓ) (triv : satisfies-rel-funext cof)
         (Y0 : Ψ → UU ℓ) (a : (φ : Φ) → C (Y0 (i φ)))
       where

  private
    Wf : isFibrant (Ext i (λ ψ → C (Y0 ψ)) a)
    Wf = Ext-isFibrant cof Y0 a

  -- public: EA and Q (below) form the statement of `RS48Ext` (and are
  -- referenced by the paper index src/index.agda)
  EA : UU (ℓΦ ⊔ ℓΨ ⊔ ℓ)
  EA = fibrant-match Wf

  private
    ν : C EA → Ext i (λ ψ → C (Y0 ψ)) a
    ν = pr1ᵉ (pr2ᵉ (fibrant-witness Wf))

  -- The section value represented by an element of the fibrant match.
  value : EA → (ψ : Ψ) → Y0 ψ
  value f ψ = ic (ext-app (ν (c f)) ψ)

  -- The pointwise path family and its canonical strict boundary.  These are
  -- public because the proof of truncation preservation recurses on them.
  pointwise-path : (f g : EA) → Ψ → UU ℓ
  pointwise-path f g ψ = Id (value f ψ) (value g ψ)

  pointwise-boundary : (f g : EA) (φ : Φ) → C (pointwise-path f g (i φ))
  pointwise-boundary f g φ =
    exo-tr (λ v → C (Id (value f (i φ)) (ic v)))
      (exo-inv (ext-bdry (ν (c g)) φ))
      (c (=ᵉ-to-Id
        {a = value f (i φ)} {b = ic (a φ)}
        (ext-bdry (ν (c f)) φ)))

  module _ (f : EA) where

    private
      ext-f : Ext i (λ ψ → C (Y0 ψ)) a
      ext-f = ν (c f)

      sf : (ψ : Ψ) → C (Y0 ψ)
      sf = pr1ᵉ ext-f

      -- RS 4.3 data: X = C∘Y0, the pointwise-identity family Yf, diagonal b.
      X : Ψ → UUᵉ ℓ
      X ψ = C (Y0 ψ)

      Yf : (ψ : Ψ) → X ψ → UUᵉ ℓ
      Yf ψ x = C (Id (ic (sf ψ)) (ic x))

      FΣ : Ψ → UUᵉ ℓ
      FΣ ψ = Σᵉ (X ψ) (Yf ψ)

      b : (φ : Φ) → Yf (i φ) (a φ)
      b φ = c (=ᵉ-to-Id {a = ic (sf (i φ))} {b = ic (a φ)} (ext-bdry ext-f φ))

      -- the fibre extension type over a base point z : Extᵢ(X,a)
      PathFam : (z : Ext i X a) → Ψ → UU ℓ
      PathFam z ψ = Id (ic (sf ψ)) (ic (ext-app z ψ))

      bd : (z : Ext i X a) (φ : Φ) → C (PathFam z (i φ))
      bd z φ = exo-tr (Yf (i φ)) (exo-inv (ext-bdry z φ)) (b φ)

      QF : (z : Ext i X a) → isFibrant (Ext i (λ ψ → C (PathFam z ψ)) (bd z))
      QF z = Ext-isFibrant cof (PathFam z) (bd z)

    Q : EA → UU (ℓΦ ⊔ ℓΨ ⊔ ℓ)
    Q g = fibrant-match
      (Ext-isFibrant cof (pointwise-path f g) (pointwise-boundary f g))

    private
      -- contractible-fibred family for the relative-funext step
      Fam : Ψ → UU ℓ
      Fam ψ = Σ (Y0 ψ) (λ y → Id (ic (sf ψ)) y)

      iso-fam : (ψ : Ψ) → C (Fam ψ) ≅ FΣ ψ
      iso-fam ψ = ≅-sym (exo-Σᵉ-equiv {A = Y0 ψ} {B = λ y → Id (ic (sf ψ)) y})

      bdry1 : (φ : Φ) → C (Fam (i φ))
      bdry1 φ = pr1ᵉ (pr2ᵉ (iso-fam (i φ))) (a φ ,ᵉ b φ)

      -- big-iso : Extᵢ(C∘Fam, bdry1) ≅ Σᵉ(Extᵢ(X,a)) QF-underlying   (= isFibrant-Σ underlying)
      step-fam : Ext i (λ ψ → C (Fam ψ)) bdry1
               ≅ Ext i FΣ (λ φ → pr1ᵉ (iso-fam (i φ)) (bdry1 φ))
      step-fam = Ext-fam-≅ i (λ ψ → C (Fam ψ)) FΣ iso-fam bdry1

      step-bdry : Ext i FΣ (λ φ → pr1ᵉ (iso-fam (i φ)) (bdry1 φ))
                ≅ Ext i FΣ (λ φ → a φ ,ᵉ b φ)
      step-bdry = Ext-bdry-≅ i FΣ
                    (funextᵉ (λ φ → pr2ᵉ (pr2ᵉ (pr2ᵉ (iso-fam (i φ)))) (a φ ,ᵉ b φ)))

      big-iso : Ext i (λ ψ → C (Fam ψ)) bdry1
              ≅ Σᵉ (Ext i X a) (λ z → Ext i (λ ψ → Yf ψ (ext-app z ψ)) (bd z))
      big-iso = ≅-trans step-fam (≅-trans step-bdry (RS43 i X Yf a b))

      contr-L : is-contr (fibrant-match (Ext-isFibrant cof Fam bdry1))
      contr-L = triv Fam (λ ψ → sing-contr (ic (sf ψ))) bdry1

      contr-Tot : is-contr (fibrant-match (isFibrant-Σ Wf QF))
      contr-Tot = Fib-iso-contr' (Ext-isFibrant cof Fam bdry1)
                                 (isFibrant-Σ Wf QF) big-iso contr-L

      -- the canonical (refl) centre of the fibre over f
      centre : Q f
      centre = ic (pr1ᵉ (fibrant-witness (QF (ν (c f))))
                        (ext-λ (λ ψ → c refl)
                               (funextᵉ (λ φ → exo-inv (tr-idpath-refl (ext-bdry ext-f φ))))))

      happ : (g : EA) → Id f g → Q g
      happ g p = tr Q p centre

    -- RS 4.8 for Ext: the comparison map is a fibrewise equivalence.
    RS48Ext-isEquiv : (g : EA) → isEquiv (happ g)
    RS48Ext-isEquiv = fundamental-id happ contr-Tot

    RS48Ext : (g : EA) → Id f g ≃ Q g
    RS48Ext g = happ g , RS48Ext-isEquiv g

    -- Naive form (RS 4.8(ii), Rzk `NaiveExtExt`): extensions that are pointwise
    -- equal, with refl on Φ, are equal.  Immediate from the inverse of RS48Ext.
    naive-ext-ext : (g : EA) → Q g → Id f g
    naive-ext-ext g = pr1 (≃-sym (RS48Ext g))

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

  [Rzk]        Nikolai Kudasov and others.  Rzk proof assistant, since 2023.
               https://github.com/rzk-lang/rzk

-}