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