# HG changeset patch # User Shinji KONO # Date 1614907220 -32400 # Node ID 99c91423b871fd7f5f0c4d58b67eedc30538adc5 # Parent e2e11014b0f816b61d66e54d906848057614b201 ... diff -r e2e11014b0f8 -r 99c91423b871 src/SetsCompleteness.agda --- a/src/SetsCompleteness.agda Thu Mar 04 18:51:10 2021 +0900 +++ b/src/SetsCompleteness.agda Fri Mar 05 10:20:20 2021 +0900 @@ -202,31 +202,28 @@ open import Relation.Binary.PropositionalEquality open ≡-Reasoning --- data cequ {c : Level} (A B : Set c) ( f g : A → B ) : Set c where --- casef : (a : A) → {!!} - -record cequ {c : Level} (A B : Set c) ( f g : A → B ) : Set c where - field - q : B → B - qo : (a : A) → q (f a) ≡ q (g a) +data cequ {c : Level} {A B : Set c} ( f g : A → B ) : Set c where + celem : (b : B) → (a : A) → f a ≡ b → g a ≡ b → cequ f g -data cequ' {c : Level} {A B : Set c} ( f g : A → B ) : {a : A } → (f a ≡ g a) → Set c where - celem : {a : A } → (f=g : f a ≡ g a) → cequ' f g f=g +record cequ' {c : Level} {A B : Set c} ( f g : A → B ) : Set c where + field + cb : B + celem' : (a : A ) → f a ≡ cb → g a ≡ cb -c-equ : { c₂ : Level} {a b : Obj (Sets {c₂}) } ( f g : Hom (Sets {c₂}) a b ) → (x : b) → cequ a b f g -c-equ {_} {a} {b} f g x = record { q = {!!} ; qo = {!!} } +c-equ : { c₂ : Level} {a b : Obj (Sets {c₂}) } ( f g : Hom (Sets {c₂}) a b ) → b → cequ f g +c-equ {_} {a} {b} f g = {!!} -SetsIsCoEqualizer : { c₂ : Level} → (a b : Obj (Sets {c₂}) ) (f g : Hom (Sets {c₂}) a b) → IsCoEqualizer Sets (λ x → c-equ {c₂} f g x) f g +SetsIsCoEqualizer : { c₂ : Level} → (a b : Obj (Sets {c₂}) ) (f g : Hom (Sets {c₂}) a b) → IsCoEqualizer Sets (c-equ f g) f g SetsIsCoEqualizer {c₂} a b f g = record { ef=eg = extensionality Sets {!!} ; k = k ; ke=h = λ {d} {h} {eq} → ke=h {d} {h} {eq} ; uniqueness = {!!} } where - k : {d : Obj Sets} (h : Hom Sets b d) → Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] → Hom Sets (cequ a b f g) d + k : {d : Obj Sets} (h : Hom Sets b d) → Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] → Hom Sets {!!} d k = {!!} ke=h : {d : Obj Sets } {h : Hom Sets b d } → { eq : Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] } - → Sets [ Sets [ k h eq o c-equ f g ] ≈ h ] + → Sets [ Sets [ k h eq o {!!} ] ≈ h ] ke=h = {!!} open Functor diff -r e2e11014b0f8 -r 99c91423b871 src/yoneda.agda --- a/src/yoneda.agda Thu Mar 04 18:51:10 2021 +0900 +++ b/src/yoneda.agda Fri Mar 05 10:20:20 2021 +0900 @@ -9,8 +9,7 @@ open import Category -- https://github.com/konn/category-agda open import Level open import Category.Sets -module yoneda where --- { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where +module yoneda { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) where open import HomReasoning open import cat-utility @@ -25,20 +24,20 @@ open Functor -YObj : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) -YObj {_} {c₂} A = Functor (Category.op A) (Sets {c₂}) -YHom : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (f : YObj A ) → (g : YObj A ) → Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) -YHom {_} {c₂} A f g = NTrans (Category.op A) (Sets {c₂}) f g +YObj : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) +YObj = Functor (Category.op A) (Sets {c₂}) +YHom : ( f : YObj ) → (g : YObj ) → Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) +YHom f g = NTrans (Category.op A) (Sets {c₂}) f g open NTrans -Yid : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a : YObj A } → YHom A a a -Yid {_} {c₂} A {a} = record { TMap = λ a → λ x → x ; isNTrans = isNTrans1 {a} } where - isNTrans1 : {a : YObj A } → IsNTrans (Category.op A) (Sets {c₂}) a a (λ a → λ x → x ) +Yid : {a : YObj } → YHom a a +Yid {a} = record { TMap = λ a → λ x → x ; isNTrans = isNTrans1 {a} } where + isNTrans1 : {a : YObj } → IsNTrans (Category.op A) (Sets {c₂}) a a (λ a → λ x → x ) isNTrans1 {a} = record { commute = refl } -_+_ : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } {a b c : YObj A} → YHom A b c → YHom A a b → YHom A a c -_+_ {_} {c₂} {_} {A} {a} {b} {c} f g = record { TMap = λ x → Sets [ TMap f x o TMap g x ] ; isNTrans = isNTrans1 } where - commute1 : (a b c : YObj A ) (f : YHom A b c) (g : YHom A a b ) +_+_ : {a b c : YObj} → YHom b c → YHom a b → YHom a c +_+_ {a} {b} {c} f g = record { TMap = λ x → Sets [ TMap f x o TMap g x ] ; isNTrans = isNTrans1 } where + commute1 : (a b c : YObj ) (f : YHom b c) (g : YHom a b ) (a₁ b₁ : Obj (Category.op A)) (h : Hom (Category.op A) a₁ b₁) → Sets [ Sets [ FMap c h o Sets [ TMap f a₁ o TMap g a₁ ] ] ≈ Sets [ Sets [ TMap f b₁ o TMap g b₁ ] o FMap a h ] ] @@ -58,13 +57,13 @@ isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) a c (λ x → Sets [ TMap f x o TMap g x ]) isNTrans1 = record { commute = λ {a₁ b₁ h} → commute1 a b c f g a₁ b₁ h } -_==_ : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } {a b : YObj A} → YHom A a b → YHom A a b → Set (c₂ ⊔ c₁) -_==_ {_} { c₂} {_} {A} f g = ∀{x : Obj (Category.op A)} → (Sets {c₂}) [ TMap f x ≈ TMap g x ] +_==_ : {a b : YObj} → YHom a b → YHom a b → Set (c₂ ⊔ c₁) +_==_ f g = ∀{x : Obj (Category.op A)} → (Sets {c₂}) [ TMap f x ≈ TMap g x ] infix 4 _==_ -isSetsAop : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → IsCategory (YObj A) (YHom A) _==_ _+_ ( Yid A ) -isSetsAop {_} {c₂} {_} A = +isSetsAop : IsCategory (YObj) (YHom) _==_ _+_ ( Yid ) +isSetsAop = record { isEquivalence = record {refl = refl ; trans = λ {i j k} → trans1 {_} {_} {i} {j} {k} ; sym = λ {i j} → sym1 {_} {_} {i} {j}} ; identityL = refl ; identityR = refl @@ -72,22 +71,22 @@ ; associative = refl } where open ≈-Reasoning (Sets {c₂}) - sym1 : {a b : YObj A } {i j : YHom A a b } → i == j → j == i + sym1 : {a b : YObj } {i j : YHom a b } → i == j → j == i sym1 {a} {b} {i} {j} eq {x} = sym eq - trans1 : {a b : YObj A } {i j k : YHom A a b} → i == j → j == k → i == k + trans1 : {a b : YObj } {i j k : YHom a b} → i == j → j == k → i == k trans1 {a} {b} {i} {j} {k} i=j j=k {x} = trans-hom i=j j=k - o-resp-≈ : {A₁ B C : YObj A} {f g : YHom A A₁ B} {h i : YHom A B C} → + o-resp-≈ : {A₁ B C : YObj} {f g : YHom A₁ B} {h i : YHom B C} → f == g → h == i → h + f == i + g o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f=g h=i {x} = resp f=g h=i -SetsAop : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Category (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) (c₂ ⊔ c₁) -SetsAop {_} {c₂} {_} A = - record { Obj = YObj A - ; Hom = YHom A +SetsAop : Category (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) (c₂ ⊔ c₁) +SetsAop = + record { Obj = YObj + ; Hom = YHom ; _o_ = _+_ ; _≈_ = _==_ - ; Id = Yid A - ; isCategory = isSetsAop A + ; Id = Yid + ; isCategory = isSetsAop } -- A is Locally small @@ -105,8 +104,8 @@ open import Function -y-obj : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor (Category.op A) (Sets {c₂}) -y-obj {_} {c₂} {_} A a = record { +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 { @@ -140,21 +139,21 @@ -- ---- -y-tmap : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( a b : Obj A ) → (f : Hom A a b ) → (x : Obj (Category.op A)) → - FObj (y-obj A a) x → FObj (y-obj A b ) x -y-tmap {_} {c₂} {_} A a b f x = λ ( g : Hom A x a ) → A [ f o g ] -- ( h : Hom A x b ) +y-tmap : ( a b : Obj A ) → (f : Hom A a b ) → (x : Obj (Category.op A)) → + FObj (y-obj a) x → FObj (y-obj b ) x +y-tmap a b f x = λ ( g : Hom A x a ) → A [ f o g ] -- ( h : Hom A x b ) -y-map : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A } → (f : Hom A a b ) → YHom A (y-obj A a) (y-obj A b) -y-map {_} {c₂} {_} A {a} {b} f = record { TMap = y-tmap A a b f ; isNTrans = isNTrans1 {a} {b} f } where +y-map : {a b : Obj A } → (f : Hom A a b ) → YHom (y-obj a) (y-obj b) +y-map {a} {b} f = record { TMap = y-tmap a b f ; isNTrans = isNTrans1 {a} {b} f } where lemma-y-obj4 : {a₁ b₁ : Obj (Category.op A)} {g : Hom (Category.op A) a₁ b₁} → {a b : Obj A } → (f : Hom A a b ) → - Sets [ Sets [ FMap (y-obj A b) g o y-tmap A a b f a₁ ] ≈ - Sets [ y-tmap A a b f b₁ o FMap (y-obj A a) g ] ] + Sets [ Sets [ FMap (y-obj b) g o y-tmap a b f a₁ ] ≈ + Sets [ y-tmap a b f b₁ o FMap (y-obj a) g ] ] lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ {_} {_} {_} {A} ( begin A [ A [ f o x ] o g ] ≈↑⟨ assoc ⟩ A [ f o A [ x o g ] ] ∎ ) ) - isNTrans1 : {a b : Obj A } → (f : Hom A a b ) → IsNTrans (Category.op A) (Sets {c₂}) (y-obj A a) (y-obj A b) (y-tmap A a b f ) + isNTrans1 : {a b : Obj A } → (f : Hom A a b ) → IsNTrans (Category.op A) (Sets {c₂}) (y-obj a) (y-obj b) (y-tmap a b f ) isNTrans1 {a} {b} f = record { commute = λ{a₁ b₁ g } → lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f } ----- @@ -163,10 +162,10 @@ -- ----- -YonedaFunctor : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Functor A (SetsAop A) -YonedaFunctor A = record { - FObj = λ a → y-obj A a - ; FMap = λ f → y-map A f +YonedaFunctor : Functor A SetsAop +YonedaFunctor = record { + FObj = λ a → y-obj a + ; FMap = λ f → y-map f ; isFunctor = record { identity = identity ; distr = distr1 @@ -174,24 +173,24 @@ } } where - ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → SetsAop A [ y-map A f ≈ y-map A g ] - ≈-cong {a} {b} {f} {g} eq = let open ≈-Reasoning (A) in -- (λ x g₁ → A [ f o g₁ ] ) ≡ (λ x g₁ → A [ g o g₁ ] ) + ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → SetsAop [ y-map f ≈ y-map g ] + ≈-cong {a} {b} {f} {g} eq = let open ≈-Reasoning A in -- (λ x g₁ → A [ f o g₁ ] ) ≡ (λ x g₁ → A [ g o g₁ ] ) extensionality A ( λ h → ≈-≡ {_} {_} {_} {A} ( begin A [ f o h ] ≈⟨ resp refl-hom eq ⟩ A [ g o h ] ∎ ) ) - identity : {a : Obj A} → SetsAop A [ y-map A (id1 A a) ≈ id1 (SetsAop A) (y-obj A a ) ] - identity {a} = let open ≈-Reasoning (A) in -- (λ x g → A [ id1 A a o g ] ) ≡ (λ a₁ x → x) + identity : {a : Obj A} → SetsAop [ y-map (id1 A a) ≈ id1 SetsAop (y-obj a ) ] + identity {a} = let open ≈-Reasoning A in -- (λ x g → A [ id1 A a o g ] ) ≡ (λ a₁ x → x) extensionality A ( λ g → ≈-≡ {_} {_} {_} {A} ( begin A [ id1 A a o g ] ≈⟨ idL ⟩ g ∎ ) ) - distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → SetsAop A [ y-map A (A [ g o f ]) ≈ SetsAop A [ y-map A g o y-map A f ] ] - distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in -- (λ x g₁ → (A [ (A [ g o f] o g₁ ]))) ≡ (λ x x₁ → A [ g o A [ f o x₁ ] ] ) + distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → SetsAop [ y-map (A [ g o f ]) ≈ SetsAop [ y-map g o y-map f ] ] + distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning A in -- (λ x g₁ → (A [ (A [ g o f] o g₁ ]))) ≡ (λ x x₁ → A [ g o A [ f o x₁ ] ] ) extensionality A ( λ h → ≈-≡ {_} {_} {_} {A} ( begin A [ A [ g o f ] o h ] ≈↑⟨ assoc ⟩ @@ -208,35 +207,35 @@ -- x ∈ F(a) , (g : Hom A b a) → ( FMap F g ) x ------ -F2Natmap : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a : Obj A} → {F : Obj ( SetsAop A) } - → {x : FObj F a} → (b : Obj (Category.op A)) → Hom Sets (FObj (y-obj A a) b) (FObj F b) -F2Natmap A {a} {F} {x} b = λ ( g : Hom A b a ) → ( FMap F g ) x +F2Natmap : {a : Obj A} → {F : Obj SetsAop } + → {x : FObj F a} → (b : Obj (Category.op A)) → Hom Sets (FObj (y-obj a) b) (FObj F b) +F2Natmap {a} {F} {x} b = λ ( g : Hom A b a ) → ( FMap F g ) x -F2Nat : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a : Obj A} → {F : Obj (SetsAop A )} → FObj F a → Hom (SetsAop A) (y-obj A a) F -F2Nat {_} {c₂} A {a} {F} x = record { TMap = F2Natmap A {a} {F} {x} ; isNTrans = isNTrans1 } where +F2Nat : {a : Obj A} → {F : Obj SetsAop } → FObj F a → Hom SetsAop (y-obj a) F +F2Nat {a} {F} x = record { TMap = F2Natmap {a} {F} {x} ; isNTrans = isNTrans1 } where commute1 : {a₁ b : Obj (Category.op A)} {f : Hom (Category.op A) a₁ b} (g : Hom A a₁ a) → (Sets [ FMap F f o FMap F g ]) x ≡ FMap F (A [ g o f ] ) x commute1 g = let open ≈-Reasoning (Sets) in cong ( λ f → f x ) ( sym ( distr F ) ) commute : {a₁ b : Obj (Category.op A)} {f : Hom (Category.op A) a₁ b} → - Sets [ Sets [ FMap F f o F2Natmap A {a} {F} {x} a₁ ] ≈ Sets [ F2Natmap A {a} {F} {x} b o FMap (y-obj A a) f ] ] + Sets [ Sets [ FMap F f o F2Natmap {a} {F} {x} a₁ ] ≈ Sets [ F2Natmap {a} {F} {x} b o FMap (y-obj a) f ] ] commute {a₁} {b} {f} = let open ≈-Reasoning (Sets) in begin - Sets [ FMap F f o F2Natmap A {a} {F} {x} a₁ ] + Sets [ FMap F f o F2Natmap {a} {F} {x} a₁ ] ≈⟨⟩ Sets [ FMap F f o (λ ( g : Hom A a₁ a ) → ( FMap F g ) x) ] ≈⟨ extensionality A ( λ (g : Hom A a₁ a) → commute1 {a₁} {b} {f} g ) ⟩ - Sets [ (λ ( g : Hom A b a ) → ( FMap F g ) x) o FMap (y-obj A a) f ] + Sets [ (λ ( g : Hom A b a ) → ( FMap F g ) x) o FMap (y-obj a) f ] ≈⟨⟩ - Sets [ F2Natmap A {a} {F} {x} b o FMap (y-obj A a) f ] + Sets [ F2Natmap {a} {F} {x} b o FMap (y-obj a) f ] ∎ - isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) (y-obj A a) F (F2Natmap A {a} {F}) + isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) (y-obj a) F (F2Natmap {a} {F}) isNTrans1 = record { commute = λ {a₁ b f} → commute {a₁} {b} {f} } -- F(a) <- Nat(h_a,F) -Nat2F : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a : Obj A} → {F : Obj (SetsAop A) } → Hom (SetsAop A) (y-obj A a) F → FObj F a -Nat2F A {a} {F} ha = ( TMap ha a ) (id1 A a) +Nat2F : {a : Obj A} → {F : Obj SetsAop } → Hom SetsAop (y-obj a) F → FObj F a +Nat2F {a} {F} ha = ( TMap ha a ) (id1 A a) ---- -- @@ -244,9 +243,9 @@ -- ---- -F2Nat→Nat2F : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a : Obj A } → {F : Obj (SetsAop A)} → (fa : FObj F a) - → Nat2F A {a} {F} (F2Nat A {a} {F} fa) ≡ fa -F2Nat→Nat2F A {a} {F} fa = let open ≈-Reasoning (Sets) in cong ( λ f → f fa ) ( +F2Nat→Nat2F : {a : Obj A } → {F : Obj SetsAop } → (fa : FObj F a) + → Nat2F {a} {F} (F2Nat {a} {F} fa) ≡ fa +F2Nat→Nat2F {a} {F} fa = let open ≈-Reasoning (Sets) in cong ( λ f → f fa ) ( -- FMap F (Category.Category.Id A) fa ≡ fa begin ( FMap F (id1 A _ )) @@ -254,7 +253,7 @@ id1 Sets (FObj F a) ∎ ) -open import Relation.Binary.PropositionalEquality +-- open import Relation.Binary.PropositionalEquality ≡-cong = Relation.Binary.PropositionalEquality.cong @@ -262,18 +261,18 @@ -- ha : NTrans (op A) Sets (y-obj {a}) F -- FMap F g o TMap ha a ≈ TMap ha b o FMap (y-obj {a}) g -Nat2F→F2Nat : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a : Obj A } → {F : Obj (SetsAop A)} → (ha : Hom (SetsAop A) (y-obj A a) F) - → SetsAop A [ F2Nat A {a} {F} (Nat2F A {a} {F} ha) ≈ ha ] -Nat2F→F2Nat A {a} {F} ha {b} = let open ≡-Reasoning in +Nat2F→F2Nat : {a : Obj A } → {F : Obj SetsAop } → (ha : Hom SetsAop (y-obj a) F) + → SetsAop [ F2Nat {a} {F} (Nat2F {a} {F} ha) ≈ ha ] +Nat2F→F2Nat {a} {F} ha {b} = let open ≡-Reasoning in begin - TMap (F2Nat A {a} {F} (Nat2F A {a} {F} ha)) b + TMap (F2Nat {a} {F} (Nat2F {a} {F} ha)) b ≡⟨⟩ (λ g → FMap F g (TMap ha a (Category.Category.Id A))) ≡⟨ extensionality A (λ g → ( begin FMap F g (TMap ha a (Category.Category.Id A)) ≡⟨ ≡-cong (λ f → f (Category.Category.Id A)) (IsNTrans.commute (isNTrans ha)) ⟩ - TMap ha b (FMap (y-obj A a) g (Category.Category.Id A)) + TMap ha b (FMap (y-obj a) g (Category.Category.Id A)) ≡⟨⟩ TMap ha b ( (A Category.o Category.Category.Id A) g ) ≡⟨ ≡-cong ( TMap ha b ) ( ≈-≡ {_} {_} {_} {A} (IsCategory.identityL ( Category.isCategory A ))) ⟩ @@ -288,9 +287,31 @@ -- that is FMapp Yoneda is injective and surjective -- λ b g → (A Category.o f₁) g -YondaLemma1 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a a' : Obj A } {f : FObj (FObj (YonedaFunctor A) a) a' } - → SetsAop A [ F2Nat A {a'} {FObj (YonedaFunctor A) a} f ≈ FMap (YonedaFunctor A) f ] -YondaLemma1 A {a} {a'} {f} = refl +YondaLemma1 : {a a' : Obj A } {f : FObj (FObj YonedaFunctor a) a' } + → SetsAop [ F2Nat {a'} {FObj YonedaFunctor a} f ≈ FMap YonedaFunctor f ] +YondaLemma1 {a} {a'} {f} = refl + +open import Relation.Binary.HeterogeneousEquality hiding ([_]) +a1 : { c₁ : Level} {A B : Set c₁ } {a : A } { b : B } → a ≅ b → A ≡ B +a1 refl = refl + +domF : (y : Obj SetsAop) → {x : Obj (Category.op A)} → FObj y x → Obj A +domF y {x} z = x + +-- faithful (injective ) +Yoneda-injective : {a b : Obj A } → {x y : Obj SetsAop} → (g h : Hom SetsAop y (FObj YonedaFunctor a)) (f : Hom A a b ) + → SetsAop [ SetsAop [ FMap YonedaFunctor f o g ] ≈ SetsAop [ FMap YonedaFunctor f o h ] ] + → SetsAop [ g ≈ h ] +Yoneda-injective {a} {b} {x} {y} g h f yg=yh = extensionality A (λ z → ( begin + TMap g _ z ≡⟨ {!!} ⟩ + TMap g _ z ≡⟨ {!!} ⟩ + TMap h _ z ∎ )) where open ≡-Reasoning + +-- full (surjective) +Yoneda-surjective : {a b : Obj A } → {x y : Obj SetsAop} → (g h : Hom SetsAop (FObj YonedaFunctor b) y) (f : Hom A a b ) + → SetsAop [ SetsAop [ g o FMap YonedaFunctor f ] ≈ SetsAop [ h o FMap YonedaFunctor f ] ] + → SetsAop [ g ≈ h ] +Yoneda-surjective g h f gy=hy = {!!} -- F2Nat is bijection so FMap YonedaFunctor also ( using functional extensionality ) @@ -321,15 +342,11 @@ -- Instead we prove only -- inv ( FObj YonedaFunctor a ) ≡ a -inv : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a x : Obj A} ( f : FObj (FObj (YonedaFunctor A) a) x) → Obj A -inv A {a} f = Category.cod A f +inv : {a x : Obj A} ( f : FObj (FObj YonedaFunctor a) x) → Obj A +inv {a} f = Category.cod A f -YonedaLemma21 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a x : Obj A} ( f : ( FObj (FObj (YonedaFunctor A ) a) x) ) → inv A f ≡ a -YonedaLemma21 A {a} {x} f = refl - -open import Relation.Binary.HeterogeneousEquality -a1 : { c₁ : Level} {A B : Set c₁ } {a : A } { b : B } → a ≅ b → A ≡ B -a1 refl = refl +YonedaLemma21 : {a x : Obj A} ( f : ( FObj (FObj YonedaFunctor a) x) ) → inv f ≡ a +YonedaLemma21 {a} {x} f = refl -- YondaLemma3 : {c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → -- (a b x : Obj A ) → Hom A a x ≅ Hom A b x → a ≡ b