Home
module category-theory.category-identity where
Imports
open import foundations.universe
open import foundations.identity-type
open import foundations.proposition
open import foundations.function-extensionality
open import foundations.set
open import foundations.proposition-h-level
open import category-theory.category
private variable o h : Level
module _ (e : FunExtAll) where
isPropIsCategory : (𝒞 : CategoryData o h) → isProp (isCategory 𝒞)
isPropIsCategory 𝒞 a b = q
where
open CategoryData 𝒞
module a = isCategory a
module b = isCategory b
p1 : Id (∀ {A B} (f : Hom A B) → _) a.identˡ b.identˡ
p1 = byFunExtImplicit e _ _ λ A → byFunExtImplicit e _ _ λ B → byFunExtType e _ _ (λ f → a.is-set-hom _ f _ _)
p2 : Id (∀ {A B} (f : Hom A B) → _) a.identʳ b.identʳ
p2 = byFunExtImplicit e _ _ λ A → byFunExtImplicit e _ _ λ B → byFunExtType e _ _ (λ f → a.is-set-hom _ f _ _)
p3 : Id (∀ A → _) a.ident² b.ident²
p3 = byFunExtType e _ _ λ A → a.is-set-hom _ _ _ _
p4 : Id (∀ {A B C D} {f : Hom A B} {g} {h : Hom C D} → (h ∘ g) ∘ f ＝ h ∘ (g ∘ f)) a.assoc b.assoc
p4 = byFunExtImplicit e _ _ (λ A → byFunExtImplicit e _ _ (λ B → byFunExtImplicit e _ _ (λ C → byFunExtImplicit e _ _ (λ D → byFunExtImplicit e _ _ (λ f → byFunExtImplicit e _ _ (λ g → byFunExtImplicit e _ _ (λ h → a.is-set-hom _ _ _ _)))))))
p5 : Id (∀ {A B C D} {f : Hom A B} {g} {h : Hom C D} → h ∘ (g ∘ f) ＝ (h ∘ g) ∘ f) a.sym-assoc b.sym-assoc
p5 = byFunExtImplicit e _ _ (λ A → byFunExtImplicit e _ _ (λ B → byFunExtImplicit e _ _ (λ C → byFunExtImplicit e _ _ (λ D → byFunExtImplicit e _ _ (λ f → byFunExtImplicit e _ _ (λ g → byFunExtImplicit e _ _ (λ h → a.is-set-hom _ _ _ _)))))))
p6 : Id (∀ {A B} → isSet (Hom A B)) a.is-set-hom b.is-set-hom
p6 = byFunExtImplicit e _ _ (λ A → byFunExtImplicit e _ _ (λ B → isPropIsSet e _ _))
q : a ＝ b
q with p1 | p2 | p3 | p4 | p5 | p6
q | refl | refl | refl | refl | refl | refl = refl