module Id.Id where

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

open import Id.Intro public
open import Id.Elim public
open import Id.Groupoid

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

  module _ {A : C .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 : C .Ty} {B : C .Ty} (f : C .Tm A → C .Tm B) (g : C .Tm B → C .Tm A) (h : (b : C .Tm B) → C .Tm (Id (f (g b)) b)) where
    abstract
      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 (C : Fam) (D : Fam) ⦃ 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 ⦄ (_ : ⊤) 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) _ _) _ _))