Jonathan Sterling, started 22 March, 2023.

Based on Egbert Rijke's "Introduction to Homotopy Type Theory".

\begin{code}

{-# OPTIONS --safe --without-K #-}

module UF.IdentitySystems where

open import MLTT.Spartan
open import UF.Base
open import UF.Embeddings
open import UF.Equiv
open import UF.FunExt
open import UF.Retracts
open import UF.Subsingletons
open import UF.PairFun as PairFun

record Has-Id-Sys {𝓦} (A : 𝓤 ̇ ) (a : A) (fam : A → 𝓦 ̇) : 𝓤ω where
 field
  ctr : fam a
  ind : {𝓥 : Universe} (P : (x : A) (q : fam x) → 𝓥 ̇) (p : P a ctr) (x : A) (q : fam x) → P x q
  ind-β : {𝓥 : Universe} (P : (x : A) (q : fam x) → 𝓥 ̇) (p : P a ctr) → ind P p a ctr ＝ p

 to-＝ : (x : A) → fam x → a ＝ x
 to-＝ = ind _ refl

 from-＝ : (x : A) → a ＝ x → fam x
 from-＝ x refl = ctr

 to-＝-is-equiv : (x : A) → is-equiv (to-＝ x)
 pr₁ (pr₁ (to-＝-is-equiv x)) = from-＝ x
 pr₂ (pr₁ (to-＝-is-equiv x)) refl = ind-β _ _
 pr₁ (pr₂ (to-＝-is-equiv x)) = from-＝ x
 pr₂ (pr₂ (to-＝-is-equiv x)) q = aux x q
  where
   aux : (x : A) (q : fam x) → from-＝ x (to-＝ x q) ＝ q
   aux = ind _ (ap (from-＝ a) (ind-β _ _))

record Id-Sys 𝓦 (A : 𝓤 ̇ ) (a : A) : 𝓤ω where
 field
  fam : A → 𝓦  ̇
  sys : Has-Id-Sys A a fam
 open Has-Id-Sys sys public


Unbiased-Id-Sys : Universe → 𝓤 ̇ → 𝓤ω
Unbiased-Id-Sys 𝓦 A = (a : A) → Id-Sys 𝓦 A a


module from-path-characterization
  {A : 𝓤 ̇ }
  (Q : A → A → 𝓤 ̇ )
  (H : {x y : A} → (x ＝ y) ≃ Q x y)
  (a : A)
 where
  open Id-Sys
  open Has-Id-Sys

  private
   Q-refl : {x : A} → Q x x
   Q-refl = eqtofun H refl

   aux
    : (P : (x : A) (q : Q a x) → 𝓥 ̇ )
    → (p : P a Q-refl)
    → (x : A)
    → (q : a ＝ x)
    → P x (eqtofun H q)
   aux P p x refl = p

  id-sys : Id-Sys 𝓤 A a
  fam id-sys = Q a
  ctr (sys id-sys) = Q-refl
  ind (sys id-sys) P p x q =
   transport (P x)
    (inverses-are-sections _ (eqtofun- H) q)
    (aux P p x (back-eqtofun H q))
  ind-β (sys id-sys) P p =
   ap gen
    (Aux-is-prop
     (back-eqtofun H Q-refl ,
      inverses-are-sections _ (eqtofun- H)  Q-refl)
     (refl , refl))
   where
    Aux = Σ ϕ ꞉ a ＝ a , eqtofun H ϕ ＝ Q-refl

    Aux-singl : singleton-type' refl ≃ Aux
    Aux-singl =
     pair-fun-equiv (≃-refl (a ＝ a)) λ ϕ →
     ap (eqtofun H) ,
     embedding-gives-embedding' _
      (equivs-are-embeddings _ (eqtofun- H))
      ϕ
      refl

    Aux-is-prop : is-prop Aux
    Aux-is-prop =
     retract-of-prop
      (≃-gives-◁ (≃-sym Aux-singl))
      (singleton-types'-are-props refl)

    gen : Aux → P a Q-refl
    gen (ϕ , ψ ) = transport (P a) ψ (aux P p a ϕ)


module _ 𝓦 𝓦' (A : 𝓤 ̇ ) (B : A → 𝓥 ̇ ) where
 record Dep-Id-Sys {a : A} ([a] : Id-Sys 𝓦 A a) (b : B a) : 𝓤ω where
  private
   module [a] = Id-Sys [a]
  field
   fam : (x : A) (q : [a].fam x) (y : B x) → 𝓦' ̇
   sys : Has-Id-Sys (B a) b (fam a [a].ctr)

  open Has-Id-Sys sys public


module _
  {A : 𝓤 ̇ } {B : A → 𝓥 ̇ }
  {a : A} {b : B a}
  ([a] : Id-Sys 𝓦 A a)
  ([b] : Dep-Id-Sys 𝓦 𝓦' A B [a] b)
 where
  module [a] = Id-Sys [a]
  module [b] = Dep-Id-Sys [b]

  open Id-Sys
  open Has-Id-Sys

  pair-id-sys : Id-Sys (𝓦 ⊔ 𝓦') (Σ B) (a , b)
  fam pair-id-sys (x , y) = Σ ϕ ꞉ [a].fam x , [b].fam x ϕ y
  pr₁ (ctr (sys pair-id-sys)) = [a].ctr
  pr₂ (ctr (sys pair-id-sys)) = [b].ctr
  ind (sys pair-id-sys) P p =
   λ (x , y) (ϕ , ψ) → aux x ϕ y ψ
   where
    aux : (x : A) (ϕ : [a].fam x) (y : B x) (ψ : [b].fam x ϕ y) → P (x , y) (ϕ , ψ)
    aux = [a].ind _ ([b].ind _ p)
  ind-β (sys pair-id-sys) P p =
   happly (happly ([a].ind-β _ _) b) [b].ctr ∙ [b].ind-β _ _

module _ (A : 𝓤 ̇ ) where
 open Id-Sys
 open Has-Id-Sys

 ＝-id-sys : Unbiased-Id-Sys 𝓤 A
 fam (＝-id-sys a) = a ＝_
 ctr (sys (＝-id-sys a)) = refl
 ind (sys (＝-id-sys a)) P p x refl = p
 ind-β (sys (＝-id-sys a)) _ _ = refl

module _ (fe : funext 𝓤 𝓥) {A : 𝓤 ̇ } {B : 𝓥 ̇ } (f : A → B) where
 homotopy-id-sys : Id-Sys (𝓤 ⊔ 𝓥) (A → B) f
 homotopy-id-sys = from-path-characterization.id-sys _∼_ (happly-≃ fe) f

\end{code}