open import category-theory.category
module category-theory.isomorphism {o h} (𝒞 : Category o h) where
open import foundations.universe open import foundations.identity-type open import foundations.groupoid-laws open import foundations.identity-type-reasoning open import foundations.proposition open import foundations.functions-are-functors open import foundations.transport open import foundations.sigma-type open Category 𝒞
private variable A B : Ob
record isIso (f : Hom A B) : Type h where
field
g : Hom B A
invˡ : g ∘ f ＝ id A
invʳ : f ∘ g ＝ id B
Iso : Ob → Ob → Type h
Iso A B = Σ (Hom A B) isIso
「同型射である」ということは命題である。
isPropIsIso : (f : Hom A B) → isProp (isIso f)
isPropIsIso {A = A} {B = B} f I J = q
where
module I = isIso I
module J = isIso J
p1 : I.g ＝ J.g
p1 =
I.g
＝⟨ sym (identʳ I.g) ⟩
I.g ∘ id B
＝⟨ ap (I.g ∘_) (sym J.invʳ) ⟩
I.g ∘ (f ∘ J.g)
＝⟨ sym assoc ⟩
(I.g ∘ f) ∘ J.g
＝⟨ ap (_∘ J.g) I.invˡ ⟩
id A ∘ J.g
＝⟨ identˡ J.g ⟩
J.g
∎
p2 : subst (λ g → g ∘ f ＝ id A) p1 I.invˡ ＝ J.invˡ
p2 = is-set-hom _ _ _ _
p3 : subst (λ g → f ∘ g ＝ id B) p1 I.invʳ ＝ J.invʳ
p3 = is-set-hom _ _ _ _
q : I ＝ J
q with p1 | p2 | p3
... | refl | refl | refl = refl