{-# OPTIONS --postfix-projections --prop #-}
module Id where

open import Agda.Primitive
open import Lib
open import Fam as _

--------------------------
--- Introduction rules ---
--------------------------

record Id-Intro {ic jc} (C : Fam {ic} {jc}) : Set (ic  jc) where
  module C = Fam C
  field Id  :  {A : C.Ty} (x : C.Tm A) (y : C.Tm A)  C.Ty
        idp :  {A : C.Ty} {x : C.Tm A}  C.Tm (Id {A} x x)

  Singl :  {A}  C.Tm A  Set jc
  Singl x = Σ _ λ y  C.Tm (Id x y)

  center :  {A x}  Singl {A} x
  center = _ , idp

  isContr : C.Ty  Set _
  isContr A = Σ (C.Tm A) λ a   b  C.Tm (Id a b)

  allPaths : C.Ty  Set _
  allPaths A =  a b  C.Tm (Id {A} a b)

  isProp : C.Ty  Set _
  isProp A =  a b  isContr (Id {A} a b)

  record IsSet (A : C.Ty) : Set jc where
    field prop-Id :  a b  isProp (Id {A} a b)

    K :  {x} (p : C.Tm (Id x x))  C.Tm (Id p idp)
    K p = prop-Id _ _ _ _ .fst

instance
  Id-Intro-⊤ :  {i j}  Id-Intro (Fam-⊤ {i} {j})
  Id-Intro-⊤ .Id-Intro.Id _ _ = tt
  Id-Intro-⊤ .Id-Intro.idp = tt

IsSet-⊤ :  {i j}  Id-Intro.IsSet (Id-Intro-⊤ {i} {j}) tt
IsSet-⊤ .Id-Intro.IsSet.prop-Id _ _ _ _ = tt , λ _  tt

-------------------------------------------------
--- Weak identity type elimination structures ---
-------------------------------------------------

record Id-Elim {ic jc id jd} (C : Fam {ic} {jc})  CId : Id-Intro C 
               (D : Fam {id} {jd})  DId : Id-Intro D  : Set (ic  jc  id  jd) where
  open Id-Intro CId
  private
    module CId = Id-Intro CId
    module D   = Fam D
    module DId = Id-Intro DId
  field J :  {A : C.Ty} {x : C.Tm A} (P : Singl x  D.Ty)
              (d : D.Tm (P center)) (yp : Singl x)
               D.Tm (P yp)
        J-β :  {A : C.Ty} {x : C.Tm A} {P : Singl x  D.Ty}
                {d : D.Tm (P center)}
               D.Tm (DId.Id (J P d center) d)

  transp :  {A : C.Ty} {x : C.Tm A} (P : C.Tm A  D.Ty)
             (d : D.Tm (P x)) {y : C.Tm A} (p : C.Tm (Id x y))
            D.Tm (P y)
  transp P d p = J  (z , _)  P z) d (_ , p)

  transp-β :  {A : C.Ty} {x : C.Tm A} {P : C.Tm A  D.Ty}
                  {d : D.Tm (P x)}
                 D.Tm (DId.Id (transp P d idp) d)
  transp-β = J-β

  ap :  {A B} (f : C.Tm A  D.Tm B) {x y : C.Tm A} (p : C.Tm (CId.Id x y))  D.Tm (DId.Id (f x) (f y))
  ap f {x = x} p = transp  z  DId.Id (f x) (f z)) DId.idp p

-----------------------------------------------------------
--- Constructions using a weak identity type structure  ---
---  (Groupoid operations and laws, etc)                ---
-----------------------------------------------------------
module IdM {ic jc} (C : Fam {ic} {jc})  CId : Id-Intro C   CId-Elim-C : Id-Elim C C  (_ :  {lzero}) where -- (_ : ⊤) forces the resolution of instance arguments
  open Fam C
  open Id-Intro CId public
  open Id-Elim CId-Elim-C public

  abstract
    trans :  {A} {x y z : Tm A}  Tm (Id x y)  Tm (Id y z)  Tm (Id x z)
    trans {x = x} p q = transp  w  Id x w) p q

    trans-β-l :  {A} {y z : Tm A} {q : Tm (Id y z)}  Tm (Id (trans idp q) q)
    trans-β-l {q = q} = J  (z , q)  Id (trans idp q) q) J-β (_ , q)

    trans-β-r :  {A} {x y : Tm A} {p : Tm (Id x y)}  Tm (Id (trans p idp) p)
    trans-β-r = J-β

    trans-β-triangle :  {A} {x : Tm A}  Tm (Id (trans-β-l {q = idp {x = x}}) (trans-β-r))
    trans-β-triangle = J-β

  abstract
    sym :  {A} {x y : Tm A}  Tm (Id x y)  Tm (Id y x)
    sym {x = x} {y = y} p = transp  z  Id z x) idp p

    sym-β :  {A} {x : Tm A}  Tm (Id (sym (idp {x = x})) idp)
    sym-β = J-β

  abstract
    sym-sym :  {A} {x y : Tm A} (p : Tm (Id x y))  Tm (Id (sym (sym p)) p)
    sym-sym p = J  (z , q)  Id (sym (sym q)) q) (trans (ap sym sym-β) sym-β) (_ , p)

  abstract
    trans-assoc :  {A} {x y z w : Tm A} {p : Tm (Id x y)} {q : Tm (Id y z)} {r : Tm (Id z w)}
                 Tm (Id (trans p (trans q r)) (trans (trans p q) r))
    trans-assoc {A} {x} {y} {z} {w} {p} {q} {r}
      = J  (w , r)  Id (trans p (trans q r)) (trans (trans p q) r))
          (trans (ap (trans p) trans-β-r) (sym trans-β-r)) (_ , r)

  abstract
    trans-sym-r :  {A} {x y : Tm A} (p : Tm (Id x y))  Tm (Id (trans p (sym p)) idp)
    trans-sym-r p = J  (_ , q)  Id (trans q (sym q)) idp)
                      (trans (ap (trans _) sym-β) trans-β-r)
                        (_ , p)

    trans-sym-r-β :  {A} {x : Tm A}  Tm (Id (trans-sym-r {x = x} idp) (trans (ap (trans _) sym-β) trans-β-r))
    trans-sym-r-β = J-β

  abstract
    trans-sym-l :  {A} {x y : Tm A} (p : Tm (Id x y))  Tm (Id (trans (sym p) p) idp)
    trans-sym-l p = J  (_ , p)  Id (trans (sym p) p) idp) (trans (ap  q  trans q _) sym-β) trans-β-r) (_ , p)

  abstract
    sym-trans :  {A} {x y z : Tm A} {p : Tm (Id x y)} {q : Tm (Id y z)}
                 Tm (Id (sym (trans p q)) (trans (sym q) (sym p)))
    sym-trans {A} {x} {y} {z} {p} {q} =
      J  (_ , q)  Id (sym (trans p q)) (trans (sym q) (sym p)))
        (trans (ap sym trans-β-r) (sym (trans (ap  q  trans q (sym p)) sym-β) trans-β-l) )) (_ , q)

  abstract
    cong-trans :  {A} {x y z : Tm A} {p₁ p₂ : Tm (Id x y)} {q₁ q₂ : Tm (Id y z)}
                Tm (Id p₁ p₂)  Tm (Id q₁ q₂)
                Tm (Id (trans p₁ q₁) (trans p₂ q₂))
    cong-trans {p₁ = p₁} {q₂ = q₂} α β = trans (ap (trans p₁) β) (ap  p  trans p q₂) α)

  abstract
    ap-id :  {A} {x y : Tm A} {p : Tm (Id x y)}
           Tm (Id (ap  x  x) p) p)
    ap-id {x = x} = J  (y , p)  Id (ap  x  x) p) p)
                    J-β _

  abstract
    ap-id' :  {A} (f : Tm A  Tm A) (h :  a  Tm (Id (f a) a)) {x y : Tm A} {p : Tm (Id x y)}
           Tm (Id (ap f p) (trans (h x) (trans p (sym (h y)))))
    ap-id' f h {x = x} = J  (y , p)  Id (ap f p) (trans (h x) (trans p (sym (h y)))))
                          (trans J-β (sym (trans (ap (trans _) trans-β-l) (trans-sym-r _)))) _

  abstract
    ap-∘ :  {A B C} (f : Tm A  Tm B) (g : Tm B  Tm C) {x y} {p : Tm (Id x y)}
          Tm (Id (ap (g  f) p) (ap g (ap f p)))
    ap-∘ {A} {B} {C} f g {x} {y} {p} = J  (y , p)  Id (ap (g  f) p) (ap g (ap f p)))
                                         (trans J-β (sym (trans (ap (ap g) J-β) J-β))) _

  abstract
    trans-ap :  {A B} {f : Tm A  Tm B} {x y z : Tm A} {p : Tm (Id x y)} {q : Tm (Id y z)}
              Tm (Id (trans (ap f p) (ap f q)) (ap f (trans p q)))
    trans-ap {A} {B} {f} {x} {y} {z} {p} {q} =
      J  (z , q)  Id (trans (ap f p) (ap f q)) (ap f (trans p q)))
        (trans (ap (trans (ap f p)) J-β) (trans trans-β-r (sym (trans (ap (ap f) trans-β-r) idp)))) (_ , q)

  abstract
    transp-trans :  {A : Ty} {x : Tm A} {P : Tm A  Ty}
                     {d : Tm (P x)} {y z} {p : Tm (Id x y)} {q : Tm (Id y z)}
                    Tm (Id (transp P (transp P d p) q) (transp P d (trans p q)))
    transp-trans {A} {x} {P} {d} {y} {z} {p} {q} =
      J  (_ , q)  Id (transp P (transp P d p) q) (transp P d (trans p q)))
        (trans transp-β (sym (ap (transp P d) trans-β-r)))
        (_ , q)

  abstract
    trans-pentagon :  {A} {x y : Tm A} (p : Tm (Id x y)) 
                     Tm (Id (trans (sym (trans-β-r)) (ap (trans p) (sym (trans-sym-l p))))
                            (sym (trans trans-assoc (trans (ap  q  trans q p) (trans-sym-r p)) trans-β-l))))
    trans-pentagon p = J  (y , p)  Id (trans (sym (trans-β-r)) (ap (trans p) (sym (trans-sym-l p))))
                                         (sym (trans trans-assoc (trans (ap  q  trans q p) (trans-sym-r p)) trans-β-l))))
                         p₀ (_ , p) where
      p₀ : Tm (Id (trans (sym (trans-β-r)) (ap (trans idp) (sym (trans-sym-l idp))))
                  (sym (trans trans-assoc (trans (ap  q  trans q idp) (trans-sym-r idp)) trans-β-l))))
      p₀ = trans (ap (trans _) (trans (ap-id' _  a  trans-β-l))
                 (trans (ap  q  trans trans-β-l (trans (sym q) (sym trans-β-l))) (trans J-β (ap  q  trans q trans-β-r) (ap-id' _  _  trans-β-r)))))
                 idp)))
           (sym (trans (trans sym-trans (trans (ap (trans _) (ap sym (trans J-β (ap  q  trans q (sym trans-β-r)) (ap-id' _  _  trans-β-l))))))
           (ap  q  trans (sym q) (sym (trans (trans trans-β-l (trans trans-β-r (sym trans-β-l))) (sym trans-β-r)))) (ap  q  trans q trans-β-l) (ap-id' _  _  trans-β-r))))))
           (trans (cong-trans (trans sym-trans (cong-trans idp (trans sym-trans (cong-trans (trans sym-trans (cong-trans (sym-sym _) (trans (ap sym trans-sym-r-β) (trans sym-trans (cong-trans idp (trans (ap sym (ap-id' _  a  trans-β-l))) (trans sym-trans (cong-trans (trans sym-trans (cong-trans (sym-sym _) idp)) idp)))))))) idp)))) (trans sym-trans (cong-trans (sym-sym _) (trans sym-trans (cong-trans (trans sym-trans (cong-trans (sym-sym _) idp)) idp)))))
           (trans (trans (sym trans-assoc) (cong-trans idp (trans (sym trans-assoc) idp)))
           (trans (cong-trans (ap sym trans-β-triangle) idp)
           (ap (trans _)
           (trans (sym trans-assoc)
           (trans (cong-trans (sym trans-β-triangle) idp)
           (ap (trans _)
           (sym
           (trans (cong-trans (trans sym-trans (cong-trans idp (trans sym-trans (cong-trans (trans sym-trans (cong-trans (sym-sym _) idp)) idp)))) idp)
           (trans (sym trans-assoc)
           (sym
           (trans (sym trans-assoc)
           (ap (trans _)
           (trans (sym trans-assoc)
           (trans (sym trans-assoc)
           (sym
           (trans (sym trans-assoc)
           (trans (sym trans-assoc)
           (trans (cong-trans (sym trans-β-triangle) idp)
           (ap (trans _)
           (ap (trans _)
           (sym (trans (cong-trans idp (trans trans-assoc (trans (cong-trans (trans-sym-l _) idp) trans-β-l)))
           (trans (trans trans-assoc (cong-trans (trans trans-assoc (trans (cong-trans (trans-sym-l _) idp) trans-β-l)) idp))
           idp))))))))))))))))))))))))))

  module _ {A : Ty} where
    abstract
      isContr⇒allPaths : isContr A  allPaths A
      isContr⇒allPaths (x , f) a b = trans (sym (f a)) (f b)

    abstract
      allPaths⇒isProp : allPaths A  isProp A
      allPaths⇒isProp x a b = trans (x a b) (sym (x b b))
                              , λ p  J  (z , q)  Id (trans (x a z) (sym (x z z))) q)
                                        (trans-sym-r _)
                                        (_ , p)

    abstract
      isContr-from-transp : (e :  (P : C.Tm A  C.Ty) x (d : C.Tm (P x)) y  C.Tm (P y))  C.Tm A  isContr A
      isContr-from-transp e c = c , e (Id _) c idp

  module _ {A : Ty} {B : Ty} (f : Tm A  Tm B) (g : Tm B  Tm A) (h : (b : Tm B)  Tm (Id (f (g b)) b)) where
    isContr-retract : isContr A  isContr B
    isContr-retract (c , p) = f c , λ b  trans (ap f (p (g b))) (h _)


-------------------------------------------------------------------------------------
--- Constructions using a heterogeneous weak identity type elimination structure  ---
-------------------------------------------------------------------------------------
module Id-ElimM {ic jc id jd} (C : Fam {ic} {jc}) (D : Fam {id} {jd})  CId : Id-Intro C   DId : Id-Intro D 
                 CId-Elim-C : Id-Elim C C   CId-Elim-D : Id-Elim C D   DId-Elim-D : Id-Elim D D  (_ :  {lzero}) where
  private
    module C          = Fam C
    module CId        = IdM C _
    module CId-Elim-D = Id-Elim CId-Elim-D
    module D          = Fam D
    module DId        = IdM D _
  open CId-Elim-D public

  abstract
    transp-trans :  {A : C.Ty} {x : C.Tm A} {P : C.Tm A  D.Ty}
                     {d : D.Tm (P x)} {y z} {p : C.Tm (CId.Id x y)} {q : C.Tm (CId.Id y z)}
                    D.Tm (DId.Id (CId-Elim-D.transp P (CId-Elim-D.transp P d p) q) (CId-Elim-D.transp P d (CId.trans p q)))
    transp-trans {A} {x} {P} {d} {y} {z} {p} {q} =
      CId-Elim-D.J  (_ , q)  DId.Id (CId-Elim-D.transp P (CId-Elim-D.transp P d p) q) (CId-Elim-D.transp P d (CId.trans p q)))
        (DId.trans CId-Elim-D.transp-β (DId.sym (CId-Elim-D.ap (CId-Elim-D.transp P d) CId.trans-β-r)))
        (_ , q)

  module _ {A} (cA : CId.isContr A) (P : C.Tm A  D.Ty) where
    abstract
      isContr-transp :  {x} y (d : D.Tm (P x))  D.Tm (P y)
      isContr-transp y d = CId-Elim-D.transp P d (CId.isContr⇒allPaths cA _ _)

      isContr-transp-β :  {x} (d : D.Tm (P x))  D.Tm (DId.Id (isContr-transp x d) d)
      isContr-transp-β d = DId.trans (CId-Elim-D.ap (CId-Elim-D.transp P d) (CId.isContr⇒allPaths (CId.allPaths⇒isProp (CId.isContr⇒allPaths cA) _ _) _ _)) CId-Elim-D.transp-β

      isContr-transp-trans :  {x y z} (d : D.Tm (P x))  D.Tm (DId.Id (isContr-transp z (isContr-transp y d)) (isContr-transp z d))
      isContr-transp-trans d = DId.trans transp-trans (CId-Elim-D.ap (CId-Elim-D.transp P d) (CId.isContr⇒allPaths (CId.allPaths⇒isProp (CId.isContr⇒allPaths cA) _ _) _ _))