```{-# OPTIONS --rewriting #-}

module Id  where

open import Equality
open import EquationalReasoning
open import Fibration
open import Function
open import Interval
open import Level
open import Path
open import Product
open import Sigma

----------------------------------------------------------------------
-- Propositional identity types
----------------------------------------------------------------------
Id :
{ℓ ℓ' : Level}
{Γ : Set ℓ}
(A : Γ → Set ℓ')
(a b : (x : Γ) → A x)
→ -------------------
Γ → Set ℓ'
Id A a b x = a x ~ b x

IdAct :
{ℓ ℓ' : Level}
{Γ : Set ℓ}
(A : Γ → Set ℓ')
{{_ : isFib A}}
(a b : (x : Γ) → A x)
(x y : Γ)
(p : x ~ y)
→ ---------------------
Id A a b x → Id A a b y
IdAct A a b _ _ p q =
~symm (I~∗O A b p) ∙ ⟨ i ⟩(p ∗ (q at i)) ∙ (I~∗O A a p)

IdActId :
{ℓ ℓ' : Level}
{Γ : Set ℓ}
(A : Γ → Set ℓ')
{{_ : isFib A}}
(a b : (x : Γ) → A x)
(x : Γ)
(q : Id A a b x)
→ -----------------------------
q ~ IdAct A a b x x (~refl x) q
IdActId A {{α}} a b x q =
let f = q at_ in
path:
q
~[ ∙refl q ]
q ∙ ~refl (a x)
~[ ~cong (q ∙_) (~symm (~invl (~substrefl α (a x)))) ]
q ∙ ~symm (~substrefl α (a x)) ∙ ~substrefl α (a x)
~[ ~cong (λ p → q ∙ ~symm (~substrefl α (a x)) ∙ p)
(refl∙ (~substrefl α (a x))) ]
q ∙ ~symm (~substrefl α (a x)) ∙ ~refl (~subst α (~refl x) (a x)) ∙
~substrefl α (a x)
~[ ⟨ j ⟩((q from j) ∙ ~symm (~substrefl α (f j)) ∙
⟨ i ⟩(~subst α (~refl x) (f (cvx O i j))) ∙ ~substrefl α (a x)) ]
~refl (b x) ∙ ~symm (~substrefl α (b x)) ∙
⟨ i ⟩(~subst α (~refl x) (f i)) ∙ ~substrefl α (a x)
~[ ~symm (refl∙ (~symm (~substrefl α (b x)) ∙
⟨ i ⟩(~subst α (~refl x) (f i)) ∙ ~substrefl α (a x))) ]
~symm (~substrefl α (b x)) ∙ ⟨ i ⟩(~subst α (~refl x) (f i)) ∙
~substrefl α (a x)
~[ ~cong (λ p → ~symm p ∙ ⟨ i ⟩(~subst α (~refl x) (f i)) ∙
~substrefl α (a x)) (I~∗Oid A {{α}} b x) ]
~symm (I~∗O A b (~refl x)) ∙ ⟨ i ⟩(~subst α (~refl x) (f i)) ∙
~substrefl α (a x)
~[ ~cong (λ p → ~symm (I~∗O A b (~refl x)) ∙
⟨ i ⟩(~subst α (~refl x) (f i)) ∙ p) (I~∗Oid A {{α}} a x) ]
~symm (I~∗O A b (~refl x)) ∙ ⟨ i ⟩(~subst α (~refl x) (f i)) ∙
(I~∗O A a (~refl x))
endp

isFibId :
{ℓ ℓ' : Level}
{Γ : Set ℓ}
(A : Γ → Set ℓ')
{{_ : isFib A}}
(a b : (x : Γ) → A x)
→ -------------------
isFib (Id A a b)
isFibId A {{α}} a b = (IdAct A {{α}} a b , IdActId A {{α}} a b)

Refl :
{ℓ ℓ' : Level}
{Γ : Set ℓ}
{A : Γ → Set ℓ'}
(a : (x : Γ) → A x)
→ ------------------
(x : Γ) → Id A a a x
Refl a x = ~refl (a x)

Idelim :
{ℓ ℓ' ℓ'' : Level}
{Γ : Set ℓ}
{A : Γ → Set ℓ'}
{a : (x : Γ) → A x}
(B : (Σ (Σ Γ A) (Id (A ∘ fst) (a ∘ fst) snd)) → Set ℓ'')
{{_ : isFib B}}
(b : (x : Γ) → B ((x , a x) , Refl a x))
{a' : (x : Γ) → A x}
(e : (x : Γ) → Id A a a' x)
→ ------------------------------------------------------
(x : Γ) → B ((x , a' x) , e x)
Idelim B {{β}} b e x =
~subst β (⟨ i ⟩((x , e x at i) , e x upto i)) (b x)

Idcomp :
{ℓ ℓ' ℓ'' : Level}
{Γ : Set ℓ}
{A : Γ → Set ℓ'}
{a : (x : Γ) → A x}
(B : (Σ (Σ Γ A) (Id (A ∘ fst) (a ∘ fst) snd)) → Set ℓ'')
{{_ : isFib B}}
(b : (x : Γ) → B ((x , a x) , Refl a x))
(x : Γ)
→ ------------------------------------------------------
b x ~ Idelim B b (Refl a) x
Idcomp B {{β}} b x = ~substrefl β (b x)
```