{-# OPTIONS --safe #-}
module Cubical.Categories.Adjoint where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Data.Sigma
open import Cubical.Categories.Category
open import Cubical.Categories.Functor
open import Cubical.Categories.Instances.Functors
open import Cubical.Categories.NaturalTransformation
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open Functor
open Iso
open Category
private
variable
ℓC ℓC' ℓD ℓD' : Level
module UnitCounit {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (F : Functor C D) (G : Functor D C) where
record TriangleIdentities
(η : 𝟙⟨ C ⟩ ⇒ (funcComp G F))
(ε : (funcComp F G) ⇒ 𝟙⟨ D ⟩)
: Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD'))
where
field
Δ₁ : ∀ c → F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε ⟦ F ⟅ c ⟆ ⟧ ≡ D .id
Δ₂ : ∀ d → η ⟦ G ⟅ d ⟆ ⟧ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫ ≡ C .id
record _⊣_ : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
field
η : 𝟙⟨ C ⟩ ⇒ (funcComp G F)
ε : (funcComp F G) ⇒ 𝟙⟨ D ⟩
triangleIdentities : TriangleIdentities η ε
open TriangleIdentities triangleIdentities public
private
variable
C : Category ℓC ℓC'
D : Category ℓC ℓC'
module _ {F : Functor C D} {G : Functor D C} where
open UnitCounit
open _⊣_
open NatTrans
open TriangleIdentities
opositeAdjunction : (F ⊣ G) → ((G ^opF) ⊣ (F ^opF))
N-ob (η (opositeAdjunction x)) = N-ob (ε x)
N-hom (η (opositeAdjunction x)) f = sym (N-hom (ε x) f)
N-ob (ε (opositeAdjunction x)) = N-ob (η x)
N-hom (ε (opositeAdjunction x)) f = sym (N-hom (η x) f)
Δ₁ (triangleIdentities (opositeAdjunction x)) =
Δ₂ (triangleIdentities x)
Δ₂ (triangleIdentities (opositeAdjunction x)) =
Δ₁ (triangleIdentities x)
Iso⊣^opF : Iso (F ⊣ G) ((G ^opF) ⊣ (F ^opF))
fun Iso⊣^opF = opositeAdjunction
inv Iso⊣^opF = _
rightInv Iso⊣^opF _ = refl
leftInv Iso⊣^opF _ = refl
private
variable
F F' : Functor C D
G G' : Functor D C
module AdjointUniqeUpToNatIso where
open UnitCounit
module Left
(F⊣G : _⊣_ {D = D} F G)
(F'⊣G : F' ⊣ G) where
open NatTrans
private
variable
H H' : Functor C D
_D⋆_ = seq' D
m : (H⊣G : H ⊣ G) (H'⊣G : H' ⊣ G) →
∀ {x} → D [ H ⟅ x ⟆ , H' ⟅ x ⟆ ]
m {H = H} H⊣G H'⊣G =
H ⟪ (H'⊣G .η) ⟦ _ ⟧ ⟫ ⋆⟨ D ⟩ (H⊣G .ε) ⟦ _ ⟧ where open _⊣_
private
s : (H⊣G : H ⊣ G) (H'⊣G : H' ⊣ G) → ∀ {x} →
seq' D (m H'⊣G H⊣G {x}) (m H⊣G H'⊣G {x})
≡ D .id
s {H = H} {H' = H'} H⊣G H'⊣G = by-N-homs ∙ by-Δs
where
open _⊣_ H⊣G using (η ; Δ₂)
open _⊣_ H'⊣G using (ε ; Δ₁)
by-N-homs =
AssocCong₂⋆R {C = D} _
(AssocCong₂⋆L {C = D} (sym (N-hom ε _)) _)
∙ cong₂ _D⋆_
(sym (F-seq H' _ _)
∙∙ cong (H' ⟪_⟫) ((sym (N-hom η _)))
∙∙ F-seq H' _ _)
(sym (N-hom ε _))
by-Δs =
⋆Assoc D _ _ _
∙∙ cong (H' ⟪ _ ⟫ D⋆_)
(sym (⋆Assoc D _ _ _)
∙ cong (_D⋆ ε ⟦ _ ⟧)
( sym (F-seq H' _ _)
∙∙ cong (H' ⟪_⟫) (Δ₂ (H' ⟅ _ ⟆))
∙∙ F-id H')
∙ ⋆IdL D _)
∙∙ Δ₁ _
open NatIso
open isIso
F≅ᶜF' : F ≅ᶜ F'
N-ob (trans F≅ᶜF') _ = _
N-hom (trans F≅ᶜF') _ =
sym (⋆Assoc D _ _ _)
∙∙ cong (_D⋆ (F⊣G .ε) ⟦ _ ⟧)
(sym (F-seq F _ _)
∙∙ cong (F ⟪_⟫) (N-hom (F'⊣G .η) _)
∙∙ (F-seq F _ _))
∙∙ AssocCong₂⋆R {C = D} _ (N-hom (F⊣G .ε) _)
where open _⊣_
inv (nIso F≅ᶜF' _) = _
sec (nIso F≅ᶜF' _) = s F⊣G F'⊣G
ret (nIso F≅ᶜF' _) = s F'⊣G F⊣G
F≡F' : isUnivalent D → F ≡ F'
F≡F' univD =
isUnivalent.CatIsoToPath
(isUnivalentFUNCTOR _ _ univD)
(NatIso→FUNCTORIso _ _ F≅ᶜF')
module Right (F⊣G : F UnitCounit.⊣ G)
(F⊣G' : F UnitCounit.⊣ G') where
G≅ᶜG' : G ≅ᶜ G'
G≅ᶜG' = Iso.inv congNatIso^opFiso
(Left.F≅ᶜF' (opositeAdjunction F⊣G')
(opositeAdjunction F⊣G))
open NatIso
G≡G' : isUnivalent _ → G ≡ G'
G≡G' univC =
isUnivalent.CatIsoToPath
(isUnivalentFUNCTOR _ _ univC)
(NatIso→FUNCTORIso _ _ G≅ᶜG')
module NaturalBijection where
record _⊣_ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (F : Functor C D) (G : Functor D C) : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
field
adjIso : ∀ {c d} → Iso (D [ F ⟅ c ⟆ , d ]) (C [ c , G ⟅ d ⟆ ])
infix 40 _♭
infix 40 _♯
_♭ : ∀ {c d} → (D [ F ⟅ c ⟆ , d ]) → (C [ c , G ⟅ d ⟆ ])
(_♭) {_} {_} = adjIso .fun
_♯ : ∀ {c d} → (C [ c , G ⟅ d ⟆ ]) → (D [ F ⟅ c ⟆ , d ])
(_♯) {_} {_} = adjIso .inv
field
adjNatInD : ∀ {c : C .ob} {d d'} (f : D [ F ⟅ c ⟆ , d ]) (k : D [ d , d' ])
→ (f ⋆⟨ D ⟩ k) ♭ ≡ f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫
adjNatInC : ∀ {c' c d} (g : C [ c , G ⟅ d ⟆ ]) (h : C [ c' , c ])
→ (h ⋆⟨ C ⟩ g) ♯ ≡ F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯
adjNatInD' : ∀ {c : C .ob} {d d'} (g : C [ c , G ⟅ d ⟆ ]) (k : D [ d , d' ])
→ g ♯ ⋆⟨ D ⟩ k ≡ (g ⋆⟨ C ⟩ G ⟪ k ⟫) ♯
adjNatInD' {c} {d} {d'} g k =
g ♯ ⋆⟨ D ⟩ k
≡⟨ sym (adjIso .leftInv (g ♯ ⋆⟨ D ⟩ k)) ⟩
((g ♯ ⋆⟨ D ⟩ k) ♭) ♯
≡⟨ cong _♯ (adjNatInD (g ♯) k) ⟩
((g ♯) ♭ ⋆⟨ C ⟩ G ⟪ k ⟫) ♯
≡⟨ cong _♯ (cong (λ g' → seq' C g' (G ⟪ k ⟫)) (adjIso .rightInv g)) ⟩
(g ⋆⟨ C ⟩ G ⟪ k ⟫) ♯ ∎
adjNatInC' : ∀ {c' c d} (f : D [ F ⟅ c ⟆ , d ]) (h : C [ c' , c ])
→ h ⋆⟨ C ⟩ (f ♭) ≡ (F ⟪ h ⟫ ⋆⟨ D ⟩ f) ♭
adjNatInC' {c'} {c} {d} f h =
h ⋆⟨ C ⟩ (f ♭)
≡⟨ sym (adjIso .rightInv (h ⋆⟨ C ⟩ (f ♭))) ⟩
((h ⋆⟨ C ⟩ (f ♭)) ♯) ♭
≡⟨ cong _♭ (adjNatInC (f ♭) h) ⟩
((F ⟪ h ⟫ ⋆⟨ D ⟩ (f ♭) ♯) ♭)
≡⟨ cong _♭ (cong (λ f' → seq' D (F ⟪ h ⟫) f') (adjIso .leftInv f)) ⟩
(F ⟪ h ⟫ ⋆⟨ D ⟩ f) ♭ ∎
isLeftAdjoint : {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (F : Functor C D) → Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD'))
isLeftAdjoint {C = C}{D} F = Σ[ G ∈ Functor D C ] F ⊣ G
isRightAdjoint : {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (G : Functor D C) → Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD'))
isRightAdjoint {C = C}{D} G = Σ[ F ∈ Functor C D ] F ⊣ G
module _ (F : Functor C D) (G : Functor D C) where
open UnitCounit
open NaturalBijection renaming (_⊣_ to _⊣²_)
module _ (adj : F ⊣² G) where
open _⊣²_ adj
open _⊣_
adjNat' : ∀ {c c' d d'} {f : D [ F ⟅ c ⟆ , d ]} {k : D [ d , d' ]}
→ {h : C [ c , c' ]} {g : C [ c' , G ⟅ d' ⟆ ]}
→ ((f ⋆⟨ D ⟩ k ≡ F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯) → (f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫ ≡ h ⋆⟨ C ⟩ g))
× ((f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫ ≡ h ⋆⟨ C ⟩ g) → (f ⋆⟨ D ⟩ k ≡ F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯))
adjNat' {c} {c'} {d} {d'} {f} {k} {h} {g} = D→C , C→D
where
D→C : (f ⋆⟨ D ⟩ k ≡ F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯) → (f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫ ≡ h ⋆⟨ C ⟩ g)
D→C eq = f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫
≡⟨ sym (adjNatInD _ _) ⟩
((f ⋆⟨ D ⟩ k) ♭)
≡⟨ cong _♭ eq ⟩
(F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯) ♭
≡⟨ sym (cong _♭ (adjNatInC _ _)) ⟩
(h ⋆⟨ C ⟩ g) ♯ ♭
≡⟨ adjIso .rightInv _ ⟩
h ⋆⟨ C ⟩ g
∎
C→D : (f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫ ≡ h ⋆⟨ C ⟩ g) → (f ⋆⟨ D ⟩ k ≡ F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯)
C→D eq = f ⋆⟨ D ⟩ k
≡⟨ sym (adjIso .leftInv _) ⟩
(f ⋆⟨ D ⟩ k) ♭ ♯
≡⟨ cong _♯ (adjNatInD _ _) ⟩
(f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫) ♯
≡⟨ cong _♯ eq ⟩
(h ⋆⟨ C ⟩ g) ♯
≡⟨ adjNatInC _ _ ⟩
F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯
∎
open NatTrans
adj'→adj : F ⊣ G
adj'→adj = record
{ η = η'
; ε = ε'
; triangleIdentities = record
{Δ₁ = Δ₁'
; Δ₂ = Δ₂' }}
where
commInD : ∀ {x y} (f : C [ x , y ]) → D .id ⋆⟨ D ⟩ F ⟪ f ⟫ ≡ F ⟪ f ⟫ ⋆⟨ D ⟩ D .id
commInD f = (D .⋆IdL _) ∙ sym (D .⋆IdR _)
sharpen1 : ∀ {x y} (f : C [ x , y ]) → F ⟪ f ⟫ ⋆⟨ D ⟩ D .id ≡ F ⟪ f ⟫ ⋆⟨ D ⟩ D .id ♭ ♯
sharpen1 f = cong (λ v → F ⟪ f ⟫ ⋆⟨ D ⟩ v) (sym (adjIso .leftInv _))
η' : 𝟙⟨ C ⟩ ⇒ G ∘F F
η' .N-ob x = D .id ♭
η' .N-hom f = sym (fst (adjNat') (commInD f ∙ sharpen1 f))
commInC : ∀ {x y} (g : D [ x , y ]) → C .id ⋆⟨ C ⟩ G ⟪ g ⟫ ≡ G ⟪ g ⟫ ⋆⟨ C ⟩ C .id
commInC g = (C .⋆IdL _) ∙ sym (C .⋆IdR _)
sharpen2 : ∀ {x y} (g : D [ x , y ]) → C .id ♯ ♭ ⋆⟨ C ⟩ G ⟪ g ⟫ ≡ C .id ⋆⟨ C ⟩ G ⟪ g ⟫
sharpen2 g = cong (λ v → v ⋆⟨ C ⟩ G ⟪ g ⟫) (adjIso .rightInv _)
ε' : F ∘F G ⇒ 𝟙⟨ D ⟩
ε' .N-ob x = C .id ♯
ε' .N-hom g = sym (snd adjNat' (sharpen2 g ∙ commInC g))
Δ₁' : ∀ c → F ⟪ η' ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε' ⟦ F ⟅ c ⟆ ⟧ ≡ D .id
Δ₁' c =
F ⟪ η' ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε' ⟦ F ⟅ c ⟆ ⟧
≡⟨ sym (snd adjNat' (cong (λ v → (η' ⟦ c ⟧) ⋆⟨ C ⟩ v) (G .F-id))) ⟩
D .id ⋆⟨ D ⟩ D .id
≡⟨ D .⋆IdL _ ⟩
D .id
∎
Δ₂' : ∀ d → η' ⟦ G ⟅ d ⟆ ⟧ ⋆⟨ C ⟩ G ⟪ ε' ⟦ d ⟧ ⟫ ≡ C .id
Δ₂' d =
(η' ⟦ G ⟅ d ⟆ ⟧) ⋆⟨ C ⟩ (G ⟪ ε' ⟦ d ⟧ ⟫)
≡⟨ fst adjNat' (cong (λ v → v ⋆⟨ D ⟩ (ε' ⟦ d ⟧)) (sym (F .F-id))) ⟩
C .id ⋆⟨ C ⟩ C .id
≡⟨ C .⋆IdL _ ⟩
C .id
∎
module _ (adj : F ⊣ G) where
open _⊣_ adj
open _⊣²_
open NatTrans
adj→adj' : F ⊣² G
adj→adj' .adjIso {c = c} .fun f = η ⟦ c ⟧ ⋆⟨ C ⟩ G ⟪ f ⟫
adj→adj' .adjIso {d = d} .inv g = F ⟪ g ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧
adj→adj' .adjIso {c = c} {d} .rightInv g
= η ⟦ c ⟧ ⋆⟨ C ⟩ G ⟪ F ⟪ g ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧ ⟫
≡⟨ cong (λ v → η ⟦ c ⟧ ⋆⟨ C ⟩ v) (G .F-seq _ _) ⟩
η ⟦ c ⟧ ⋆⟨ C ⟩ (G ⟪ F ⟪ g ⟫ ⟫ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫)
≡⟨ sym (C .⋆Assoc _ _ _) ⟩
η ⟦ c ⟧ ⋆⟨ C ⟩ G ⟪ F ⟪ g ⟫ ⟫ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫
≡⟨ rCatWhisker {C = C} _ _ _ natu ⟩
(g ⋆⟨ C ⟩ η ⟦ G ⟅ d ⟆ ⟧) ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫
≡⟨ C .⋆Assoc _ _ _ ⟩
g ⋆⟨ C ⟩ (η ⟦ G ⟅ d ⟆ ⟧ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫)
≡⟨ lCatWhisker {C = C} _ _ _ (Δ₂ d) ⟩
g ⋆⟨ C ⟩ C .id
≡⟨ C .⋆IdR _ ⟩
g
∎
where
natu : η ⟦ c ⟧ ⋆⟨ C ⟩ G ⟪ F ⟪ g ⟫ ⟫ ≡ g ⋆⟨ C ⟩ η ⟦ G ⟅ d ⟆ ⟧
natu = sym (η .N-hom _)
adj→adj' .adjIso {c = c} {d} .leftInv f
= F ⟪ η ⟦ c ⟧ ⋆⟨ C ⟩ G ⟪ f ⟫ ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧
≡⟨ cong (λ v → v ⋆⟨ D ⟩ ε ⟦ d ⟧) (F .F-seq _ _) ⟩
F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ F ⟪ G ⟪ f ⟫ ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧
≡⟨ D .⋆Assoc _ _ _ ⟩
F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ (F ⟪ G ⟪ f ⟫ ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧)
≡⟨ lCatWhisker {C = D} _ _ _ natu ⟩
F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ (ε ⟦ F ⟅ c ⟆ ⟧ ⋆⟨ D ⟩ f)
≡⟨ sym (D .⋆Assoc _ _ _) ⟩
F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε ⟦ F ⟅ c ⟆ ⟧ ⋆⟨ D ⟩ f
≡⟨ rCatWhisker {C = D} _ _ _ (Δ₁ c) ⟩
D .id ⋆⟨ D ⟩ f
≡⟨ D .⋆IdL _ ⟩
f
∎
where
natu : F ⟪ G ⟪ f ⟫ ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧ ≡ ε ⟦ F ⟅ c ⟆ ⟧ ⋆⟨ D ⟩ f
natu = ε .N-hom _
adj→adj' .adjNatInD {c = c} f k = cong (λ v → η ⟦ c ⟧ ⋆⟨ C ⟩ v) (G .F-seq _ _) ∙ (sym (C .⋆Assoc _ _ _))
adj→adj' .adjNatInC {d = d} g h = cong (λ v → v ⋆⟨ D ⟩ ε ⟦ d ⟧) (F .F-seq _ _) ∙ D .⋆Assoc _ _ _