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!