module Cat.Instances.Shape.Isomorphism where
The isomorphism category🔗
The isomorphism category is the category with two points, along with a unique isomorphism between them.
0≅1 : Precategory lzero lzero 0≅1 .Precategory.Ob = Bool 0≅1 .Precategory.Hom _ _ = ⊤ 0≅1 .Precategory.Hom-set _ _ = hlevel 2 0≅1 .Precategory.id = tt 0≅1 .Precategory._∘_ tt tt = tt 0≅1 .Precategory.idr tt i = tt 0≅1 .Precategory.idl tt i = tt 0≅1 .Precategory.assoc tt tt tt i = tt
Note that the space of isomorphisms between any 2 objects is contractible.
0≅1-iso-contr : ∀ X Y → is-contr (Isomorphism 0≅1 X Y) 0≅1-iso-contr _ _ .centre = 0≅1.make-iso tt tt (hlevel 1 _ _) (hlevel 1 _ _) 0≅1-iso-contr _ _ .paths p = trivial!
The isomorphism category is strict, as its objects form a set.
0≅1-is-strict : is-set 0≅1.Ob 0≅1-is-strict = hlevel 2
The isomorphism category is not univalent🔗
The isomorphism category is the canonical example of a non-univalent
category. If it were univalent, then we’d get a path between true and false!
0≅1-not-univalent : ¬ is-category 0≅1 0≅1-not-univalent is-cat = true≠false $ is-cat .to-path $ 0≅1-iso-contr true false .centre
Functors out of the isomorphism category🔗
One important fact about the isomorphism category is that it
classifies isomorphisms in categories, in the sense that functors out of
0≅1 into
some category
are equivalent to isomorphisms in
Isos : ∀ {o ℓ} → Precategory o ℓ → Type (o ⊔ ℓ) Isos 𝒞 = Σ[ A ∈ 𝒞 ] Σ[ B ∈ 𝒞 ] (A 𝒞.≅ B) where module 𝒞 = Cat.Reasoning 𝒞
To prove this, we fix some category
and construct an isomorphism between functors out of 0≅1 and
isomorphisms in
module _ {o ℓ} {𝒞 : Precategory o ℓ} where private module 𝒞 = Cat.Reasoning 𝒞 open Functor open 𝒞._≅_
For the forward direction, we use the fact that all objects in 0≅1 are
isomorphic to construct an iso between true and false, and then use the
fact that functors preserve isomorphisms to obtain an isomorphism in
functor→iso : (F : Functor 0≅1 𝒞) → Isos 𝒞 functor→iso F = _ , _ , F-map-iso F (0≅1-iso-contr true false .centre)
For the backwards direction, we are given an isomorphism
in
Our functor will map true to
and false to
this is somewhat arbitrary, but lines up with our choices for the
forward direction. We then perform a big case bash to construct the
mapping of morphisms, and unpack the components of the provided
isomorphism into place. Functoriality follows by the fact that the
provided isomorphism is indeed an isomorphism.
iso→functor : Isos 𝒞 → Functor 0≅1 𝒞 iso→functor (X , Y , isom) = fun where fun : Functor _ _ fun .F₀ true = X fun .F₀ false = Y fun .F₁ {true} {true} _ = 𝒞.id fun .F₁ {true} {false} _ = isom .to fun .F₁ {false} {true} _ = isom .from fun .F₁ {false} {false} _ = 𝒞.id fun .F-id {true} = refl fun .F-id {false} = refl fun .F-∘ {true} {true} {z} f g = sym $ 𝒞.idr _ fun .F-∘ {true} {false} {true} f g = sym $ isom .invr fun .F-∘ {true} {false} {false} f g = sym $ 𝒞.idl _ fun .F-∘ {false} {true} {true} f g = sym $ 𝒞.idl _ fun .F-∘ {false} {true} {false} f g = sym $ isom .invl fun .F-∘ {false} {false} {z} f g = sym $ 𝒞.idr _
Showing that this function is an equivalence is relatively simple: the only tricky part is figuring out which lemmas to use to characterise path spaces!
iso≃functor : is-equiv iso→functor iso≃functor = is-iso→is-equiv (iso functor→iso rinv linv) where rinv : is-right-inverse functor→iso iso→functor rinv F = Functor-path (λ { true → refl ; false → refl }) (λ { {true} {true} _ → sym (F .F-id) ; {true} {false} tt → refl ; {false} {true} tt → refl ; {false} {false} tt → sym (F .F-id) }) linv : is-left-inverse functor→iso iso→functor linv F = Σ-pathp refl $ Σ-pathp refl $ trivial!