|
| 1 | +{-# OPTIONS --without-K --safe #-} |
| 2 | +module Categories.CoYoneda where |
| 3 | + |
| 4 | +-- CoYoneda Lemma. See Yoneda for more documentation |
| 5 | + |
| 6 | +open import Level |
| 7 | +open import Function.Base using (_$_) |
| 8 | +open import Function.Bundles using (Inverse) |
| 9 | +open import Function.Equality using (Π; _⟨$⟩_; cong) |
| 10 | +open import Relation.Binary.Bundles using (module Setoid) |
| 11 | +import Relation.Binary.Reasoning.Setoid as SetoidR |
| 12 | +open import Data.Product using (_,_; Σ) |
| 13 | + |
| 14 | +open import Categories.Category using (Category; _[_,_]) |
| 15 | +open import Categories.Category.Product using (πʳ; πˡ; _※_) |
| 16 | +open import Categories.Category.Construction.Presheaves using (CoPresheaves) |
| 17 | +open import Categories.Category.Construction.Functors using (eval) |
| 18 | +open import Categories.Category.Construction.Functors |
| 19 | +open import Categories.Category.Instance.Setoids using (Setoids) |
| 20 | +open import Categories.Functor using (Functor; _∘F_) renaming (id to idF) |
| 21 | +open import Categories.Functor.Hom using (module Hom; Hom[_][_,-]; Hom[_][-,-]) |
| 22 | +open import Categories.Functor.Bifunctor using (Bifunctor) |
| 23 | +-- open import Categories.Functor.Presheaf using (Presheaf) |
| 24 | +open import Categories.Functor.Construction.LiftSetoids using (LiftSetoids) |
| 25 | +open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) renaming (id to idN) |
| 26 | +open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism) |
| 27 | + |
| 28 | +import Categories.Morphism as Mor |
| 29 | +import Categories.Morphism.Reasoning as MR |
| 30 | +import Categories.NaturalTransformation.Hom as NT-Hom |
| 31 | + |
| 32 | +private |
| 33 | + variable |
| 34 | + o ℓ e : Level |
| 35 | + |
| 36 | +module Yoneda (C : Category o ℓ e) where |
| 37 | + open Category C hiding (op) -- uses lots |
| 38 | + open HomReasoning using (_○_; ⟺) |
| 39 | + open MR C using (id-comm) |
| 40 | + open NaturalTransformation using (η; commute) |
| 41 | + open NT-Hom C using (Hom[C,A]⇒Hom[C,B]) |
| 42 | + private |
| 43 | + module CE = Category.Equiv C using (refl) |
| 44 | + module C = Category C using (op) |
| 45 | + |
| 46 | + -- The CoYoneda embedding functor |
| 47 | + embed : Functor C.op (CoPresheaves C) |
| 48 | + embed = record |
| 49 | + { F₀ = Hom[ C ][_,-] |
| 50 | + ; F₁ = Hom[C,A]⇒Hom[C,B] -- B⇒A induces a NatTrans on the Homs. |
| 51 | + ; identity = identityʳ ○_ |
| 52 | + ; homomorphism = λ h₁≈h₂ → ∘-resp-≈ˡ h₁≈h₂ ○ sym-assoc |
| 53 | + ; F-resp-≈ = λ f≈g h≈i → ∘-resp-≈ h≈i f≈g |
| 54 | + } |
| 55 | + |
| 56 | + -- Using the adjunction between product and product, we get a kind of contravariant Bifunctor |
| 57 | + yoneda-inverse : (a : Obj) (F : Functor C (Setoids ℓ e)) → |
| 58 | + Inverse (Category.hom-setoid (CoPresheaves C) {Functor.F₀ embed a} {F}) (Functor.F₀ F a) |
| 59 | + yoneda-inverse a F = record |
| 60 | + { f = λ nat → η nat a ⟨$⟩ id |
| 61 | + ; f⁻¹ = λ x → ntHelper record |
| 62 | + { η = λ X → record |
| 63 | + { _⟨$⟩_ = λ X⇒a → F.₁ X⇒a ⟨$⟩ x |
| 64 | + ; cong = λ i≈j → F.F-resp-≈ i≈j SE.refl |
| 65 | + } |
| 66 | + ; commute = λ {X} {Y} X⇒Y {f} {g} f≈g → |
| 67 | + let module SR = SetoidR (F.₀ Y) in |
| 68 | + SR.begin |
| 69 | + F.₁ (X⇒Y ∘ f ∘ id) ⟨$⟩ x SR.≈⟨ F.F-resp-≈ (∘-resp-≈ʳ (identityʳ ○ f≈g)) SE.refl ⟩ |
| 70 | + F.₁ (X⇒Y ∘ g) ⟨$⟩ x SR.≈⟨ F.homomorphism SE.refl ⟩ |
| 71 | + F.₁ X⇒Y ⟨$⟩ (F.₁ g ⟨$⟩ x) |
| 72 | + SR.∎ |
| 73 | + } |
| 74 | + ; cong₁ = λ i≈j → i≈j CE.refl |
| 75 | + ; cong₂ = λ i≈j y≈z → F.F-resp-≈ y≈z i≈j |
| 76 | + ; inverse = (λ Fa → F.identity SE.refl) , λ nat {x} {z} {y} z≈y → |
| 77 | + let module SR = SetoidR (F.₀ x) in |
| 78 | + SR.begin |
| 79 | + F.₁ z ⟨$⟩ (η nat a ⟨$⟩ id) SR.≈˘⟨ commute nat z (CE.refl {a}) ⟩ |
| 80 | + η nat x ⟨$⟩ z ∘ id ∘ id SR.≈⟨ cong (η nat x) (∘-resp-≈ʳ identity² ○ identityʳ ○ z≈y ) ⟩ |
| 81 | + η nat x ⟨$⟩ y |
| 82 | + SR.∎ |
| 83 | + } |
| 84 | + where |
| 85 | + module F = Functor F using (₀; ₁; F-resp-≈; homomorphism; identity) |
| 86 | + module SE = Setoid (F.₀ a) using (refl) |
| 87 | + |
| 88 | + private |
| 89 | + Nat[Hom[C][c,-],F] : Bifunctor (CoPresheaves C) C (Setoids (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)) |
| 90 | + Nat[Hom[C][c,-],F] = Hom[ CoPresheaves C ][-,-] ∘F (Functor.op embed ∘F πʳ ※ πˡ) |
| 91 | + |
| 92 | + FC : Bifunctor (CoPresheaves C) C (Setoids _ _) |
| 93 | + FC = LiftSetoids (o ⊔ ℓ ⊔ e) (o ⊔ ℓ) ∘F eval {C = C} {D = Setoids ℓ e} |
| 94 | + |
| 95 | + module yoneda-inverse {a} {F} = Inverse (yoneda-inverse a F) |
| 96 | + |
| 97 | + -- the two bifunctors above are naturally isomorphic. |
| 98 | + -- it is easy to show yoneda-inverse first then to yoneda. |
| 99 | + yoneda : NaturalIsomorphism Nat[Hom[C][c,-],F] FC |
| 100 | + yoneda = record |
| 101 | + { F⇒G = ntHelper record |
| 102 | + { η = λ where |
| 103 | + (F , A) → record |
| 104 | + { _⟨$⟩_ = λ α → lift (yoneda-inverse.f α) |
| 105 | + ; cong = λ i≈j → lift (i≈j CE.refl) |
| 106 | + } |
| 107 | + ; commute = λ where |
| 108 | + {_} {G , B} (α , f) {β} {γ} β≈γ → lift $ cong (η α B) (helper f β γ β≈γ) |
| 109 | + } |
| 110 | + ; F⇐G = ntHelper record |
| 111 | + { η = λ (F , A) → record |
| 112 | + { _⟨$⟩_ = λ x → yoneda-inverse.f⁻¹ (lower x) |
| 113 | + ; cong = λ i≈j y≈z → Functor.F-resp-≈ F y≈z (lower i≈j) |
| 114 | + } |
| 115 | + ; commute = λ { {F , A} {G , B} (α , f) {X} {Y} eq {Z} {h} {i} eq′ → helper′ α f (lower eq) eq′} |
| 116 | + } |
| 117 | + ; iso = λ (F , A) → record |
| 118 | + { isoˡ = λ {α β} i≈j {X} y≈z → |
| 119 | + Setoid.trans (Functor.F₀ F X) ( yoneda-inverse.inverseʳ α {x = X} y≈z) (i≈j CE.refl) |
| 120 | + ; isoʳ = λ eq → lift (Setoid.trans (Functor.F₀ F A) ( yoneda-inverse.inverseˡ {F = F} _) (lower eq)) |
| 121 | + } |
| 122 | + } |
| 123 | + where helper : {F : Functor C (Setoids ℓ e)} |
| 124 | + {A B : Obj} (f : A ⇒ B) |
| 125 | + (β γ : NaturalTransformation Hom[ C ][ A ,-] F) → |
| 126 | + Setoid._≈_ (Functor.F₀ Nat[Hom[C][c,-],F] (F , A)) β γ → |
| 127 | + Setoid._≈_ (Functor.F₀ F B) (η β B ⟨$⟩ id ∘ f) (Functor.F₁ F f ⟨$⟩ (η γ A ⟨$⟩ id)) |
| 128 | + helper {F} {A} {B} f β γ β≈γ = S.begin |
| 129 | + η β B ⟨$⟩ id ∘ f S.≈⟨ cong (η β B) (MR.id-comm-sym C ○ ∘-resp-≈ʳ (⟺ identity²)) ⟩ |
| 130 | + η β B ⟨$⟩ f ∘ id ∘ id S.≈⟨ commute β f CE.refl ⟩ |
| 131 | + F.₁ f ⟨$⟩ (η β A ⟨$⟩ id) S.≈⟨ cong (F.₁ f) (β≈γ CE.refl) ⟩ |
| 132 | + F.₁ f ⟨$⟩ (η γ A ⟨$⟩ id) S.∎ |
| 133 | + where |
| 134 | + module F = Functor F using (₀;₁) |
| 135 | + module S = SetoidR (F.₀ B) |
| 136 | + |
| 137 | + helper′ : ∀ {F G : Functor C (Setoids ℓ e)} |
| 138 | + {A B Z : Obj} |
| 139 | + {h i : B ⇒ Z} |
| 140 | + {X Y : Setoid.Carrier (Functor.F₀ F A)} |
| 141 | + (α : NaturalTransformation F G) |
| 142 | + (f : A ⇒ B) → |
| 143 | + Setoid._≈_ (Functor.F₀ F A) X Y → |
| 144 | + h ≈ i → |
| 145 | + Setoid._≈_ (Functor.F₀ G Z) (Functor.F₁ G h ⟨$⟩ (η α B ⟨$⟩ (Functor.F₁ F f ⟨$⟩ X))) |
| 146 | + (η α Z ⟨$⟩ (Functor.F₁ F (i ∘ f) ⟨$⟩ Y)) |
| 147 | + helper′ {F} {G} {A} {B} {Z} {h} {i} {X} {Y} α f eq eq′ = S.begin |
| 148 | + G.₁ h ⟨$⟩ (η α B ⟨$⟩ (F.₁ f ⟨$⟩ X)) S.≈˘⟨ commute α h ((S′.sym (cong (F.₁ f) eq))) ⟩ |
| 149 | + η α Z ⟨$⟩ (F.₁ h ⟨$⟩ (F.₁ f ⟨$⟩ Y)) S.≈⟨ cong (η α Z) ((F.F-resp-≈ eq′ S′.refl)) ⟩ |
| 150 | + η α Z ⟨$⟩ (F.₁ i ⟨$⟩ (F.₁ f ⟨$⟩ Y)) S.≈˘⟨ cong (η α Z) ((F.homomorphism (Setoid.refl (F.₀ A)))) ⟩ |
| 151 | + η α Z ⟨$⟩ (F.₁ (i ∘ f) ⟨$⟩ Y) S.∎ |
| 152 | + where |
| 153 | + module F = Functor F using (₀; ₁; homomorphism; F-resp-≈) |
| 154 | + module G = Functor G using (₀; ₁) |
| 155 | + module S = SetoidR (G.₀ Z) |
| 156 | + module S′ = Setoid (F.₀ B) using (refl; sym) |
| 157 | + |
| 158 | + module yoneda = NaturalIsomorphism yoneda |
0 commit comments