Last active
February 18, 2023 16:11
-
-
Save khibino/b956f8f6e2483180bfbb8698b1d05acd to your computer and use it in GitHub Desktop.
Yoneda Lemma Proof under Higher-Order types
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| module YonedaHO where | |
| open import Agda.Primitive using (Level; lsuc; _⊔_) | |
| open import Level using (lift) | |
| open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym; trans; cong; cong-app) | |
| open import Data.Product using (_×_; ∃; _,_; proj₂) | |
| {- apply _≡_ for objects and morphisms for Locally Small Categories -} | |
| {- morphism type definition -} | |
| Hom : (o m : Level) → Set (lsuc o ⊔ lsuc m) | |
| Hom o m = Set o → Set o → Set m | |
| {- Category definition -} | |
| record Cat | |
| {o m} | |
| (hom : Hom o m) | |
| : Set (lsuc o ⊔ lsuc m) where | |
| infix 5 _⟿_ | |
| _⟿_ = hom | |
| infixr 9 compose | |
| syntax compose f g = f ∘ g | |
| field | |
| id : ∀{a} → a ⟿ a | |
| compose : ∀ {a b c} → (b ⟿ c) → (a ⟿ b) → (a ⟿ c) | |
| left-id : ∀ {a b} (f : a ⟿ b) → id ∘ f ≡ f | |
| right-id : ∀ {a b} (f : a ⟿ b) → f ∘ id ≡ f | |
| associativity : ∀ {a b c d} (f : c ⟿ d) (g : b ⟿ c) (h : a ⟿ b) → | |
| (f ∘ g) ∘ h ≡ f ∘ (g ∘ h) | |
| get-homᵒᵖ : ∀{o m} → Hom o m → Hom o m | |
| get-homᵒᵖ hom a b = hom b a | |
| _ᵒᵖ : ∀ {o m} {hom : Hom o m} → Cat hom → Cat (get-homᵒᵖ hom) | |
| _ᵒᵖ {o} {m} {hom} C = | |
| record | |
| { id = idᵒᵖ | |
| ; compose = _∘ᵒᵖ_ | |
| ; left-id = left-idᵒᵖ | |
| ; right-id = right-idᵒᵖ | |
| ; associativity = associativityᵒᵖ | |
| } | |
| where | |
| _⟿_ = hom | |
| _⟿ᵒᵖ_ = get-homᵒᵖ (_⟿_) | |
| infix 5 _⟿_ _⟿ᵒᵖ_ | |
| idᵒᵖ = Cat.id C | |
| _∘_ : ∀ {a b c} → (b ⟿ c) → (a ⟿ b) → (a ⟿ c) | |
| _∘_ = Cat.compose C | |
| _∘ᵒᵖ_ : ∀ {a b c} → (b ⟿ᵒᵖ c) → (a ⟿ᵒᵖ b) → (a ⟿ᵒᵖ c) | |
| f ∘ᵒᵖ g = g ∘ f | |
| infixr 9 _∘_ _∘ᵒᵖ_ | |
| left-idᵒᵖ : ∀ {a b} (f : a ⟿ᵒᵖ b) → idᵒᵖ ∘ᵒᵖ f ≡ f | |
| left-idᵒᵖ = Cat.right-id C | |
| right-idᵒᵖ : ∀ {a b} (f : a ⟿ᵒᵖ b) → f ∘ᵒᵖ idᵒᵖ ≡ f | |
| right-idᵒᵖ = Cat.left-id C | |
| associativityᵒᵖ : ∀ {a b c d} (f : c ⟿ᵒᵖ d) (g : b ⟿ᵒᵖ c) (h : a ⟿ᵒᵖ b) → | |
| (f ∘ᵒᵖ g) ∘ᵒᵖ h ≡ f ∘ᵒᵖ (g ∘ᵒᵖ h) | |
| associativityᵒᵖ f g h = sym (Cat.associativity C h g f) | |
| infix 9 _ᵒᵖ | |
| {- Functor definition -} | |
| record Functor | |
| {o₁ m₁} | |
| {hom₁ : Hom o₁ m₁} | |
| (C₁ : Cat hom₁) | |
| {o₂ m₂} | |
| {hom₂ : Hom o₂ m₂} | |
| (C₂ : Cat hom₂) | |
| : Set (lsuc o₁ ⊔ lsuc m₁ ⊔ lsuc o₂ ⊔ lsuc m₂) where | |
| _⟿₁_ = hom₁ | |
| infix 5 _⟿₁_ | |
| id₁ = Cat.id C₁ | |
| _∘₁_ = Cat.compose C₁ | |
| _⟿₂_ = hom₂ | |
| id₂ = Cat.id C₂ | |
| _∘₂_ = Cat.compose C₂ | |
| infixr 9 _∘₁_ _∘₂_ | |
| field | |
| F : Set o₁ → Set o₂ | |
| fmap : ∀ {a b} → (a ⟿₁ b) → (F a ⟿₂ F b) | |
| fmap-id : ∀ {a} → fmap {a} {a} id₁ ≡ id₂ | |
| fmap-dist : ∀ {a b c} {f : b ⟿₁ c} {g : a ⟿₁ b} → | |
| fmap {a} {c} (f ∘₁ g) ≡ fmap {b} {c} f ∘₂ fmap {a} {b} g | |
| {- Naturality type -} | |
| Naturality : ∀ {o m} {hom : Hom o m} {C : Cat hom} | |
| {oᴰ mᴰ} {homᴰ : Hom oᴰ mᴰ} {D : Cat homᴰ} → | |
| Functor C D → | |
| Functor C D → | |
| Set (lsuc o ⊔ m ⊔ mᴰ) | |
| Naturality | |
| {o} {m} {hom} {C} | |
| {oᴰ} {mᴰ} {homᴰ} {D} | |
| rF | |
| rG | |
| = (Nat : ∀ a → F a ⟿ᴰ G a) → | |
| (∀ {a b} (f : a ⟿ b) → Nat b ∘ᴰ fmapF {a} {b} f ≡ fmapG {a} {b} f ∘ᴰ Nat a) | |
| where | |
| _⟿_ = hom | |
| _⟿ᴰ_ = homᴰ | |
| infix 5 _⟿_ _⟿ᴰ_ | |
| _∘ᴰ_ = Cat.compose D | |
| infixr 9 _∘ᴰ_ | |
| F = Functor.F rF | |
| fmapF = Functor.fmap rF | |
| G = Functor.F rG | |
| fmapG = Functor.fmap rG | |
| --- | |
| {- extensionality type -} | |
| EX : ∀ (lᵢ lⱼ : Level) -> Set (lsuc lᵢ ⊔ lsuc lⱼ) | |
| EX lᵢ lⱼ = | |
| {A : Set lᵢ} {B : A → Set lⱼ} {f g : (x : A) → B x} → | |
| (∀ x → f x ≡ g x) → f ≡ g | |
| {- hom-set of universe polymorphic Sets -} | |
| _→ᵤ_ : ∀{l} -> Set l → Set l → Set l | |
| _→ᵤ_ a b = a → b | |
| {- universe polymorphic Sets definition -} | |
| 𝕊𝕖𝕥 : ∀ {l : Level} → Cat (_→ᵤ_ {l}) | |
| 𝕊𝕖𝕥 = | |
| record | |
| { id = λ {a} (x : a) → x | |
| ; compose = λ f g x → f (g x) | |
| ; left-id = λ f → refl | |
| ; right-id = λ f → refl | |
| ; associativity = λ f g h → refl | |
| } | |
| module WithSets | |
| {l : Level} | |
| (extensionality : ∀{lᵢ lⱼ} → EX lᵢ lⱼ) | |
| where | |
| _→₀_ : Set l → Set l → Set l | |
| _→₀_ = _→ᵤ_ {l} | |
| 𝕊𝕖𝕥₀ : Cat (_→₀_) | |
| 𝕊𝕖𝕥₀ = 𝕊𝕖𝕥 | |
| idₛ : ∀ {a : Set l} → a →₀ a | |
| idₛ = Cat.id 𝕊𝕖𝕥₀ | |
| _∘ₛ_ = Cat.compose 𝕊𝕖𝕥₀ | |
| infixr 9 _∘ₛ_ | |
| homF : ∀ {o} {hom : Hom o l} (C : Cat hom) (r : Set o) → Functor C 𝕊𝕖𝕥₀ | |
| homF {o} {hom} C r = | |
| record | |
| { F = Homᵣ | |
| ; fmap = fmapʰ | |
| ; fmap-id = fmapʰ-id | |
| ; fmap-dist = fmapʰ-dist | |
| } | |
| where | |
| {- hom-set of C -} | |
| _⟿_ = hom | |
| infix 5 _⟿_ | |
| id : ∀ {a : Set o} → (a ⟿ a) | |
| id = Cat.id C | |
| _∘_ = Cat.compose C | |
| infixr 9 _∘_ | |
| Homᵣ : Set o → Set l | |
| Homᵣ = _⟿_ r | |
| fmapʰ : ∀ {a b : Set o} → (a ⟿ b) → (r ⟿ a) → (r ⟿ b) | |
| fmapʰ = Cat.compose C | |
| fmapʰ-id : ∀ {a : Set o} → fmapʰ {a} {a} id ≡ idₛ | |
| fmapʰ-id = extensionality (Cat.left-id C) | |
| fmapʰ-dist : ∀ {a b c} {f : b ⟿ c} {g : a ⟿ b} → | |
| fmapʰ {a} {c} (f ∘ g) ≡ fmapʰ {b} {c} f ∘ₛ fmapʰ {a} {b} g | |
| fmapʰ-dist {_} {_} {_} {f} {g} = extensionality (Cat.associativity C f g) | |
| module Yoneda | |
| {o} | |
| {hom : Hom o l} | |
| (C : Cat hom) | |
| (recF : Functor C 𝕊𝕖𝕥₀) | |
| (r : Set o) | |
| where | |
| {- hom-set of C -} | |
| _⟿_ = hom | |
| infix 5 _⟿_ | |
| F = Functor.F recF | |
| fmapᶠ = Functor.fmap recF | |
| fmapᶠ-id = Functor.fmap-id recF | |
| fmapʰ = Functor.fmap (homF C r) | |
| {- construction of Yoneda map ⟹ -} | |
| map-⟹ : (∀ (a : Set o) → (r ⟿ a) →₀ F a) → F r | |
| map-⟹ Nat = Nat r (Cat.id C) | |
| {- construction of Yoneda map ⟸ -} | |
| map-⟸ : F r → (∀ (a : Set o) → (r ⟿ a) →₀ F a) | |
| map-⟸ x a k = fmapᶠ k x | |
| module Lemma | |
| (naturality : ∀ {r : Set o} → Naturality (homF C r) recF) | |
| where | |
| _∘_ : ∀ {x y z} {a : Set x} {b : Set y} {c : Set z} → (b → c) → (a → b) → (a → c) | |
| _∘_ f g x = f (g x) | |
| {- proof: composition of Yoneda map (⟹ ∘ ⟸) is identity -} | |
| id-right-left : map-⟹ ∘ map-⟸ ≡ (λ x → x) | |
| id-right-left = fmapᶠ-id | |
| {- proof: composition of Yoneda map (⟸ ∘ ⟹) is identity, arguments applied form -} | |
| id-left-right-applied : ∀ (Nat : ∀ (a : Set o) → (r ⟿ a) →₀ F a) (b : Set o) (k : r ⟿ b) → | |
| (map-⟸ ∘ map-⟹) Nat b k ≡ Nat b k | |
| id-left-right-applied Nat b k = trans naturality-on-id nat-on-right-id-k | |
| where | |
| id = Cat.id C | |
| naturality-on-id : (fmapᶠ {r} {b} k ∘ₛ Nat r) id ≡ (Nat b ∘ₛ fmapʰ {r} {b} k) id | |
| naturality-on-id = sym (cong-app (naturality Nat k) id) | |
| nat-on-right-id-k : (Nat b ∘ₛ fmapʰ {r} {b} k) id ≡ Nat b k | |
| nat-on-right-id-k = cong (Nat b) (Cat.right-id C k) | |
| {- proof: composition of Yoneda map (⟸ ∘ ⟹) is identity -} | |
| id-left-right : (map-⟸ ∘ map-⟹) ≡ Cat.id 𝕊𝕖𝕥 | |
| id-left-right = | |
| extensionality λ Nat → | |
| extensionality-Nat Nat λ b → | |
| extensionality (id-left-right-applied Nat b) | |
| where | |
| extensionality-Nat : ∀ (Nat : ∀ (a : Set o) → (r ⟿ a) →₀ F a) → | |
| (∀ (b : Set o) → (map-⟸ ∘ map-⟹) Nat b ≡ Nat b) → | |
| (map-⟸ ∘ map-⟹) Nat ≡ Nat | |
| extensionality-Nat Nat forallEQ = | |
| extensionality | |
| {_} {_} | |
| {Set o} {λ (b : Set o) → (r ⟿ b) →₀ F b} | |
| {(map-⟸ ∘ map-⟹) Nat} {Nat} forallEQ | |
| {- Since we have shown id-right-left , id-left-right , proof of Yoneda lemma is complete -} | |
| module WithCategory | |
| {o} | |
| {hom : Hom o l} | |
| (C : Cat hom) | |
| where | |
| _⟿_ = hom | |
| _⟿ᵒᵖ_ = get-homᵒᵖ _⟿_ | |
| infix 5 _⟿_ _⟿ᵒᵖ_ | |
| {- only hom term -} | |
| yonedaEmbeddingHom : {r s : Set o} → | |
| (r ⟿ s) → | |
| (∀ (a : Set o) → (r ⟿ᵒᵖ a) → (s ⟿ᵒᵖ a)) | |
| yonedaEmbeddingHom {r} {s} = Yoneda.map-⟸ (C ᵒᵖ) hom-s⟿ᵒᵖ r | |
| where | |
| hom-s⟿ᵒᵖ : Functor (C ᵒᵖ) 𝕊𝕖𝕥₀ | |
| hom-s⟿ᵒᵖ = homF (C ᵒᵖ) s | |
| s⟿ᵒᵖ = Functor.F hom-s⟿ᵒᵖ | |
| {- also known as Yoneda Functor -} | |
| yonedaEmbeddingHomᵒᵖ : {r s : Set o} → | |
| (r ⟿ᵒᵖ s) → | |
| (∀ (a : Set o) → (r ⟿ a) → (s ⟿ a)) | |
| yonedaEmbeddingHomᵒᵖ {r} {s} = Yoneda.map-⟸ C hom-s⟿ r | |
| where | |
| hom-s⟿ : Functor C 𝕊𝕖𝕥₀ | |
| hom-s⟿ = homF C s | |
| s⟿ = Functor.F hom-s⟿ | |
| {- category to category function -} | |
| yonedaEmbedding : ∀ {o} {hom : Hom o l} (C : Cat hom) → | |
| ∃ (λ (hom₁ : Hom o (l ⊔ lsuc o)) → Cat hom₁) | |
| yonedaEmbedding {o} {hom} C = | |
| _⟿₁_ , | |
| record | |
| { id = id₁ | |
| ; compose = _∘₁_ | |
| ; left-id = left-id₁ | |
| ; right-id = right-id₁ | |
| ; associativity = associativity₁ | |
| } | |
| where | |
| _⟿ᵒᵖ_ = get-homᵒᵖ hom | |
| infix 5 _⟿ᵒᵖ_ | |
| _⟿₁_ : Set o -> Set o -> Set (l ⊔ lsuc o) | |
| r ⟿₁ s = ∀ (a : Set o) → (r ⟿ᵒᵖ a) → (s ⟿ᵒᵖ a) | |
| infix 5 _⟿₁_ | |
| id₁ : ∀ {a} → a ⟿₁ a | |
| id₁ = λ a z → z | |
| _∘₁_ : ∀ {q r s} → (r ⟿₁ s) → (q ⟿₁ r) → (q ⟿₁ s) | |
| _∘₁_ f g a k = f a (g a k) | |
| infixr 9 _∘₁_ | |
| left-id₁ : ∀ {a b} (f : a ⟿₁ b) → id₁ ∘₁ f ≡ f | |
| left-id₁ f = refl | |
| right-id₁ : ∀ {a b} (f : a ⟿₁ b) → f ∘₁ id₁ ≡ f | |
| right-id₁ f = refl | |
| associativity₁ : ∀ {a b c d} (f : c ⟿₁ d) (g : b ⟿₁ c) (h : a ⟿₁ b) → | |
| (f ∘₁ g) ∘₁ h ≡ f ∘₁ (g ∘₁ h) | |
| associativity₁ f g h = refl | |
| {- also known as Yoneda Functor, essentially same as yonedaEmbedding function -} | |
| yonedaEmbeddingᵒᵖ : ∀ {o} {homᵒᵖ : Hom o l} (Cᵒᵖ : Cat homᵒᵖ) → | |
| ∃ (λ (hom₁ : Hom o (l ⊔ lsuc o)) → Cat hom₁) | |
| yonedaEmbeddingᵒᵖ Cᵒᵖ = yonedaEmbedding Cᵒᵖ | |
| {- constructing Functor using yonedaEmbeddingᵒᵖ -} | |
| yonedaFunctor : ∀ {o} {homᵒᵖ : Hom o l} (Cᵒᵖ : Cat homᵒᵖ) → | |
| Functor Cᵒᵖ (proj₂ (yonedaEmbeddingᵒᵖ Cᵒᵖ)) | |
| yonedaFunctor {o} {homᵒᵖ} Cᵒᵖ = | |
| record | |
| { F = Y | |
| ; fmap = fmapʸ | |
| ; fmap-id = fmapʸ-id | |
| ; fmap-dist = fmapʸ-dist | |
| } | |
| where | |
| _⟿ᵒᵖ_ = homᵒᵖ | |
| infix 5 _⟿ᵒᵖ_ | |
| idᵒᵖ = Cat.id Cᵒᵖ | |
| _∘ᵒᵖ_ = Cat.compose Cᵒᵖ | |
| infixr 9 _∘ᵒᵖ_ | |
| _⟿ʸ_ : Hom o (l ⊔ lsuc o) | |
| r ⟿ʸ s = ∀ (a : Set o) → (a ⟿ᵒᵖ r) → (a ⟿ᵒᵖ s) | |
| infix 5 _⟿ʸ_ | |
| Yc : Cat _⟿ʸ_ | |
| Yc = proj₂ (yonedaEmbeddingᵒᵖ Cᵒᵖ) | |
| _∘ʸ_ = Cat.compose Yc | |
| infixr 9 _∘ʸ_ | |
| idʸ : ∀ {a} → a ⟿ʸ a | |
| idʸ = λ a z → z | |
| Y : Set o → Set o | |
| Y a = a | |
| fmapʸ : ∀ {r s} → (r ⟿ᵒᵖ s) → (Y r ⟿ʸ Y s) | |
| fmapʸ {r} {s} f a g = f ∘ᵒᵖ g | |
| fmapʸ-id : ∀ {r} → fmapʸ {r} {r} idᵒᵖ ≡ idʸ | |
| fmapʸ-id = extensionality λ a → extensionality (Cat.left-id Cᵒᵖ) | |
| fmapʸ-dist : ∀ {q r s} {f : r ⟿ᵒᵖ s} {g : q ⟿ᵒᵖ r} → | |
| fmapʸ {q} {s} (f ∘ᵒᵖ g) ≡ fmapʸ {r} {s} f ∘ʸ fmapʸ {q} {r} g | |
| fmapʸ-dist {_} {_} {_} {f} {g} = | |
| extensionality λ a → | |
| extensionality λ h → | |
| Cat.associativity Cᵒᵖ f g h |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment