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

open import Agda.Primitive
open import Lib
open import Fam as _
open import Id
open import Id-Tele as _

-------------------------------------------------------------------------------------------
--- "Internal" PathFrom and PathTo type families, and proofs that they are contractible ---
-------------------------------------------------------------------------------------------

module _ {ic jc} {C : Fam {ic} {jc}} ⦃ CId : Id-Intro C ⦄ ⦃ CId-Elim-C : Id-Elim C C ⦄ where
  private
    open Id-Tele-r C
    module C           = Fam C
    module CC          = Fam (C ∗ C)
    module CId         = IdM C _
    module CCId        = IdM (C ∗ C) _

  PathFrom : ∀ {A} → C.Tm A → CC.Ty
  PathFrom {A} x = A , λ y → CId.Id x y

  abstract
    isContr-PathFrom : ∀ {A} x → CCId.isContr (PathFrom {A} x)
    isContr-PathFrom {A} x = (x , CId.idp)
                           , λ { (y , p) → p , CId.J (λ (y , p) → CId.Id (CId.transp _ CId.idp p) p) CId.transp-β _ }

module _ {ic jc} {C : Fam {ic} {jc}} ⦃ CId : Id-Intro C ⦄ ⦃ CId-Elim-C : Id-Elim C C ⦄ where
  private
    open Id-Tele-r C
    module C           = Fam C
    module CC          = Fam (C ∗ C)
    module CId         = IdM C _
    module CCId        = IdM (C ∗ C) _

  PathTo : ∀ {A} → C.Tm A → CC.Ty
  PathTo {A} x = A , λ y → CId.Id y x

  abstract
    isContr-PathTo : ∀ {A} x → CCId.isContr (PathTo {A} x)
    isContr-PathTo {A} x = (x , CId.idp)
                         , λ { (y , p) → CId.sym p , CId.trans (CId.J (λ (x , p) → CId.Id (CId.transp _ _ p) (CId.sym p)) (CId.trans CId.transp-β (CId.sym CId.sym-β)) _) (CId.sym-sym _) }

--------------------------------
--- hSets are closed under Σ ---
--------------------------------
module _ {ic jc id jd} {C : Fam {ic} {jc}} ⦃ CId : Id-Intro C ⦄ ⦃ CId-Elim-C : Id-Elim C C ⦄
         {D : Fam {id} {jd}} ⦃ DId : Id-Intro D ⦄ ⦃ CId-Elim-D : Id-Elim C D ⦄ ⦃ DId-Elim-D : Id-Elim D D ⦄ ⦃ DId-Elim-C : Id-Elim D C ⦄ where
  private
    open Id-Tele-r C
    open Id-Tele-r D
    module CId  = IdM C _
    module DId  = IdM D _
    module CDId = IdM (C ∗ D) _

  instance
    IsSet-Σ : ∀ {A B} ⦃ IsSet-A : CId.IsSet A ⦄ ⦃ IsSet-B : ∀ {a} → DId.IsSet (B a) ⦄ → CDId.IsSet (A , B)
    IsSet-Σ ⦃ IsSet-A ⦄ ⦃ IsSet-B ⦄ = cheat

-- This seems to cause a loop in the instance resolution because of the η law for ⊤
-- module _ {i j} where
--   instance
--     IsSet-⊤ : Id-Intro.IsSet (Id-Intro-⊤ {i} {j}) _
--     IsSet-⊤ = _

------------------------------------------------------------
--- "Bidirectional" identity type elimination structures ---
------------------------------------------------------------
module Id-Elim↕ {ic jc id jd} (C : Fam {ic} {jc}) ⦃ CId : Id-Intro C ⦄ ⦃ CId-Elim-C : Id-Elim C C ⦄
                (D : Fam {id} {jd}) ⦃ DId : Id-Intro D ⦄ ⦃ CId-Elim-D : Id-Elim C D ⦄ ⦃ DId-Elim-D : Id-Elim D D ⦄ (_ : ⊤ {lzero}) where
  private
    open Id-Tele-r C
    open Id-Tele-r D
    module C           = Fam C
    module CId         = IdM C _
    module D           = Fam D
    module DIdM        = IdM D _
    module CCId-Elim-D = Id-ElimM (C ∗ C) D _

  J↕ : ∀ {A x} (P : CId.Singl {A} x → D.Ty) yp (d : D.Tm (P yp)) zq → D.Tm (P zq)
  J↕ {A} {x} P _ d zq = CCId-Elim-D.isContr-transp (isContr-PathFrom x) P zq d

  J↕-β : ∀ {A x} (P : CId.Singl {A} x → D.Ty) yp (d : D.Tm (P yp)) → D.Tm (DIdM.Id (J↕ P yp d yp) d)
  J↕-β {A} {x} P yp d = CCId-Elim-D.isContr-transp-β _ _ _

------------------------------------------------------------------------
--- Parametrized (or Frobenius) identity type elimination structures ---
------------------------------------------------------------------------
record Id-Elim-Param {ic jc id jd ie je} (C : Fam {ic} {jc}) ⦃ CId : Id-Intro C ⦄
                     (D : Fam {id} {jd})
                     (E : Fam {ie} {je}) ⦃ EId : Id-Intro E ⦄ : Set (ic ⊔ jc ⊔ id ⊔ jd ⊔ ie ⊔ je) where
  private
    module C   = Fam C
    module CId = Id-Intro CId
    module D   = Fam D
    module E   = Fam E
    module EId = Id-Intro EId

  field J : ∀ {A : C.Ty} {x : C.Tm A} (B : CId.Singl x → D.Ty)
              (P : ∀ yp (b : D.Tm (B yp)) → E.Ty) (d : ∀ b → E.Tm (P CId.center b))
              yp b
            → E.Tm (P yp b)
        J-β : ∀ {A : C.Ty} {x : C.Tm A} {B : CId.Singl x → D.Ty}
                {P : ∀ yp (b : D.Tm (B yp)) → E.Ty} {d : ∀ b → E.Tm (P CId.center b)}
                {b}
              → E.Tm (EId.Id (J B P d _ _) (d b))

  transp : ∀ {A : C.Ty} {x : C.Tm A} (B : C.Tm A → D.Ty)
             (P : ∀ y (b : D.Tm (B y)) → E.Ty) (d : ∀ b → E.Tm (P x b))
             {y} (p : C.Tm  (CId.Id x y)) b
         → E.Tm (P y b)
  transp B P d p b = J (λ (y , _) → B y) (λ (y , _) b → P y b) d (_ , p) b

  transp-β : ∀ {A : C.Ty} {x : C.Tm A} {B : C.Tm A → D.Ty}
             {P : ∀ y (b : D.Tm (B y)) → E.Ty} {d : ∀ b → E.Tm (P x b)}
             {b}
           → E.Tm (EId.Id (transp B P d CId.idp b) (d b))
  transp-β = J-β

module Id-Elim-ParamM {ic jc id jd ie je} (C : Fam {ic} {jc}) ⦃ CId : Id-Intro C ⦄ ⦃ CId-Elim-C : Id-Elim C C ⦄
                      (D : Fam {id} {jd})
                      (E : Fam {ie} {je}) ⦃ EId : Id-Intro E ⦄ ⦃ CId-Elim-E : Id-Elim C E ⦄ ⦃ EId-Elim-E : Id-Elim E E ⦄ ⦃ CId-Elim-E-Param-D : Id-Elim-Param C D E ⦄ (_ : ⊤ {lzero}) where
  private
    module C          = Fam C
    module CId        = IdM C _
    module D          = Fam D
    module E          = Fam E
    module EId        = IdM E _
    module CId-Elim-E = Id-ElimM C E _

  open Id-Elim-Param CId-Elim-E-Param-D public

  abstract
    transp-trans : ∀ {A : C.Ty} {x : C.Tm A} {B : C.Tm A → D.Ty} {P : ∀ x → D.Tm (B x) → E.Ty}
                     {e : ∀ d → E.Tm (P x d)} {y z} {p : C.Tm (CId.Id x y)} {q : C.Tm (CId.Id y z)} {d}
                   → E.Tm (EId.Id (transp B P (λ d' → transp B P e p d') q d) (transp B P e (CId.trans p q) d))
    transp-trans {A} {x} {B} {P} {e} {y} {z} {p} {q} {d}
      = J (λ (y , _) → B y) (λ (_ , q) d → EId.Id (transp B P (λ d' → transp B P e p d') q d) (transp B P e (CId.trans p q) d))
         (λ d → EId.trans transp-β (EId.sym (CId-Elim-E.ap (λ k → transp B P e k d) CId.trans-β-r)))
         (_ , q) d

  module _ {A} (cA : CId.isContr A) (P : C.Tm A → D.Ty) (Q : ∀ a → D.Tm (P a) → E.Ty) where
    abstract
      isContr-transp : ∀ {x} y (e : ∀ d → E.Tm (Q x d)) → (∀ d → E.Tm (Q y d))
      isContr-transp y e d = transp P Q e (CId.isContr⇒allPaths cA _ _) d

      isContr-transp-β : ∀ {x} (e : ∀ d → E.Tm (Q x d)) d → E.Tm (EId.Id (isContr-transp x e d) (e d))
      isContr-transp-β e d = EId.trans (CId-Elim-E.ap (λ k → transp P Q e k d) (CId.isContr⇒allPaths (CId.allPaths⇒isProp (CId.isContr⇒allPaths cA) _ _) _ _))
                             transp-β

      isContr-transp-trans : ∀ {x y z} (e : ∀ d → E.Tm (Q x d)) d → E.Tm (EId.Id (isContr-transp z (λ d' → isContr-transp y e d') d) (isContr-transp z e d))
      isContr-transp-trans e d = EId.trans transp-trans
                                 (CId-Elim-E.ap (λ k → transp P Q e k d) (CId.isContr⇒allPaths (CId.allPaths⇒isProp (CId.isContr⇒allPaths cA) _ _) _ _))


-----------------------------------------------------------------------
--- Derivation of parametrized identity type elimination structures ---
-----------------------------------------------------------------------
module _ {ic jc id jd ie je} {C : Fam {ic} {jc}} ⦃ CId : Id-Intro C ⦄ ⦃ CId-Elim-C : Id-Elim C C ⦄
         {D : Fam {id} {jd}} ⦃ DId : Id-Intro D ⦄ ⦃ CId-Elim-D : Id-Elim C D ⦄ ⦃ DId-Elim-D : Id-Elim D D ⦄
         {E : Fam {ie} {je}} ⦃ EId : Id-Intro E ⦄ ⦃ CId-Elim-E : Id-Elim C E ⦄ ⦃ DId-Elim-E : Id-Elim D E ⦄ ⦃ EId-Elim-E : Id-Elim E E ⦄ where
  private
    module C           = Fam C
    module CId         = IdM C _
    module CId-Elim-D  = Id-ElimM C D _
    module CId-Elim↕-D = Id-Elim↕ C D _
    module E           = Fam E
    module EId         = IdM E _
    module DId-Elim-E  = Id-ElimM D E _
    module CId-Elim-E  = Id-ElimM C E _

  abstract
    instance
      Id-Elim⇒Id-Elim-Param : Id-Elim-Param C D E
      Id-Elim⇒Id-Elim-Param .Id-Elim-Param.J {A} {x} B P d yp b = d₂ where
        b₀ = CId-Elim↕-D.J↕ B _ b _
        d₁ = CId-Elim-E.J (λ zq → P zq (CId-Elim↕-D.J↕ B _ b _)) (d b₀) yp
        d₂ = DId-Elim-E.transp (P yp) d₁ (CId-Elim↕-D.J↕-β _ _ _)
      Id-Elim⇒Id-Elim-Param .Id-Elim-Param.J-β {A} {x} {B} {P} {d} {b} = d₂-β where
        b₀ = CId-Elim↕-D.J↕ B _ b _
        d₁ = CId-Elim-E.J (λ zq → P zq (CId-Elim↕-D.J↕ B _ b _)) (d b₀) _
        d₁-β = CId-Elim-E.J-β {P = λ zq → P zq (CId-Elim↕-D.J↕ B _ b _)} {d b₀}
        d₂ = DId-Elim-E.transp (P _) d₁ (CId-Elim↕-D.J↕-β _ _ _)
        d₂-β : E.Tm (EId.Id d₂ (d b))
        d₂-β = EId.trans (EId.ap (λ k → DId-Elim-E.transp (P _) k _) d₁-β)
               (DId-Elim-E.J (λ (z , q) → EId.Id (DId-Elim-E.transp (P _) (d b₀) q) (d z))
                             DId-Elim-E.transp-β _)