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

--------------------------------------------------------------------------------
-- Congruence of the extension type in its family.
--
--   Ext-fam-≅ :  ((ψ : Ψ) → A ψ ≅ A' ψ)  →  Extᵢ(A , a)  ≅  Extᵢ(A' , a')
--
-- where the transported boundary is  a' φ = to (a φ).  A pointwise exo-iso of
-- the families lifts to a strict isomorphism of the extension types, the
-- boundary transported by the forward maps.  (This is the family-congruence
-- companion to the structural RS 4.1/4.3/4.4 isomorphisms; it is what lets us
-- rewrite an `Ext` along `exo-Σᵉ-equiv` etc.)
--------------------------------------------------------------------------------

module Extension.ExtFamIso where

open import Extension.Prelude
open import Extension.Core

private
  variable
    ℓΦ ℓΨ ℓA ℓA' : Level

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

  private
    mapto : (ψ : Ψ) → A ψ → A' ψ
    mapto ψ = pr1ᵉ (e ψ)
    mapfrom : (ψ : Ψ) → A' ψ → A ψ
    mapfrom ψ = pr1ᵉ (pr2ᵉ (e ψ))
    mapgf : (ψ : Ψ) (x : A ψ) → mapfrom ψ (mapto ψ x) =ᵉ x
    mapgf ψ = pr1ᵉ (pr2ᵉ (pr2ᵉ (e ψ)))
    mapfg : (ψ : Ψ) (y : A' ψ) → mapto ψ (mapfrom ψ y) =ᵉ y
    mapfg ψ = pr2ᵉ (pr2ᵉ (pr2ᵉ (e ψ)))

    a' : (φ : Φ) → A' (i φ)
    a' φ = mapto (i φ) (a φ)

  Ext-fam-≅ : Ext i A a ≅ Ext i A' a'
  Ext-fam-≅ = toE ,ᵉ (fromE ,ᵉ (fromtoE ,ᵉ tofromE))
    where
    toE : Ext i A a → Ext i A' a'
    toE (h ,ᵉ p) = (λ ψ → mapto ψ (h ψ))
                 ,ᵉ funextᵉ (λ φ → exo-ap (mapto (i φ)) (happlyᵉ p φ))

    fromE : Ext i A' a' → Ext i A a
    fromE (h' ,ᵉ p') = (λ ψ → mapfrom ψ (h' ψ)) ,ᵉ funextᵉ bd
      where
      bd : (φ : Φ) → mapfrom (i φ) (h' (i φ)) =ᵉ a φ
      bd φ = exo-concat (exo-ap (mapfrom (i φ)) (happlyᵉ p' φ)) (mapgf (i φ) (a φ))

    fromtoE : (z : Ext i A a) → fromE (toE z) =ᵉ z
    fromtoE (h ,ᵉ p) = ext-≡ (funextᵉ (λ ψ → mapgf ψ (h ψ)))

    tofromE : (z : Ext i A' a') → toE (fromE z) =ᵉ z
    tofromE (h' ,ᵉ p') = ext-≡ (funextᵉ (λ ψ → mapfg ψ (h' ψ)))

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

-}