open import Cat.Functor.Equivalence
open import Cat.Functor.Naturality
open import Cat.Functor.Univalence
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Functor.Reasoning as Fr
import Cat.Reasoning as Cr

module
{o β o' β'} {C : Precategory o β} {D : Precategory o' β'}
where

private
module C = Cr C
module D = Cr D


Let be a functor participating in two adjunctions and Using the data from both adjunctions, we can exhibit a natural isomorphism which additionally preserves the unit and counit: Letting be the components of the natural isomorphism, we have idem for

module _ {F : Functor C D} {G G' : Functor D C} (a : F β£ G) (a' : F β£ G') where
private
module F = Fr F
module G = Fr G
module G' = Fr G'
module a = _β£_ a
module a' = _β£_ a'
open a.unit using (Ξ·)
open a.counit using (Ξ΅)
open a'.unit hiding (is-natural) renaming (Ξ· to Ξ·')
open a'.counit hiding (is-natural) renaming (Ξ΅ to Ξ΅')
open make-natural-iso


The isomorphism is defined (in components) to be with inverse Here, we show the construction of both directions, cancellation in one directly, and naturality (naturality for the inverse is taken care of by make-natural-iso). Cancellation in the other direction is exactly analogous, and so was omitted.

  private
make-GβG' : make-natural-iso G G'
make-GβG' .eta x = G'.β (Ξ΅ x) C.β Ξ·' _
make-GβG' .inv x = G.β (Ξ΅' x) C.β Ξ· _
make-GβG' .invβeta x =
(G.β (Ξ΅' x) C.β Ξ· _) C.β G'.β (Ξ΅ _) C.β Ξ·' _    β‘β¨ C.extendl (C.pullr (a.unit.is-natural _ _ _) β G.pulll (a'.counit.is-natural _ _ _)) β©β‘
G.β (Ξ΅ x D.β Ξ΅' _) C.β Ξ· _ C.β Ξ·' _             β‘β¨ C.reflβ©ββ¨ a.unit.is-natural _ _ _ β©β‘
G.β (Ξ΅ x D.β Ξ΅' _) C.β G.β (F.β (Ξ·' _)) C.β Ξ· _ β‘β¨ G.pulll (D.cancelr a'.zig) β©β‘
G.β (Ξ΅ x) C.β Ξ· _                               β‘β¨ a.zag β©β‘
C.id                                            β
make-GβG' .natural x y f =
G'.β f C.β G'.β (Ξ΅ x) C.β Ξ·' _               β‘β¨ C.pulll (G'.weave (sym (a.counit.is-natural _ _ _))) β©β‘
(G'.β (Ξ΅ y) C.β G'.β (F.β (G.β f))) C.β Ξ·' _ β‘β¨ C.extendr (sym (a'.unit.is-natural _ _ _)) β©β‘
(G'.β (Ξ΅ y) C.β Ξ·' _) C.β G.β f              β

    make-GβG' .etaβinv x =
C.extendl (C.pullr (a'.unit.is-natural _ _ _))
Β·Β· apβ C._β_ refl (C.pushl (sym (a'.unit.is-natural _ _ _)))
Β·Β· C.extend-inner (a'.unit.is-natural _ _ _)
Β·Β· G'.extendl (a.counit.is-natural _ _ _)
Β·Β· apβ C._β_ refl ( apβ C._β_ refl (a'.unit.is-natural _ _ _)
β G'.cancell a.zig)
β a'.zag


The data above is exactly what we need to define a natural isomorphism Showing that this isomorphism commutes with the adjunction natural transformations is a matter of calculating:

  right-adjoint-unique : Cr.Isomorphism Cat[ D , C ] G G'

abstract
unique-preserves-unit
: β {x} β make-GβG' .eta _ C.β Ξ· x β‘ Ξ·' x
unique-preserves-unit =
make-GβG' .eta _ C.β Ξ· _                 β‘β¨ C.pullr (a'.unit.is-natural _ _ _) β©β‘
G'.β (Ξ΅ _) C.β G'.β (F.β (Ξ· _)) C.β Ξ·' _ β‘β¨ G'.cancell a.zig β©β‘
Ξ·' _                                     β

unique-preserves-counit
: β {x} β Ξ΅ _ D.β F.β (make-GβG' .inv _) β‘ Ξ΅' x
unique-preserves-counit =
Ξ΅ _ D.β F.β (make-GβG' .inv _)         β‘β¨ D.reflβ©ββ¨ F.F-β _ _ β©β‘
Ξ΅ _ D.β F.β (G.β (Ξ΅' _)) D.β F.β (Ξ· _) β‘β¨ D.extendl (a.counit.is-natural _ _ _) β©β‘
Ξ΅' _ D.β Ξ΅ _ D.β F.β (Ξ· _)             β‘β¨ D.elimr a.zig β©β‘
Ξ΅' _                                   β


If the codomain category is furthermore univalent, so that natural isomorphisms are an identity system on the functor category we can upgrade the isomorphism to an identity and preservation of the adjunction data means this identity can be improved to an identification between pairs of the functors and their respective adjunctions.

is-left-adjoint-is-prop
: is-category C
β (F : Functor C D)
β is-prop $Ξ£[ G β Functor D C ] (F β£ G) is-left-adjoint-is-prop cc F (G , a) (G' , a') i = Gβ‘G' cd i , aβ‘a' cd i   where Gβ G' = right-adjoint-unique a a' cd = Functor-is-category cc open _β£_ open _=>_ open Functor module F = Fr F module _ (d : is-category Cat[ D , C ]) where Gβ‘G' = d .to-path Gβ G' abstract same-eta : PathP (Ξ» i β Id => Gβ‘G' i Fβ F) (a .unit) (a' .unit) same-eta = Nat-pathp refl (Ξ» i β Gβ‘G' i Fβ F) Ξ» x β Hom-pathp-reflr C$
apβ C._β_ (whisker-path-left {G = G} {G'} {F = F} d GβG') refl
β unique-preserves-unit a a'

same-eps : PathP (Ξ» i β F Fβ Gβ‘G' i => Id) (a .counit) (a' .counit)
same-eps = Nat-pathp (Ξ» i β F Fβ Gβ‘G' i) refl
Ξ» x β Hom-pathp-refll D $apβ D._β_ refl (whisker-path-right {G = F} {F = G} {G'} d Gβ G') β unique-preserves-counit a a' aβ‘a' : PathP (Ξ» i β F β£ Gβ‘G' i) a a' aβ‘a' i .unit = same-eta i aβ‘a' i .counit = same-eps i aβ‘a' i .zig {A} = is-setβsquarep (Ξ» i j β D.Hom-set (F.β A) (F.β A)) (Ξ» i β same-eps i .Ξ· (F.β A) D.β F.β (same-eta i .Ξ· A)) (a .zig) (a' .zig) refl i aβ‘a' i .zag {A} = is-setβsquarep (Ξ» i j β C.Hom-set (Gβ‘G' i .Fβ A) (Gβ‘G' i .Fβ A)) (Ξ» i β Gβ‘G' i .Fβ (same-eps i .Ξ· A) C.β same-eta i .Ξ· (Gβ‘G' i .Fβ A)) (a .zag) (a' .zag) (Ξ» _ β C.id) i  As a corollary, we conclude that, for a functor from a univalent category βbeing an equivalence of categoriesβ is a proposition. open is-equivalence is-equivalence-is-prop : is-category C β (F : Functor C D) β is-prop (is-equivalence F) is-equivalence-is-prop ccat F x y = go where invs = ap fst$
is-left-adjoint-is-prop ccat F (x .Fβ»ΒΉ , x .Fβ£Fβ»ΒΉ) (y .Fβ»ΒΉ , y .Fβ£Fβ»ΒΉ)

is-left-adjoint-is-prop ccat F (x .Fβ»ΒΉ , x .Fβ£Fβ»ΒΉ) (y .Fβ»ΒΉ , y .Fβ£Fβ»ΒΉ)

go : x β‘ y
go i .Fβ»ΒΉ = invs i
go i .Fβ£Fβ»ΒΉ = adjs i
go i .unit-iso a =
is-propβpathp (Ξ» i β C.is-invertible-is-prop {f = _β£_.Ξ· (adjs i) a})
(x .unit-iso a)
(y .unit-iso a) i
go i .counit-iso a =
is-propβpathp (Ξ» i β D.is-invertible-is-prop {f = _β£_.Ξ΅ (adjs i) a})
(x .counit-iso a)
(y .counit-iso a) i