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

--------------------------------------------------------------------------------
-- RS 4.8 (extension extensionality), strict form.
-- Lemma 3.13 (the reading of RS 4.9 is folded into that lemma).
--
-- The identity type of an extension type is again an extension type, of the
-- pointwise identities, restricting to reflexivity on the subshape:
--
--   (f =ˢ g)  ≅  Extᵢ(λψ. f ψ =ˢ g ψ , λφ. ⟨f∘i =ˢ a =ˢ g∘i⟩).
--
-- This is the strict/exo shadow of RS 4.8 (the homotopy form, about the identity
-- type of the fibrant match, needs the match-identity machinery, see README).
-- Both sides are strict propositions, so the equivalence is elementary: it is
-- funext for the outer level together with proof-irrelevance of `=ᵉ` (UIPᵉ).
--------------------------------------------------------------------------------

module Extension.RS48 where

open import Extension.Prelude
open import Extension.Core

private
  variable
    ℓΦ ℓΨ ℓA : Level

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

  -- pointwise-identity family and its boundary datum (f and g agree with a, so
  -- they agree with each other, on the subshape)
  private
    IdFam : Ψ → UUᵉ ℓA
    IdFam ψ = ext-app f ψ =ᵉ ext-app g ψ

    idBdry : (φ : Φ) → IdFam (i φ)
    idBdry φ = exo-concat (ext-bdry f φ) (exo-inv (ext-bdry g φ))

  Ext-Id-strict : (f =ᵉ g) ≅ Ext i IdFam idBdry
  Ext-Id-strict = to ,ᵉ (from ,ᵉ (from-to ,ᵉ to-from))
    where
    to : (f =ᵉ g) → Ext i IdFam idBdry
    to p = happlyᵉ (exo-ap pr1ᵉ p) ,ᵉ funextᵉ (λ φ → UIPᵉ _ _)

    from : Ext i IdFam idBdry → (f =ᵉ g)
    from (H ,ᵉ _) = ext-≡ (funextᵉ H)

    from-to : (p : f =ᵉ g) → from (to p) =ᵉ p
    from-to p = UIPᵉ _ p

    to-from : (w : Ext i IdFam idBdry) → to (from w) =ᵉ w
    to-from (H ,ᵉ q) = dep-pair-=ᵉ _ _ (funextᵉ (λ ψ → UIPᵉ _ _) ,ᵉ UIPᵉ _ _)

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

-}