{-# OPTIONS --postfix-projections --prop #-}
module Id where
open import Agda.Primitive
open import Lib
open import Fam as _
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
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
module IdM {ic jc} (C : Fam {ic} {jc}) ⦃ CId : Id-Intro C ⦄ ⦃ CId-Elim-C : Id-Elim C C ⦄ (_ : ⊤ {lzero}) where
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 _)
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) _ _) _ _))