open import Cat.Instances.Functor
open import Cat.Functor.Base
open import Cat.Prelude

open import Data.Bool

import Cat.Reasoning

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!
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  _ _) (hlevel  _ _)
0≅1-iso-contr _ _ .paths p =
  0≅1.≅-pathp refl refl refl

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!
-- ```

-- # 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`{.Agda} and `false`{.Agda}!

-- ```agda
-- 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`{.Agda}
-- into some category $\cC$ are equivalent to isomorphisms in $\cC$.

-- ```agda
-- Isos : ∀ {o ℓ} → Precategory o ℓ → Type (o ⊔ ℓ)
-- Isos 𝒞 = Σ[ A ∈ 𝒞.Ob ] Σ[ B ∈ 𝒞.Ob ] (A 𝒞.≅ B)
--   where module 𝒞 = Cat.Reasoning 𝒞
-- ```

-- To prove this, we fix some category $\cC$, and construct an
-- isomorphism between functors out of `0≅1`{.Agda} and isomorphisms
-- in $\cC$.

-- ```agda
-- 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`{.Agda} are isomorphic to construct an iso between `true`{.Agda}
-- and `false`{.Agda}, and then use the fact that functors preserve
-- isomorphisms to obtain an isomorphism in $\cC$.

-- ```agda
--   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 $X \cong Y$
-- in $\cC$. Our functor will map `true`{.Agda} to $X$, and `false`
-- to $Y$: 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.

-- ```agda
--   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} _ = to isom
--       fun .F₁ {false} {true} _ = from isom
--       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 $ invr isom
--       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 $ invl isom
--       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!

-- ```agda
--   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-id F)
--            ; {true} {false} tt → refl
--            ; {false} {true} tt → refl
--            ; {false} {false} tt → sym (F-id F) })

--     linv : is-left-inverse functor→iso iso→functor
--     linv F = Σ-pathp refl $ Σ-pathp refl $ 𝒞.≅-pathp refl refl refl
-- ```