module Id.Elim where

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

open import Id.Intro

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

record Id-Elim (C : Fam) ⦃ CId : Id-Intro C ⦄
               (D : Fam) ⦃ DId : Id-Intro D ⦄ : Set where
  private
    module CId = Id-Intro CId
    module DId = Id-Intro DId

  field J : ∀ {A : C .Ty} {x : C .Tm A} (P : CId.IdFrom x → D .Ty)
              (d : D .Tm (P CId.IdFrom-center)) (yp : CId.IdFrom x)
              → D .Tm (P yp)
        J-β : ∀ {A : C .Ty} {x : C .Tm A} {P : CId.IdFrom x → D .Ty}
                {d : D .Tm (P CId.IdFrom-center)}
              → D .Tm (DId.Id (J P d CId.IdFrom-center) d)

  abstract
    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 (CId.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 CId.idp) d)
    transp-β = J-β

  abstract
    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

    ap-β : ∀ {A B} {f : C .Tm A → D .Tm B} {x : C .Tm A} → D .Tm (DId.Id (ap f {x = x} CId.idp) DId.idp)
    ap-β = transp-β