module Cat.Displayed.Functor.Equivalence where
Equivalences of displayed categories🔗
Suppose are the adjoint components of an adjoint equivalence and let and be categories displayed over its endpoints. If (resp. are displayed functors in a displayed adjunction we say it is a displayed adjoint equivalence, or simply equivalence of displayed categories, if its unit and counit maps are displayed natural isomorphisms.
record adjunction-is-equivalence[_]
{oa ℓa ob ℓb oe ℓe of ℓf} {A : Precategory oa ℓa} {B : Precategory ob ℓb} {ℰ : Displayed A oe ℓe} {ℱ : Displayed B of ℓf} {F : Functor A B} {F⁻¹ : Functor B A} {F⊣F⁻¹ : F ⊣ F⁻¹}
(F⊣F⁻¹-is-equivalence : adjunction-is-equivalence F⊣F⁻¹) {F' : Displayed-functor F ℰ ℱ} {F'⁻¹ : Displayed-functor F⁻¹ ℱ ℰ} (F'⊣F'⁻¹ : F' ⊣[ F⊣F⁻¹ ] F'⁻¹) : Type (adj-level' ℰ ℱ) where open adjunction-is-equivalence F⊣F⁻¹-is-equivalence open _⊣[_]_ F'⊣F'⁻¹
private module F = Functor F module F⁻¹ = Functor F⁻¹ module A = Cr A module B = Cr B module ℰ = Dr ℰ module ℱ = Dr ℱ [ℰ,ℰ] = DisCat[ ℰ , ℰ ] [ℱ,ℱ] = DisCat[ ℱ , ℱ ] module [ℰ,ℰ] = Dr [ℰ,ℰ] module [ℱ,ℱ] = Dr [ℱ,ℱ] module F' = Displayed-functor F' module F'⁻¹ = Displayed-functor F'⁻¹
field unit'-iso : ∀ {x} x' → ℰ.is-invertible[ unit-iso x ] (unit' .η' x') counit'-iso : ∀ {x} x' → ℱ.is-invertible[ counit-iso x ] (counit' .η' x')
Again, we see that natural families of invertible morphisms give rise to displayed isomorphisms in the displayed functor category:
F'∘F'⁻¹≅Id' : F' F∘' F'⁻¹ [ℱ,ℱ].≅[ F∘F⁻¹≅Id ] Id' F'∘F'⁻¹≅Id' = [ℱ,ℱ].invertible[]→iso[] $ invertible[]→invertibleⁿ[ _ ] counit' counit'-iso Id'≅F'⁻¹∘'F' : Id' [ℰ,ℰ].≅[ Id≅F⁻¹∘F ] F'⁻¹ F∘' F' Id'≅F'⁻¹∘'F' = [ℰ,ℰ].invertible[]→iso[] $ invertible[]→invertibleⁿ[ _ ] unit' unit'-iso unit'⁻¹ = [ℰ,ℰ].from' Id'≅F'⁻¹∘'F' counit'⁻¹ = [ℱ,ℱ].from' F'∘F'⁻¹≅Id'
This implies the displayed adjunction
F'⁻¹⊣F' : F'⁻¹ ⊣[ F⁻¹⊣F ] F'
whence we have
inverse-is-equivalence' : adjunction-is-equivalence[ inverse-is-equivalence ] F'⁻¹⊣F'
Construction of F'⁻¹⊣F' and inverse-equivalence'
F'⁻¹⊣F' ._⊣[_]_.unit' = counit'⁻¹ F'⁻¹⊣F' ._⊣[_]_.counit' = unit'⁻¹ F'⁻¹⊣F' ._⊣[_]_.zig' {b} {b'} = z' where z' : unit'⁻¹ .η' (F'⁻¹.₀' b') ℰ.∘' F'⁻¹.₁' (counit'⁻¹ .η' b') ℰ.≡[ _⊣_.zig F⁻¹⊣F ] ℰ.id' z' = ℰ.cast[] $ ℰ.inverse-unique₀' (F'-map-iso F'⁻¹ (isoⁿ[]→iso[] F'∘F'⁻¹≅Id' b') ℰ.∘Iso' isoⁿ[]→iso[] Id'≅F'⁻¹∘'F' (F'⁻¹.₀' b')) ℰ.id-iso↓ zag' F'⁻¹⊣F' ._⊣[_]_.zag' {a} {a'} = z' where z' : F'.₁' (unit'⁻¹ .η' a') ℱ.∘' counit'⁻¹ .η' (F'.₀' a') ℱ.≡[ _⊣_.zag F⁻¹⊣F ] ℱ.id' z' = ℱ.cast[] $ ℱ.inverse-unique₀' (isoⁿ[]→iso[] F'∘F'⁻¹≅Id' (F'.₀' a') ℱ.∘Iso' F'-map-iso F' (isoⁿ[]→iso[] Id'≅F'⁻¹∘'F' a')) ℱ.id-iso↓ zig' inverse-is-equivalence' = record { unit'-iso = λ x' → ℱ.is-invertible[]-inverse $ counit'-iso x' ; counit'-iso = λ x' → ℰ.is-invertible[]-inverse $ unit'-iso x' }
Again we overload terminology and call a displayed functor an equivalence of displayed categories or displayed equivalence when it is part of a displayed adjoint equivalence
record is-equivalence[_]
{oa ℓa ob ℓb oe ℓe of ℓf} {A : Precategory oa ℓa} {B : Precategory ob ℓb} {ℰ : Displayed A oe ℓe} {ℱ : Displayed B of ℓf} {F : Functor A B}
(F-is-equiv : is-equivalence F) (F' : Displayed-functor F ℰ ℱ) : Type (adj-level' ℰ ℱ) where open is-equivalence F-is-equiv public
field F'⁻¹ : Displayed-functor F⁻¹ ℱ ℰ F'⊣F'⁻¹ : F' ⊣[ F⊣F⁻¹ ] F'⁻¹ has-is-equivalence' : adjunction-is-equivalence[ has-is-equivalence ] F'⊣F'⁻¹
As with an ordinary equivalence of categories there are other ways of characterising displayed equivalences which will usually be more convenient when it comes to constructing equivalences by hand.
Fully faithful, essentially surjective🔗
Here we give the displayed analogue of ff+split-eso→is-equivalence,
requiring a similarly Herculean effort. Suppose
is a displayed functor over a fully
faithful and split essentially
surjective base functor
so that
is fully
faithfully displayed and essentially split
surjective over
module _
{oa ℓa ob ℓb oe ℓe of ℓf} {A : Precategory oa ℓa} {B : Precategory ob ℓb} {ℰ : Displayed A oe ℓe} {ℱ : Displayed B of ℓf} {F : Functor A B} {F' : Displayed-functor F ℰ ℱ}
(ff : is-fully-faithful F) {eso : is-split-eso F} (ff' : is-ff[] F') (eso' : is-split-eso[ eso ] F') where private module ff[ff]+split-eso[]→is-equivalence[] where F-is-equiv = ff+split-eso→is-equivalence {F = F} ff eso open is-equivalence F-is-equiv
module A = Cr A module B = Cr B module ℰ = Dr ℰ module ℱ = Dr ℱ module F = Functor F module F' = Displayed-functor F' module F⁻¹ = Functor F⁻¹ module ff {x} {y} = Equiv (F.F₁ , ff {x} {y})
We can use the inverse action ff'⁻¹ together with essential
surjectivity to define F'⁻¹:
open ff[ff] F' ff ff' F'⁻¹ : Displayed-functor F⁻¹ ℱ ℰ F'⁻¹ .F₀' b' = eso' b' .fst F'⁻¹ .F₁' {x} {y} {f} {x'} {y'} f' = ff'⁻¹ (ffy' ℱ.∘' f' ℱ.∘' ftx') where open Σ (eso' x') renaming (fst to f*x' ; snd to f*x'-iso) open Σ (eso' y') renaming (fst to f*y' ; snd to f*y'-iso) ftx' = f*x'-iso .ℱ.to' ffy' = f*y'-iso .ℱ.from' F'⁻¹ .F-id' {x} {x'} = ℰ.begin[] ff'⁻¹ (ffx' ℱ.∘' ⌜ ℱ.id' ℱ.∘' ftx' ⌝) ℰ.≡[]⟨ apd! (ℱ.idl' ftx') ⟩ℰ.≡[] ff'⁻¹ ⌜ ffx' ℱ.∘' ftx' ⌝ ℰ.≡[]⟨ apd! (f*x'-iso.invr') ⟩ℰ.≡[] ff'⁻¹ ⌜ ℱ.id' ⌝ ℰ.≡[]˘⟨ apd¡ (F' .F-id') ⟩ℰ.≡[]˘ ff'⁻¹ (F'.₁' ℰ.id') ℰ.≡[]⟨ η[] ℰ.id' ⟩ℰ.≡[] ℰ.id' ℰ.∎[] where open Σ (eso' x') renaming (fst to f*x' ; snd to f*x'-iso) module f*x'-iso = ℱ._≅[_]_ f*x'-iso ftx' = f*x'-iso.to' ffx' = f*x'-iso.from' F'⁻¹ .F-∘' {a' = x'} {y'} {z'} {f'} {g'} = ff[]→faithful[] F' ff' $ ℱ.begin[] F'.₁' (ff'⁻¹ (ffz' ℱ.∘' (f' ℱ.∘' g') ℱ.∘' ftx')) ℱ.≡[]⟨ ε[] (ffz' ℱ.∘' (f' ℱ.∘' g') ℱ.∘' ftx') ⟩ℱ.≡[] ffz' ℱ.∘' ⌜ (f' ℱ.∘' g') ℱ.∘' ftx' ⌝ ℱ.≡[]˘⟨ apd¡ (ℱ.assoc' f' g' ftx') ⟩ℱ.≡[]˘ ffz' ℱ.∘' f' ℱ.∘' ⌜ g' ℱ.∘' ftx' ⌝ ℱ.≡[]˘⟨ apd¡ (ℱ.idl' (g' ℱ.∘' ftx')) ⟩ℱ.≡[]˘ ffz' ℱ.∘' f' ℱ.∘' ⌜ ℱ.id' ⌝ ℱ.∘' g' ℱ.∘' ftx' ℱ.≡[]˘⟨ apd¡ (f*y'-iso .ℱ.invl') ⟩ℱ.≡[]˘ ffz' ℱ.∘' f' ℱ.∘' ⌜ (fty' ℱ.∘' ffy') ℱ.∘' g' ℱ.∘' ftx' ⌝ ℱ.≡[]˘⟨ apd¡ (ℱ.assoc' fty' ffy' (g' ℱ.∘' ftx')) ⟩ℱ.≡[]˘ ffz' ℱ.∘' ⌜ f' ℱ.∘' fty' ℱ.∘' (ffy' ℱ.∘' g' ℱ.∘' ftx') ⌝ ℱ.≡[]⟨ apd! (ℱ.assoc' f' fty' (ffy' ℱ.∘' g' ℱ.∘' ftx'))⟩ℱ.≡[] ffz' ℱ.∘' (f' ℱ.∘' fty') ℱ.∘' (ffy' ℱ.∘' g' ℱ.∘' ftx') ℱ.≡[]⟨ ℱ.assoc' ffz' (f' ℱ.∘' fty') (ffy' ℱ.∘' g' ℱ.∘' ftx') ⟩ℱ.≡[] ⌜ ffz' ℱ.∘' f' ℱ.∘' fty' ⌝ ℱ.∘' (ffy' ℱ.∘' g' ℱ.∘' ftx') ℱ.≡[]˘⟨ apd¡ (ε[] (ffz' ℱ.∘' f' ℱ.∘' fty')) ⟩ℱ.≡[]˘ F'.₁' (ff'⁻¹ (ffz' ℱ.∘' f' ℱ.∘' fty')) ℱ.∘' ⌜ ffy' ℱ.∘' g' ℱ.∘' ftx' ⌝ ℱ.≡[]˘⟨ apd¡ (ε[] (ffy' ℱ.∘' g' ℱ.∘' ftx')) ⟩ℱ.≡[]˘ F'.₁' (ff'⁻¹ (ffz' ℱ.∘' f' ℱ.∘' fty')) ℱ.∘' F'.₁' (ff'⁻¹ (ffy' ℱ.∘' g' ℱ.∘' ftx')) ℱ.≡[]˘⟨ F' .F-∘' {f' = (ff'⁻¹ (ffz' ℱ.∘' f' ℱ.∘' fty'))} {g' = (ff'⁻¹ (ffy' ℱ.∘' g' ℱ.∘' ftx'))}⟩ℱ.≡[]˘ F'.₁' (ff'⁻¹ (ffz' ℱ.∘' f' ℱ.∘' fty') ℰ.∘' ff'⁻¹ (ffy' ℱ.∘' g' ℱ.∘' ftx')) ℱ.∎[] where open Σ (eso' x') renaming (fst to f*x' ; snd to f*x'-iso) open Σ (eso' y') renaming (fst to f*y' ; snd to f*y'-iso) open Σ (eso' z') renaming (fst to f*z' ; snd to f*z'-iso) ffz' = f*z'-iso .ℱ.from' ffy' = f*y'-iso .ℱ.from' ftz' = f*z'-iso .ℱ.to' fty' = f*y'-iso .ℱ.to' ffx' = f*x'-iso .ℱ.from' ftx' = f*x'-iso .ℱ.to'
Defining the displayed unit, counit, and associated identities are all
given by straightforward (if tedious) adaptions of those for ff+split-eso→is-equivalence,
and are given without commentary.
module F'⁻¹ = Displayed-functor F'⁻¹ module F'⊣F'⁻¹ where open _=[_]=>_ unit' : Id' =[ unit ]=> F'⁻¹ F∘' F' unit' .η' x' = ff'⁻¹ ffx' where open Σ (eso' (F'.₀' x')) renaming (fst to f*x' ; snd to f*x'-iso) ffx' = f*x'-iso .ℱ.from' unit' .is-natural' x' y' f' = ff[]→faithful[] F' ff' $ ℱ.begin[] F'.₁' (η'y' ℰ.∘' f') ℱ.≡[]⟨ F'.F-∘' ⟩ℱ.≡[] F'.₁' (ff'⁻¹ ffy') ℱ.∘' F'.₁' f' ℱ.≡[]⟨ ε[] ffy' ℱ.⟩∘'⟨refl ⟩ℱ.≡[] ffy' ℱ.∘' F'.₁' f' ℱ.≡[]˘⟨ ℱ.refl⟩∘'⟨ ℱ.idr' _ ⟩ℱ.≡[]˘ ffy' ℱ.∘' F'.₁' f' ℱ.∘' ℱ.id' ℱ.≡[]˘⟨ ℱ.refl⟩∘'⟨ ℱ.refl⟩∘'⟨ f*x'-iso.invl' ⟩ℱ.≡[]˘ ffy' ℱ.∘' F'.₁' f' ℱ.∘' ftx' ℱ.∘' ffx' ℱ.≡[]⟨ (ℱ.refl⟩∘'⟨ ℱ.assoc' _ _ _ ) ℱ.∙[] ℱ.assoc' _ _ _ ⟩ℱ.≡[] (ffy' ℱ.∘' F'.₁' f' ℱ.∘' ftx') ℱ.∘' ffx' ℱ.≡[]˘⟨ ε[] _ ℱ.⟩∘'⟨ ε[] _ ⟩ℱ.≡[]˘ F'.₁' (ff'⁻¹ (ffy' ℱ.∘' F'.₁' f' ℱ.∘' ftx')) ℱ.∘' F'.₁' (ff'⁻¹ ffx') ℱ.≡[]˘⟨ F'.F-∘' ⟩ℱ.≡[]˘ F'.₁' (₁' (F'⁻¹ F∘' F') f' ℰ.∘' η'x') ℱ.∎[] where open Σ (eso' (F'.₀' x')) renaming (fst to f*x' ; snd to f*x'-iso) open Σ (eso' (F'.₀' y')) renaming (fst to f*y' ; snd to f*y'-iso) module f*x'-iso = ℱ._≅[_]_ f*x'-iso module f*y'-iso = ℱ._≅[_]_ f*y'-iso ffx' = f*x'-iso.from' ffy' = f*y'-iso.from' ftx' = f*x'-iso.to' η'x' = unit' .η' x' η'y' = unit' .η' y' counit' : F' F∘' F'⁻¹ =[ counit ]=> Id' counit' .η' x' = ftx' where open Σ (eso' x') renaming (fst to f*x' ; snd to f*x'-iso) ftx' = f*x'-iso .ℱ.to' counit' .is-natural' x' y' f' = ℱ.begin[] fty' ℱ.∘' F'.₁' (ff'⁻¹ (ffy' ℱ.∘' f' ℱ.∘' ftx')) ℱ.≡[]⟨ ℱ.refl⟩∘'⟨ ε[] _ ⟩ℱ.≡[] fty' ℱ.∘' ffy' ℱ.∘' f' ℱ.∘' ftx' ℱ.≡[]⟨ ℱ.cancell[] _ f*y'-iso.invl' ⟩ℱ.≡[] f' ℱ.∘' ftx' ℱ.∎[] where open Σ (eso' x') renaming (fst to f*x' ; snd to f*x'-iso) open Σ (eso' y') renaming (fst to f*y' ; snd to f*y'-iso) module f*x'-iso = ℱ._≅[_]_ f*x'-iso module f*y'-iso = ℱ._≅[_]_ f*y'-iso ffy' = f*y'-iso.from' ftx' = f*x'-iso.to' fty' = f*y'-iso.to' zig' : ∀ {x} {x' : ℰ.Ob[ x ]} → counit' .η' (F'.₀' x') ℱ.∘' F'.₁' (unit' .η' x') ℱ.≡[ zig ] ℱ.id' zig' {x' = x'} = ℱ.begin[] ftx' ℱ.∘' F'.₁' (ff'⁻¹ ffx') ℱ.≡[]⟨ ℱ.refl⟩∘'⟨ ε[] _ ⟩ℱ.≡[] ftx' ℱ.∘' ffx' ℱ.≡[]⟨ f*x'-iso.invl' ⟩ℱ.≡[] ℱ.id' ℱ.∎[] where open Σ (eso' (F'.₀' x')) renaming (fst to f*x' ; snd to f*x'-iso) module f*x'-iso = ℱ._≅[_]_ f*x'-iso ftx' = f*x'-iso.to' ffx' = f*x'-iso.from' zag' : ∀ {x} {x' : ℱ.Ob[ x ]} → F'⁻¹.₁' (counit' .η' x') ℰ.∘' unit' .η' (F'⁻¹.₀' x') ℰ.≡[ zag ] ℰ.id' zag' {x' = x'} = ff[]→faithful[] F' ff' $ ℱ.begin[] F'.₁' (ff'⁻¹ (ffx' ℱ.∘' ftx' ℱ.∘' fftx') ℰ.∘' ff'⁻¹ fffx') ℱ.≡[]⟨ F'.F-∘' ⟩ℱ.≡[] F'.F₁' (ff'⁻¹ (ffx' ℱ.∘' ftx' ℱ.∘' fftx')) ℱ.∘' F'.F₁' (ff'⁻¹ fffx') ℱ.≡[]⟨ ε[] _ ℱ.⟩∘'⟨ ε[] _ ⟩ℱ.≡[] (ffx' ℱ.∘' ftx' ℱ.∘' fftx') ℱ.∘' fffx' ℱ.≡[]⟨ (ℱ.assoc' _ _ _ ℱ.⟩∘'⟨refl) ⟩ℱ.≡[] ((ffx' ℱ.∘' ftx') ℱ.∘' fftx') ℱ.∘' fffx' ℱ.≡[]˘⟨ ℱ.assoc' _ _ _ ⟩ℱ.≡[]˘ (ffx' ℱ.∘' ftx') ℱ.∘' (fftx' ℱ.∘' fffx') ℱ.≡[]⟨ f*x'-iso.invr' ℱ.⟩∘'⟨ f*f*x'-iso.invl' ⟩ℱ.≡[] ℱ.id' ℱ.∘' ℱ.id' ℱ.≡[]⟨ ℱ.idl' _ ⟩ℱ.≡[] ℱ.id' ℱ.≡[]˘⟨ F'.F-id' ⟩ℱ.≡[]˘ F'.₁' ℰ.id' ℱ.∎[] where open Σ (eso' x') renaming (fst to f*x' ; snd to f*x'-iso) open Σ (eso' (F'.₀' f*x')) renaming (fst to f*f*x' ; snd to f*f*x'-iso) module f*x'-iso = ℱ._≅[_]_ f*x'-iso module f*f*x'-iso = ℱ._≅[_]_ f*f*x'-iso ftx' = f*x'-iso.to' ffx' = f*x'-iso.from' fftx' = f*f*x'-iso.to' fffx' = f*f*x'-iso.from' open F'⊣F'⁻¹ F'⊣F'⁻¹ : F' ⊣[ F⊣F⁻¹ ] F'⁻¹ F'⊣F'⁻¹ = record { F'⊣F'⁻¹ } unit'-iso : ∀ {x} x' → ℰ.is-invertible[ unit-iso x ] (unit' .η' x') unit'-iso x' = record { inv' = ff'⁻¹ ftx' ; inverses' = record { invl' = ff[]→faithful[] F' ff' $ ℱ.begin[] F'.₁' (ff'⁻¹ ffx' ℰ.∘' ff'⁻¹ ftx') ℱ.≡[]⟨ F'.F-∘' ⟩ℱ.≡[] F'.₁' (ff'⁻¹ ffx') ℱ.∘' F'.₁' (ff'⁻¹ ftx') ℱ.≡[]⟨ ε[] _ ℱ.⟩∘'⟨ ε[] _ ⟩ℱ.≡[] ffx' ℱ.∘' ftx' ℱ.≡[]⟨ f*x'-iso.invr' ⟩ℱ.≡[] ℱ.id' ℱ.≡[]˘⟨ F'.F-id' ⟩ℱ.≡[]˘ F'.₁' ℰ.id' ℱ.∎[] ; invr' = ff[]→faithful[] F' ff' $ ℱ.begin[] F'.₁' (ff'⁻¹ ftx' ℰ.∘' ff'⁻¹ ffx') ℱ.≡[]⟨ F'.F-∘' ⟩ℱ.≡[] F'.₁' (ff'⁻¹ ftx') ℱ.∘' F'.₁' (ff'⁻¹ ffx') ℱ.≡[]⟨ ε[] _ ℱ.⟩∘'⟨ ε[] _ ⟩ℱ.≡[] ftx' ℱ.∘' ffx' ℱ.≡[]⟨ f*x'-iso.invl' ⟩ℱ.≡[] ℱ.id' ℱ.≡[]˘⟨ F'.F-id' ⟩ℱ.≡[]˘ F'.₁' ℰ.id' ℱ.∎[] } } where open Σ (eso' (F'.₀' x')) renaming (fst to f*x' ; snd to f*x'-iso) module f*x'-iso = ℱ._≅[_]_ f*x'-iso ftx' = f*x'-iso.to' ffx' = f*x'-iso.from' counit'-iso : ∀ {x} x' → ℱ.is-invertible[ counit-iso x ] (counit' .η' x') counit'-iso x' = record { f*x'-iso } where open Σ (eso' x') renaming (fst to f*x' ; snd to f*x'-iso) module f*x'-iso = ℱ._≅[_]_ f*x'-iso
To summarise, from the data of ff', and eso' we are able to construct a
displayed equivalence of categories:
open ff[ff]+split-eso[]→is-equivalence[] ff[ff]+split-eso[]→is-equivalence[] : is-equivalence[ F-is-equiv ] F' ff[ff]+split-eso[]→is-equivalence[] = record { F'⁻¹ = F'⁻¹ ; F'⊣F'⁻¹ = F'⊣F'⁻¹ ; has-is-equivalence' = record { unit'-iso = unit'-iso ; counit'-iso = counit'-iso } }
Isomorphism🔗
When the base functor is an isomorphism of precategories, a stronger property than being an equivalence of displayed categories is being an isomomorphism of displayed categories:
record is-precat-iso[_]
{oa ℓa ob ℓb oe ℓe of ℓf} {A : Precategory oa ℓa} {B : Precategory ob ℓb} {ℰ : Displayed A oe ℓe} {ℱ : Displayed B of ℓf} {F : Functor A B}
(F-iso : is-precat-iso F) (F' : Displayed-functor F ℰ ℱ) : Type (adj-level' ℰ ℱ) where no-eta-equality constructor iso[] open is-precat-iso F-iso public
field has-is-ff' : is-ff[] F' has-is-iso' : ∀ x → is-equiv {A = ℰ.Ob[ x ]} F'.₀'
Apart from being fully faithfully displayed, such a functor is split
surjective on objects by has-is-iso' and therefore
essentially surjective:
module _
{oa ℓa ob ℓb oe ℓe of ℓf} {A : Precategory oa ℓa} {B : Precategory ob ℓb} {ℰ : Displayed A oe ℓe} {ℱ : Displayed B of ℓf} {F : Functor A B} {F' : Displayed-functor F ℰ ℱ}
(F-iso : is-precat-iso F) (F'-iso : is-precat-iso[ F-iso ] F') where
private module A = Cr A module B = Cr B module ℰ = Dr ℰ module ℱ = Dr ℱ module F = Functor F module F' = Displayed-functor F' open is-precat-iso[_] F'-iso eso = is-precat-iso→is-split-eso F-iso F₀≃ : A.Ob ≃ B.Ob F₀≃ = (F.₀ , has-is-iso) module F₀ = Equiv F₀≃
is-precat-iso[_]→is-split-eso[] : is-split-eso[ is-precat-iso→is-split-eso F-iso ] F' is-precat-iso[_]→is-split-eso[] {x} x' = (f*x' , f*x'-iso) where open Σ (eso x) renaming (fst to f*x ; snd to f*x-iso) f*x' = equiv→inverse (has-is-iso' (F₀.from x)) (subst ℱ.Ob[_] (sym (F₀.ε x)) x') p : F'.₀' f*x' ≡ subst ℱ.Ob[_] (sym (F₀.ε x)) x' p = equiv→counit (has-is-iso' f*x) (subst ℱ.Ob[_] (sym (F₀.ε x)) x') f*x'-iso = ℱ.path[ F₀.ε x ]→iso[] (to-pathp⁻ p)
Thus, is a displayed equivalence of displayed categories.
is-precat-iso[_]→is-equivalence[] : is-equivalence[ is-precat-iso→is-equivalence F-iso ] F' is-precat-iso[_]→is-equivalence[] = ff[ff]+split-eso[]→is-equivalence[] has-is-ff has-is-ff' is-precat-iso[_]→is-split-eso[]