# HG changeset patch # User Shinji KONO # Date 1678432786 -32400 # Node ID 270f0ba65b88db7854f7683a0e680ba6d9acdf88 # Parent 3cf570d5c285c5942ce49ab48fd1d910e1634817 unify yoneda functor diff -r 3cf570d5c285 -r 270f0ba65b88 src/HomReasoning.agda --- a/src/HomReasoning.agda Wed Jan 25 10:59:28 2023 +0900 +++ b/src/HomReasoning.agda Fri Mar 10 16:19:46 2023 +0900 @@ -30,7 +30,6 @@ TMap : (A : Obj domain) → Hom codomain (FObj F A) (FObj G A) isNTrans : IsNTrans domain codomain F G TMap - module ≈-Reasoning {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where open import Relation.Binary @@ -171,100 +170,7 @@ _∎ _ = relTo refl-hom - --- - -- to avoid assoc storm, flatten composition according to the template - -- - - data MP : { a b : Obj A } ( x : Hom A a b ) → Set (c₁ ⊔ c₂ ⊔ ℓ ) where - am : { a b : Obj A } → (x : Hom A a b ) → MP x - _repl_by_ : { a b : Obj A } → (x y : Hom A a b ) → x ≈ y → MP y - _∙_ : { a b c : Obj A } {x : Hom A b c } { y : Hom A a b } → MP x → MP y → MP ( x o y ) - - open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) - - mp-before : { a b : Obj A } { f : Hom A a b } → MP f → Hom A a b - mp-before (am x) = x - mp-before (x repl y by x₁) = x - mp-before (m ∙ m₁) = mp-before m o mp-before m₁ - - mp-after : { a b : Obj A } { f : Hom A a b } → MP f → Hom A a b - mp-after (am x) = x - mp-after (x repl y by x₁) = y - mp-after (m ∙ m₁) = mp-before m o mp-before m₁ - - mp≈ : { a b : Obj A } { f g : Hom A a b } → (m : MP f ) → mp-before m ≈ mp-after m - mp≈ {a} {b} {f} {g} (am x) = refl-hom - mp≈ {a} {b} {f} {g} (x repl y by x=y ) = x=y - mp≈ {a} {b} {f} {g} (m ∙ m₁) = resp refl-hom refl-hom - - mpf : {a b c : Obj A } {y : Hom A b c } → (m : MP y ) → Hom A a b → Hom A a c - mpf (am x) y = x o y - mpf (x repl y by eq ) z = y o z - mpf (m ∙ m₁) y = mpf m ( mpf m₁ y ) - - mp-flatten : {a b : Obj A } {x : Hom A a b } → (m : MP x ) → Hom A a b - mp-flatten m = mpf m (id _) - - mpl1 : {a b c : Obj A } → Hom A b c → {y : Hom A a b } → MP y → Hom A a c - mpl1 x (am y) = x o y - mpl1 x (z repl y by eq ) = x o y - mpl1 x (y ∙ y1) = mpl1 ( mpl1 x y ) y1 - - mpl : {a b c : Obj A } {x : Hom A b c } {z : Hom A a b } → MP x → MP z → Hom A a c - mpl (am x) m = mpl1 x m - mpl (y repl x by eq ) m = mpl1 x m - mpl (m ∙ m1) m2 = mpl m (m1 ∙ m2) - - mp-flattenl : {a b : Obj A } {x : Hom A a b } → (m : MP x ) → Hom A a b - mp-flattenl m = mpl m (am (id _)) - - _⁻¹ : {a b : Obj A } ( f : Hom A a b ) → Set c₂ - _⁻¹ {a} {b} f = Hom A b a - - test1 : {a b c : Obj A } ( f : Hom A b c ) ( g : Hom A a b ) → ( _⁻¹ : {a b : Obj A } ( f : Hom A a b ) → Hom A b a ) → Hom A c a - test1 f g _⁻¹ = mp-flattenl ((am (g ⁻¹) ∙ am (f ⁻¹) ) ∙ ( (am f ∙ am g) ∙ am ((f o g) ⁻¹ ))) - - test2 : {a b c : Obj A } ( f : Hom A b c ) ( g : Hom A a b ) → ( _⁻¹ : {a b : Obj A } ( f : Hom A a b ) → Hom A b a ) → test1 f g _⁻¹ ≈ ((((g ⁻¹ o f ⁻¹ )o f ) o g ) o (f o g) ⁻¹ ) o id _ - test2 f g _⁻¹ = refl-hom - - test3 : {a b c : Obj A } ( f : Hom A b c ) ( g : Hom A a b ) → ( _⁻¹ : {a b : Obj A } ( f : Hom A a b ) → Hom A b a ) → Hom A c a - test3 f g _⁻¹ = mp-flatten ((am (g ⁻¹) ∙ am (f ⁻¹) ) ∙ ( (am f ∙ am g) ∙ am ((f o g) ⁻¹ ))) - - test4 : {a b c : Obj A } ( f : Hom A b c ) ( g : Hom A a b ) → ( _⁻¹ : {a b : Obj A } ( f : Hom A a b ) → Hom A b a ) → test3 f g _⁻¹ ≈ g ⁻¹ o (f ⁻¹ o (f o (g o ((f o g) ⁻¹ o id _)))) - test4 f g _⁻¹ = refl-hom - - o-flatten : {a b : Obj A } {x : Hom A a b } → (m : MP x ) → x ≈ mp-flatten m - o-flatten (am y) = sym-hom (idR ) - o-flatten (y repl x by eq) = sym-hom (idR ) - o-flatten (am x ∙ q) = resp ( o-flatten q ) refl-hom - o-flatten ((y repl x by eq) ∙ q) = resp ( o-flatten q ) refl-hom - -- d <- c <- b <- a ( p ∙ q ) ∙ r , ( x o y ) o z - o-flatten {a} {d} (_∙_ {a} {b} {d} {xy} {z} (_∙_ {b} {c} {d} {x} {y} p q) r) = - lemma9 _ _ _ ( o-flatten {b} {d} {x o y } (p ∙ q )) ( o-flatten {a} {b} {z} r ) where - mp-cong : { a b c : Obj A } → {p : Hom A b c} {q r : Hom A a b} → (P : MP p) → q ≈ r → mpf P q ≈ mpf P r - mp-cong (am x) q=r = resp q=r refl-hom - mp-cong (y repl x by eq) q=r = resp q=r refl-hom - mp-cong (P ∙ P₁) q=r = mp-cong P ( mp-cong P₁ q=r ) - mp-assoc : {a b c d : Obj A } {p : Hom A c d} {q : Hom A b c} {r : Hom A a b} → (P : MP p) → mpf P q o r ≈ mpf P (q o r ) - mp-assoc (am x) = sym-hom assoc - mp-assoc (y repl x by eq ) = sym-hom assoc - mp-assoc {_} {_} {_} {_} {p} {q} {r} (P ∙ P₁) = begin - mpf P (mpf P₁ q) o r ≈⟨ mp-assoc P ⟩ - mpf P (mpf P₁ q o r) ≈⟨ mp-cong P (mp-assoc P₁) ⟩ mpf P ((mpf P₁) (q o r)) - ∎ - lemma9 : (x : Hom A c d) (y : Hom A b c) (z : Hom A a b) → x o y ≈ mpf p (mpf q (id _)) - → z ≈ mpf r (id _) - → (x o y) o z ≈ mp-flatten ((p ∙ q) ∙ r) - lemma9 x y z t s = begin - (x o y) o z ≈⟨ resp refl-hom t ⟩ - mpf p (mpf q (id _)) o z ≈⟨ mp-assoc p ⟩ - mpf p (mpf q (id _) o z) ≈⟨ mp-cong p (mp-assoc q ) ⟩ - mpf p (mpf q ((id _) o z)) ≈⟨ mp-cong p (mp-cong q idL) ⟩ - mpf p (mpf q z) ≈⟨ mp-cong p (mp-cong q s) ⟩ - mpf p (mpf q (mpf r (id _))) - ∎ - --- an example +-- examples Lemma61 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → { a : Obj A } ( b : Obj A ) → diff -r 3cf570d5c285 -r 270f0ba65b88 src/applicative.agda --- a/src/applicative.agda Wed Jan 25 10:59:28 2023 +0900 +++ b/src/applicative.agda Fri Mar 10 16:19:46 2023 +0900 @@ -26,7 +26,6 @@ -- they say it is not possible to prove FreeTheorem in Agda nor Coq -- https://stackoverflow.com/questions/24718567/is-it-possible-to-get-hold-of-free-theorems-as-propositional-equalities -- so we postulate this --- and we cannot indent a postulate ... open Functor @@ -59,7 +58,6 @@ open import Category.Sets import Relation.Binary.PropositionalEquality - _・_ : {c₁ : Level} { a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c _・_ f g = λ x → f ( g x ) diff -r 3cf570d5c285 -r 270f0ba65b88 src/freyd2.agda --- a/src/freyd2.agda Wed Jan 25 10:59:28 2023 +0900 +++ b/src/freyd2.agda Fri Mar 10 16:19:46 2023 +0900 @@ -6,7 +6,7 @@ where open import HomReasoning -open import cat-utility hiding (Yoneda ; Representable ) +open import cat-utility open import Relation.Binary.Core open import Function @@ -40,48 +40,6 @@ open IsLimit open import Category.Cat -Yoneda : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor A (Sets {c₂}) -Yoneda {c₁} {c₂} {ℓ} A a = record { - FObj = λ b → Hom A a b - ; FMap = λ {x} {y} (f : Hom A x y ) → λ ( g : Hom A a x ) → A [ f o g ] -- f : Hom A x y → Hom Sets (Hom A a x ) (Hom A a y) - ; isFunctor = record { - identity = λ {b} → extensionality A ( λ x → lemma-y-obj1 {b} x ) ; - distr = λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ; - ≈-cong = λ eq → extensionality A ( λ x → lemma-y-obj3 x eq ) - } - } where - lemma-y-obj1 : {b : Obj A } → (x : Hom A a b) → A [ id1 A b o x ] ≡ x - lemma-y-obj1 {b} x = let open ≈-Reasoning A in ≡←≈ A idL - lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c ) → (x : Hom A a a₁ )→ - A [ A [ g o f ] o x ] ≡ (Sets [ _[_o_] A g o _[_o_] A f ]) x - lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning A in ≡←≈ A ( begin - A [ A [ g o f ] o x ] - ≈↑⟨ assoc ⟩ - A [ g o A [ f o x ] ] - ≈⟨⟩ - ( λ x → A [ g o x ] ) ( ( λ x → A [ f o x ] ) x ) - ∎ ) - lemma-y-obj3 : {b c : Obj A} {f g : Hom A b c } → (x : Hom A a b ) → A [ f ≈ g ] → A [ f o x ] ≡ A [ g o x ] - lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning A in ≡←≈ A ( begin - A [ f o x ] - ≈⟨ resp refl-hom eq ⟩ - A [ g o x ] - ∎ ) - --- -- Representable U ≈　Hom(A,-) - -record Representable { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( U : Functor A (Sets {c₂}) ) (a : Obj A) : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ )) where - field - -- FObj U x : A → Set - -- FMap U f = Set → Set (locally small) - -- λ b → Hom (a,b) : A → Set - -- λ f → Hom (a,-) = λ b → Hom a b - - repr→ : NTrans A (Sets {c₂}) U (Yoneda A a ) - repr← : NTrans A (Sets {c₂}) (Yoneda A a) U - reprId→ : {x : Obj A} → Sets [ Sets [ TMap repr→ x o TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (Yoneda A a) x )] - reprId← : {x : Obj A} → Sets [ Sets [ TMap repr← x o TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)] - open Representable _↓_ : { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} { A : Category c₁ c₂ ℓ } { B : Category c₁' c₂' ℓ' } @@ -103,25 +61,26 @@ YonedaFpreserveLimit0 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) (b : Obj A ) - (Γ : Functor I A) (limita : Limit I A Γ) → - IsLimit I Sets (Yoneda A b ○ Γ) (FObj (Yoneda A b) (a0 limita)) (LimitNat I A Sets Γ (a0 limita) (t0 limita) (Yoneda A b)) + (Γ : Functor I (Category.op A)) (limita : Limit I (Category.op A) Γ) → + IsLimit I Sets (Yoneda A (≡←≈ A) b ○ Γ) (FObj (Yoneda A (≡←≈ A) b) (a0 limita)) (LimitNat I (Category.op A) Sets Γ (a0 limita) (t0 limita) (Yoneda A (≡←≈ A) b)) YonedaFpreserveLimit0 {c₁} {c₂} {ℓ} A I b Γ lim = record { limit = λ a t → ψ a t ; t0f=t = λ {a t i} → t0f=t0 a t i ; limit-uniqueness = λ {b} {t} {f} t0f=t → limit-uniqueness0 {b} {t} {f} t0f=t } where - hat0 : NTrans I Sets (K I Sets (FObj (Yoneda A b) (a0 lim))) (Yoneda A b ○ Γ) - hat0 = LimitNat I A Sets Γ (a0 lim) (t0 lim) (Yoneda A b) + opA = Category.op A + hat0 : NTrans I Sets (K I Sets (FObj (Yoneda A (≡←≈ A) b) (a0 lim))) (Yoneda A (≡←≈ A) b ○ Γ) + hat0 = LimitNat I opA Sets Γ (a0 lim) (t0 lim) (Yoneda A (≡←≈ A) b) haa0 : Obj Sets - haa0 = FObj (Yoneda A b) (a0 lim) - ta : (a : Obj Sets) ( x : a ) ( t : NTrans I Sets (K I Sets a) (Yoneda A b ○ Γ)) → NTrans I A (K I A b ) Γ + haa0 = FObj (Yoneda A (≡←≈ A) b) (a0 lim) + ta : (a : Obj Sets) ( x : a ) ( t : NTrans I Sets (K I Sets a) (Yoneda A (≡←≈ A) b ○ Γ)) → NTrans I opA (K I opA b ) Γ ta a x t = record { TMap = λ i → (TMap t i ) x ; isNTrans = record { commute = commute1 } } where commute1 : {a₁ b₁ : Obj I} {f : Hom I a₁ b₁} → - A [ A [ FMap Γ f o TMap t a₁ x ] ≈ A [ TMap t b₁ x o FMap (K I A b) f ] ] - commute1 {a₁} {b₁} {f} = let open ≈-Reasoning A in begin + opA [ opA [ FMap Γ f o TMap t a₁ x ] ≈ opA [ TMap t b₁ x o FMap (K I opA b) f ] ] + commute1 {a₁} {b₁} {f} = let open ≈-Reasoning opA in begin FMap Γ f o TMap t a₁ x ≈⟨⟩ - ( ( FMap (Yoneda A b ○ Γ ) f ) * TMap t a₁ ) x + ( ( FMap (Yoneda A (≡←≈ A) b ○ Γ ) f ) * TMap t a₁ ) x ≈⟨ ≈←≡ ( cong (λ k → k x ) (IsNTrans.commute (isNTrans t)) ) ⟩ ( TMap t b₁ * ( FMap (K I Sets a) f ) ) x ≈⟨⟩ @@ -131,17 +90,17 @@ ≈↑⟨ idR ⟩ TMap t b₁ x o id1 A b ≈⟨⟩ - TMap t b₁ x o FMap (K I A b) f + TMap t b₁ x o FMap (K I opA b) f ∎ - ψ : (X : Obj Sets) ( t : NTrans I Sets (K I Sets X) (Yoneda A b ○ Γ)) - → Hom Sets X (FObj (Yoneda A b) (a0 lim)) - ψ X t x = FMap (Yoneda A b) (limit (isLimit lim) b (ta X x t )) (id1 A b ) - t0f=t0 : (a : Obj Sets ) ( t : NTrans I Sets (K I Sets a) (Yoneda A b ○ Γ)) (i : Obj I) - → Sets [ Sets [ TMap (LimitNat I A Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t ] ≈ TMap t i ] - t0f=t0 a t i = let open ≈-Reasoning A in extensionality A ( λ x → ≡←≈ A ( begin - ( Sets [ TMap (LimitNat I A Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t ] ) x + ψ : (X : Obj Sets) ( t : NTrans I Sets (K I Sets X) (Yoneda A (≡←≈ A) b ○ Γ)) + → Hom Sets X (FObj (Yoneda A (≡←≈ A) b) (a0 lim)) + ψ X t x = FMap (Yoneda A (≡←≈ A) b) (limit (isLimit lim) b (ta X x t )) (id1 A b ) + t0f=t0 : (a : Obj Sets ) ( t : NTrans I Sets (K I Sets a) (Yoneda A (≡←≈ A) b ○ Γ)) (i : Obj I) + → Sets [ Sets [ TMap (LimitNat I opA Sets Γ (a0 lim) (t0 lim) (Yoneda A (≡←≈ A) b)) i o ψ a t ] ≈ TMap t i ] + t0f=t0 a t i = let open ≈-Reasoning opA in extensionality opA ( λ x → (≡←≈ A) ( begin + ( Sets [ TMap (LimitNat I opA Sets Γ (a0 lim) (t0 lim) (Yoneda A (≡←≈ A) b)) i o ψ a t ] ) x ≈⟨⟩ - FMap (Yoneda A b) ( TMap (t0 lim) i) (FMap (Yoneda A b) (limit (isLimit lim) b (ta a x t )) (id1 A b )) + FMap (Yoneda A (≡←≈ A) b) ( TMap (t0 lim) i) (FMap (Yoneda A (≡←≈ A) b) (limit (isLimit lim) b (ta a x t )) (id1 A b )) ≈⟨⟩ -- FMap (Hom A b ) f g = A [ f o g ] TMap (t0 lim) i o (limit (isLimit lim) b (ta a x t ) o id1 A b ) ≈⟨ cdr idR ⟩ @@ -151,13 +110,13 @@ ≈⟨⟩ TMap t i x ∎ )) - limit-uniqueness0 : {a : Obj Sets} {t : NTrans I Sets (K I Sets a) (Yoneda A b ○ Γ)} {f : Hom Sets a (FObj (Yoneda A b) (a0 lim))} → - ({i : Obj I} → Sets [ Sets [ TMap (LimitNat I A Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o f ] ≈ TMap t i ]) → + limit-uniqueness0 : {a : Obj Sets} {t : NTrans I Sets (K I Sets a) (Yoneda A (≡←≈ A) b ○ Γ)} {f : Hom Sets a (FObj (Yoneda A (≡←≈ A) b) (a0 lim))} → + ({i : Obj I} → Sets [ Sets [ TMap (LimitNat I opA Sets Γ (a0 lim) (t0 lim) (Yoneda A (≡←≈ A) b)) i o f ] ≈ TMap t i ]) → Sets [ ψ a t ≈ f ] - limit-uniqueness0 {a} {t} {f} t0f=t = let open ≈-Reasoning A in extensionality A ( λ x → ≡←≈ A ( begin + limit-uniqueness0 {a} {t} {f} t0f=t = let open ≈-Reasoning opA in extensionality A ( λ x → (≡←≈ A) ( begin ψ a t x ≈⟨⟩ - FMap (Yoneda A b) (limit (isLimit lim) b (ta a x t )) (id1 A b ) + FMap (Yoneda A (≡←≈ A) b) (limit (isLimit lim) b (ta a x t )) (id1 A b ) ≈⟨⟩ limit (isLimit lim) b (ta a x t ) o id1 A b ≈⟨ idR ⟩ @@ -168,9 +127,9 @@ YonedaFpreserveLimit : {c₁ c₂ ℓ : Level} (I : Category c₁ c₂ ℓ) (A : Category c₁ c₂ ℓ) - (b : Obj A ) → LimitPreserve I A Sets (Yoneda A b) -YonedaFpreserveLimit I A b = record { - preserve = λ Γ lim → YonedaFpreserveLimit0 A I b Γ lim + (b : Obj A ) → LimitPreserve I (Category.op A) Sets (Yoneda A (≡←≈ A) b) +YonedaFpreserveLimit I opA b = record { + preserve = λ Γ lim → YonedaFpreserveLimit0 opA I b Γ lim } @@ -184,32 +143,33 @@ KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (a : Obj A ) - → HasInitialObject ( K A Sets * ↓ (Yoneda A a) ) ( record { obj = a ; hom = λ x → id1 A a } ) + → HasInitialObject ( K (Category.op A) Sets * ↓ (Yoneda A (≡←≈ A) a) ) ( record { obj = a ; hom = λ x → id1 A a } ) KUhasInitialObj {c₁} {c₂} {ℓ} A a = record { initial = λ b → initial0 b ; uniqueness = λ f → unique f } where + opA = Category.op A commaCat : Category (c₂ ⊔ c₁) c₂ ℓ - commaCat = K A Sets * ↓ Yoneda A a - initObj : Obj (K A Sets * ↓ Yoneda A a) + commaCat = K opA Sets * ↓ Yoneda A (≡←≈ A) a + initObj : Obj (K opA Sets * ↓ Yoneda A (≡←≈ A) a) initObj = record { obj = a ; hom = λ x → id1 A a } - comm2 : (b : Obj commaCat) ( x : * ) → ( Sets [ FMap (Yoneda A a) (hom b OneObj) o (λ x₁ → id1 A a) ] ) x ≡ hom b x - comm2 b OneObj = let open ≈-Reasoning A in ≡←≈ A ( begin - ( Sets [ FMap (Yoneda A a) (hom b OneObj) o (λ x₁ → id1 A a) ] ) OneObj + comm2 : (b : Obj commaCat) ( x : * ) → ( Sets [ FMap (Yoneda A (≡←≈ A) a) (hom b OneObj) o (λ x₁ → id1 A a) ] ) x ≡ hom b x + comm2 b OneObj = let open ≈-Reasoning opA in (≡←≈ A) ( begin + ( Sets [ FMap (Yoneda A (≡←≈ A) a) (hom b OneObj) o (λ x₁ → id1 A a) ] ) OneObj ≈⟨⟩ - FMap (Yoneda A a) (hom b OneObj) (id1 A a) + FMap (Yoneda A (≡←≈ A) a) (hom b OneObj) (id1 A a) ≈⟨⟩ hom b OneObj o id1 A a ≈⟨ idR ⟩ hom b OneObj ∎ ) - comm1 : (b : Obj commaCat) → Sets [ Sets [ FMap (Yoneda A a) (hom b OneObj) o hom initObj ] ≈ Sets [ hom b o FMap (K A Sets *) (hom b OneObj) ] ] + comm1 : (b : Obj commaCat) → Sets [ Sets [ FMap (Yoneda A (≡←≈ A) a) (hom b OneObj) o hom initObj ] ≈ Sets [ hom b o FMap (K opA Sets *) (hom b OneObj) ] ] comm1 b = let open ≈-Reasoning Sets in begin - FMap (Yoneda A a) (hom b OneObj) o ( λ x → id1 A a ) + FMap (Yoneda A (≡←≈ A) a) (hom b OneObj) o ( λ x → id1 A a ) ≈⟨ extensionality A ( λ x → comm2 b x ) ⟩ hom b ≈⟨⟩ - hom b o FMap (K A Sets *) (hom b OneObj) + hom b o FMap (K opA Sets *) (hom b OneObj) ∎ initial0 : (b : Obj commaCat) → Hom commaCat initObj b @@ -217,22 +177,22 @@ arrow = hom b OneObj ; comm = comm1 b } -- what is comm f ? - comm-f : (b : Obj (K A Sets * ↓ (Yoneda A a))) (f : Hom (K A Sets * ↓ Yoneda A a) initObj b) - → Sets [ Sets [ FMap (Yoneda A a) (arrow f) o ( λ x → id1 A a ) ] - ≈ Sets [ hom b o FMap (K A Sets *) (arrow f) ] ] + comm-f : (b : Obj (K opA Sets * ↓ (Yoneda A (≡←≈ A) a))) (f : Hom (K opA Sets * ↓ Yoneda A (≡←≈ A) a) initObj b) + → Sets [ Sets [ FMap (Yoneda A (≡←≈ A) a) (arrow f) o ( λ x → id1 A a ) ] + ≈ Sets [ hom b o FMap (K opA Sets *) (arrow f) ] ] comm-f b f = comm f - unique : {b : Obj (K A Sets * ↓ Yoneda A a)} (f : Hom (K A Sets * ↓ Yoneda A a) initObj b) - → (K A Sets * ↓ Yoneda A a) [ f ≈ initial0 b ] - unique {b} f = let open ≈-Reasoning A in begin + unique : {b : Obj (K opA Sets * ↓ Yoneda A (≡←≈ A) a)} (f : Hom (K opA Sets * ↓ Yoneda A (≡←≈ A) a) initObj b) + → (K opA Sets * ↓ Yoneda A (≡←≈ A) a) [ f ≈ initial0 b ] + unique {b} f = let open ≈-Reasoning opA in begin arrow f ≈↑⟨ idR ⟩ arrow f o id1 A a ≈⟨⟩ - ( Sets [ FMap (Yoneda A a) (arrow f) o id1 Sets (FObj (Yoneda A a) a) ] ) (id1 A a) + ( Sets [ FMap (Yoneda A (≡←≈ A) a) (arrow f) o id1 Sets (FObj (Yoneda A (≡←≈ A) a) a) ] ) (id1 A a) ≈⟨⟩ - ( Sets [ FMap (Yoneda A a) (arrow f) o ( λ x → id1 A a ) ] ) OneObj + ( Sets [ FMap (Yoneda A (≡←≈ A) a) (arrow f) o ( λ x → id1 A a ) ] ) OneObj ≈⟨ ≈←≡ ( cong (λ k → k OneObj ) (comm f )) ⟩ - ( Sets [ hom b o FMap (K A Sets *) (arrow f) ] ) OneObj + ( Sets [ hom b o FMap (K opA Sets *) (arrow f) ] ) OneObj ≈⟨⟩ hom b OneObj ∎ @@ -278,77 +238,78 @@ -- if K{*}↓U has initial Obj, U is representable UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) - (U : Functor A (Sets {c₂}) ) - ( i : Obj ( K A Sets * ↓ U) ) - (In : HasInitialObject ( K A Sets * ↓ U) i ) - → Representable A U (obj i) + (U : Functor (Category.op A) (Sets {c₂}) ) + ( i : Obj ( K (Category.op A) Sets * ↓ U) ) + (In : HasInitialObject ( K (Category.op A) Sets * ↓ U) i ) + → Representable A (≡←≈ A) U (obj i) UisRepresentable A U i In = record { repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } } ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = comm2 } } ; reprId→ = iso→ ; reprId← = iso← } where - comm11 : (a b : Obj A) (f : Hom A a b) (y : FObj U a ) → - ( Sets [ FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In (ob A U a x))) ] ) y - ≡ (Sets [ ( λ x → arrow (initial In (ob A U b x))) o FMap U f ] ) y + opA = Category.op A + comm11 : (a b : Obj opA) (f : Hom opA a b) (y : FObj U a ) → + ( Sets [ FMap (Yoneda A (≡←≈ A) (obj i)) f o ( λ x → arrow (initial In (ob opA U a x))) ] ) y + ≡ (Sets [ ( λ x → arrow (initial In (ob opA U b x))) o FMap U f ] ) y comm11 a b f y = begin - ( Sets [ FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In (ob A U a x))) ] ) y + ( Sets [ FMap (Yoneda A (≡←≈ A) (obj i)) f o ( λ x → arrow (initial In (ob opA U a x))) ] ) y ≡⟨⟩ - A [ f o arrow (initial In (ob A U a y)) ] + opA [ f o arrow (initial In (ob opA U a y)) ] ≡⟨⟩ - A [ arrow ( fArrow A U f y ) o arrow (initial In (ob A U a y)) ] - ≡⟨ ≡←≈ A ( uniqueness In {ob A U b (FMap U f y) } (( K A Sets * ↓ U) [ fArrow A U f y o initial In (ob A U a y)] ) ) ⟩ - arrow (initial In (ob A U b (FMap U f y) )) + opA [ arrow ( fArrow opA U f y ) o arrow (initial In (ob opA U a y)) ] + ≡⟨ (≡←≈ A) ( uniqueness In {ob opA U b (FMap U f y) } (( K opA Sets * ↓ U) [ fArrow opA U f y o initial In (ob opA U a y)] ) ) ⟩ + arrow (initial In (ob opA U b (FMap U f y) )) ≡⟨⟩ - (Sets [ ( λ x → arrow (initial In (ob A U b x))) o FMap U f ] ) y + (Sets [ ( λ x → arrow (initial In (ob opA U b x))) o FMap U f ] ) y ∎ where open import Relation.Binary.PropositionalEquality open ≡-Reasoning - tmap1 : (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj i)) b) - tmap1 b x = arrow ( initial In (ob A U b x ) ) - comm1 : {a b : Obj A} {f : Hom A a b} → Sets [ Sets [ FMap (Yoneda A (obj i)) f o tmap1 a ] ≈ Sets [ tmap1 b o FMap U f ] ] + tmap1 : (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (≡←≈ A) (obj i)) b) + tmap1 b x = arrow ( initial In (ob opA U b x ) ) + comm1 : {a b : Obj opA} {f : Hom opA a b} → Sets [ Sets [ FMap (Yoneda A (≡←≈ A) (obj i)) f o tmap1 a ] ≈ Sets [ tmap1 b o FMap U f ] ] comm1 {a} {b} {f} = let open ≈-Reasoning Sets in begin - FMap (Yoneda A (obj i)) f o tmap1 a + FMap (Yoneda A (≡←≈ A) (obj i)) f o tmap1 a ≈⟨⟩ - FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In ( ob A U a x ))) + FMap (Yoneda A (≡←≈ A) (obj i)) f o ( λ x → arrow (initial In ( ob opA U a x ))) ≈⟨ extensionality Sets ( λ y → comm11 a b f y ) ⟩ - ( λ x → arrow (initial In (ob A U b x))) o FMap U f + ( λ x → arrow (initial In (ob opA U b x))) o FMap U f ≈⟨⟩ tmap1 b o FMap U f ∎ - comm21 : (a b : Obj A) (f : Hom A a b) ( y : Hom A (obj i) a ) → + comm21 : (a b : Obj opA) (f : Hom opA a b) ( y : Hom opA (obj i) a ) → (Sets [ FMap U f o (λ x → FMap U x (hom i OneObj))] ) y ≡ - (Sets [ ( λ x → (FMap U x ) (hom i OneObj)) o (λ x → A [ f o x ] ) ] ) y + (Sets [ ( λ x → (FMap U x ) (hom i OneObj)) o (λ x → opA [ f o x ] ) ] ) y comm21 a b f y = begin FMap U f ( FMap U y (hom i OneObj)) ≡⟨ ≡-cong ( λ k → k (hom i OneObj)) ( sym ( IsFunctor.distr (isFunctor U ) ) ) ⟩ - (FMap U (A [ f o y ] ) ) (hom i OneObj) + (FMap U (opA [ f o y ] ) ) (hom i OneObj) ∎ where open import Relation.Binary.PropositionalEquality open ≡-Reasoning - tmap2 : (b : Obj A) → Hom Sets (FObj (Yoneda A (obj i)) b) (FObj U b) + tmap2 : (b : Obj A) → Hom Sets (FObj (Yoneda A (≡←≈ A) (obj i)) b) (FObj U b) tmap2 b x = ( FMap U x ) ( hom i OneObj ) - comm2 : {a b : Obj A} {f : Hom A a b} → Sets [ Sets [ FMap U f o tmap2 a ] ≈ - Sets [ tmap2 b o FMap (Yoneda A (obj i)) f ] ] + comm2 : {a b : Obj opA} {f : Hom opA a b} → Sets [ Sets [ FMap U f o tmap2 a ] ≈ + Sets [ tmap2 b o FMap (Yoneda A (≡←≈ A) (obj i)) f ] ] comm2 {a} {b} {f} = let open ≈-Reasoning Sets in begin FMap U f o tmap2 a ≈⟨⟩ FMap U f o ( λ x → ( FMap U x ) ( hom i OneObj ) ) ≈⟨ extensionality Sets ( λ y → comm21 a b f y ) ⟩ - ( λ x → ( FMap U x ) ( hom i OneObj ) ) o ( λ x → A [ f o x ] ) + ( λ x → ( FMap U x ) ( hom i OneObj ) ) o ( λ x → opA [ f o x ] ) ≈⟨⟩ - ( λ x → ( FMap U x ) ( hom i OneObj ) ) o FMap (Yoneda A (obj i)) f + ( λ x → ( FMap U x ) ( hom i OneObj ) ) o FMap (Yoneda A (≡←≈ A) (obj i)) f ≈⟨⟩ - tmap2 b o FMap (Yoneda A (obj i)) f + tmap2 b o FMap (Yoneda A (≡←≈ A) (obj i)) f ∎ - iso0 : ( x : Obj A) ( y : Hom A (obj i ) x ) ( z : * ) - → ( Sets [ FMap U y o hom i ] ) z ≡ ( Sets [ ub A U x (FMap U y (hom i OneObj)) o FMap (K A Sets *) y ] ) z + iso0 : ( x : Obj opA) ( y : Hom opA (obj i ) x ) ( z : * ) + → ( Sets [ FMap U y o hom i ] ) z ≡ ( Sets [ ub opA U x (FMap U y (hom i OneObj)) o FMap (K opA Sets *) y ] ) z iso0 x y OneObj = refl - iso→ : {x : Obj A} → Sets [ Sets [ tmap1 x o tmap2 x ] ≈ id1 Sets (FObj (Yoneda A (obj i)) x) ] - iso→ {x} = let open ≈-Reasoning A in extensionality Sets ( λ ( y : Hom A (obj i ) x ) → ≡←≈ A ( begin + iso→ : {x : Obj opA} → Sets [ Sets [ tmap1 x o tmap2 x ] ≈ id1 Sets (FObj (Yoneda A (≡←≈ A) (obj i)) x) ] + iso→ {x} = let open ≈-Reasoning opA in extensionality Sets ( λ ( y : Hom opA (obj i ) x ) → (≡←≈ A) ( begin ( Sets [ tmap1 x o tmap2 x ] ) y ≈⟨⟩ - arrow ( initial In (ob A U x (( FMap U y ) ( hom i OneObj ) ))) + arrow ( initial In (ob opA U x (( FMap U y ) ( hom i OneObj ) ))) ≈↑⟨ uniqueness In (record { arrow = y ; comm = extensionality Sets ( λ (z : * ) → iso0 x y z ) } ) ⟩ y ∎ )) @@ -356,9 +317,9 @@ iso← {x} = extensionality Sets ( λ (y : FObj U x ) → ( begin ( Sets [ tmap2 x o tmap1 x ] ) y ≡⟨⟩ - ( FMap U ( arrow ( initial In (ob A U x y ) )) ) ( hom i OneObj ) - ≡⟨ ≡-cong (λ k → k OneObj) ( comm ( initial In (ob A U x y ) )) ⟩ - hom (ob A U x y) OneObj + ( FMap U ( arrow ( initial In (ob opA U x y ) )) ) ( hom i OneObj ) + ≡⟨ ≡-cong (λ k → k OneObj) ( comm ( initial In (ob opA U x y ) )) ⟩ + hom (ob opA U x y) OneObj ≡⟨⟩ y ∎ ) ) where @@ -400,7 +361,7 @@ B [ B [ FMap U g o tmap-η a ] ≈ f ] → A [ arrow (solution f) ≈ g ] unique {a} {b} {f} {g} ugη=f = let open ≈-Reasoning A in begin arrow (solution f) - ≈↑⟨ ≈←≡ ( cong (λ k → arrow (solution k)) ( ≡←≈ B ugη=f )) ⟩ + ≈↑⟨ ≈←≡ ( cong (λ k → arrow (solution k)) ( (≡←≈ B) ugη=f )) ⟩ arrow (solution (B [ FMap U g o tmap-η a ] )) ≈↑⟨ uniqueness (In a) (record { arrow = g ; comm = comm1 }) ⟩ g diff -r 3cf570d5c285 -r 270f0ba65b88 src/yoneda.agda --- a/src/yoneda.agda Wed Jan 25 10:59:28 2023 +0900 +++ b/src/yoneda.agda Fri Mar 10 16:19:46 2023 +0900 @@ -77,7 +77,7 @@ -- A is Locally small postulate ≈-≡ : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y ----- +--- -- -- Object mapping in Yoneda Functor -- @@ -86,27 +86,7 @@ open import Function y-obj : (a : Obj A) → Functor (Category.op A) (Sets {c₂}) -y-obj a = record { - FObj = λ b → Hom (Category.op A) a b ; - FMap = λ {b c : Obj A } → λ ( f : Hom A c b ) → λ (g : Hom A b a ) → (Category.op A) [ f o g ] ; - isFunctor = record { - identity = λ {b} → extensionality A ( λ x → lemma-y-obj1 {b} x ) ; - distr = λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ; - ≈-cong = λ eq → extensionality A ( λ x → lemma-y-obj3 x eq ) - } - } where - lemma-y-obj1 : {b : Obj A } → (x : Hom A b a) → (Category.op A) [ id1 A b o x ] ≡ x - lemma-y-obj1 {b} x = let open ≈-Reasoning (Category.op A) in ≈-≡ A idL - lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A b a₁) (g : Hom A c b ) → (x : Hom A a₁ a )→ - Category.op A [ Category.op A [ g o f ] o x ] ≡ (Sets [ _[_o_] (Category.op A) g o _[_o_] (Category.op A) f ]) x - lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning (Category.op A) in ≈-≡ A ( begin - Category.op A [ Category.op A [ g o f ] o x ] ≈↑⟨ assoc ⟩ - Category.op A [ g o Category.op A [ f o x ] ] ≈⟨⟩ - ( λ x → Category.op A [ g o x ] ) ( ( λ x → Category.op A [ f o x ] ) x ) ∎ ) - lemma-y-obj3 : {b c : Obj A} {f g : Hom A c b } → (x : Hom A b a ) → A [ f ≈ g ] → Category.op A [ f o x ] ≡ Category.op A [ g o x ] - lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning (Category.op A) in ≈-≡ A ( begin - Category.op A [ f o x ] ≈⟨ resp refl-hom eq ⟩ - Category.op A [ g o x ] ∎ ) +y-obj a = Yoneda A (≈-≡ A) a ---- -- @@ -405,3 +385,4 @@ Yoneda-full-embed {a} {b} eq = ylem0 ylem1 where ylem1 : Hom A a a ≡ Hom A a b ylem1 = cong (λ k → FObj k a) eq +