Mercurial > hg > Members > kono > Proof > category

changeset 1005:fd2d54dd2197

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 10 Mar 2021 09:06:57 +0900
parents e79cb6080c79
children 444d2aba55eb
files src/yoneda.agda
diffstat 1 files changed, 48 insertions(+), 29 deletions(-) [+]
line wrap: on
line diff
--- a/src/yoneda.agda	Tue Mar 09 14:51:17 2021 +0900
+++ b/src/yoneda.agda	Wed Mar 10 09:06:57 2021 +0900
@@ -335,7 +335,6 @@
      ... | eq = ≈-Reasoning.≈←≡ A ( cong (λ k →  k (id1 A b)) eq )
      open ≈-Reasoning A
 
--- ≈←≡ (cong (λ k → Nat2F {b} {y-obj x} k) ( ≈-≡ SetsAop yg=yh))  ⟩ 
 -- full (surjective)
 
 record CatSurjective { c₁ c₂ ℓ c₁' c₂' ℓ' : Level} ( A : Category c₁ c₂ ℓ ) ( B : Category c₁' c₂' ℓ' ) (F : Functor A B)
@@ -346,26 +345,33 @@
 
 open CatSurjective
 
-CatEpiR : {c : Level } (F : Functor (Sets {c}) (Sets {c}))
-    → {a a' : Obj Sets } {b : Obj Sets} (g h : Hom Sets (FObj F a') b) 
-    → ( f : Hom Sets a a' )
-    → (Sets [ Sets [ g o FMap F f ] ≈  Sets [ h o FMap F f ] ] → Sets [ g  ≈ h ])
-    → CatSurjective Sets Sets F 
-CatEpiR  F g h f eq = record { sur = λ g → {!!}  ;  surjective = {!!} } where
-    ylem22 :  {a a' : Obj Sets} (i : Hom Sets (FObj F a) (FObj F a')) → Sets [ FMap F {!!} ≈ i ]
-    ylem22 i = begin
-     FMap F {!!} ≈⟨ {!!} ⟩
-     i ∎ 
-     where
-       open ≈-Reasoning Sets
+-- CatEpiR : {c : Level } (F : Functor (Sets {c}) (Sets {c}))
+--     → {a a' : Obj Sets } {b : Obj Sets} (g h : Hom Sets (FObj F a') b) 
+--     → ( ( f : {a a' b : Obj Sets} (g : Hom Sets (FObj F a) b) → Hom Sets a a' )
+--         → (Sets [ Sets [ g o FMap F (f  g) ] ≈  Sets [ h o FMap F (f h) ] ] → Sets [ g  ≈ h ]) )
+--     → CatSurjective Sets Sets F 
+-- CatEpiR  F g h eq = record { sur = λ {a} {a'} g →  sur0 {a} {a'} g ;  surjective = ylem22 } where
+--     sur0 : {a a' : Obj Sets} (g : Hom Sets (FObj F a) (FObj F a')) → Hom Sets a a'
+--     sur0 {a} {a'} g = {!!}
+--     ylem22 :  {a a' : Obj Sets} (g : Hom Sets (FObj F a) (FObj F a')) → Sets [ FMap F (sur0 g) ≈ g ]
+--     ylem22 g = begin
+--      FMap F (sur0 g) ≈⟨ {!!} ⟩
+--      Sets [  FMap F {!!} o FMap F {!!} ]  ≈⟨ {!!} ⟩
+--      Sets [ g o Sets [  FMap F {!!} o FMap F {!!} ] ] ≈⟨ {!!} ⟩
+--      g ∎ 
+--      where
+--        open ≈-Reasoning Sets
 
 CatEpi : {c : Level} (F : Functor (Sets {c}) (Sets {c}))
     → (s : CatSurjective Sets Sets F  )
     → {a a' : Obj Sets } {b : Obj Sets} (g h : Hom Sets (FObj F a') b)
-    → (f : {a a' : Obj Sets } {b : Obj Sets} (g h : Hom Sets (FObj F a') b) → Hom Sets a a' )
-    → Sets [ Sets [ g o FMap F (f {a} {a'} g h ) ] ≈  Sets [ h o FMap F (f g h )] ] → Sets [ g  ≈ h ]
-CatEpi F s g h f eq = begin
-     g ≈⟨ {!!} ⟩
+    → Sets [ Sets [ g o FMap F ( sur s (id1 Sets _)) ] ≈  Sets [ h o FMap F ( sur s (id1 Sets _)) ] ]  → Sets [ g  ≈ h ]
+CatEpi F s g h  eq = begin
+     g ≈↑⟨ idR ⟩
+     Sets [ g o id1  Sets _ ]  ≈↑⟨ cdr (surjective s (id1 Sets _) ) ⟩
+     Sets [ g o  FMap F (sur s (id1 Sets _)) ]  ≈⟨ eq ⟩
+     Sets [ h o  FMap F (sur s (id1 Sets _)) ]  ≈⟨ cdr (surjective s (id1 Sets _) ) ⟩
+     Sets [ h o id1  Sets _ ]  ≈⟨ idR ⟩
      h ∎ 
   where
      open ≈-Reasoning Sets
@@ -382,12 +388,16 @@
      f : {a a' : Obj A } → (g : Hom SetsAop (FObj YonedaFunctor a) (FObj YonedaFunctor a')) → Hom A a a'
      f g = Nat2F g
 
--- epi
-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 ] ]
+Yoneda-epi : { b : Obj A } {x y : Obj SetsAop} → (g h : Hom SetsAop (FObj YonedaFunctor b) y)
+    → ( {a : Obj A } (f : Hom A a b ) → SetsAop [ SetsAop [ g o FMap YonedaFunctor f ] ≈ SetsAop [ h o FMap YonedaFunctor f ] ] )
     → SetsAop [  g ≈ h ]
-Yoneda-surjective' {a} {b} {x} {y} g h f yg=yh = begin
-         TMap g _ ≈⟨ {!!} ⟩
+Yoneda-epi {b} {x} {y} g h yg=yh = begin
+         TMap g _ ≈↑⟨ idR ⟩
+         Sets [ TMap g _  o id1  Sets _ ] ≈↑⟨  cdr (surjective Yoneda-surjective (id1 SetsAop _)) ⟩
+         Sets [ TMap g _  o (λ z → A [ sur Yoneda-surjective (id1 SetsAop _) o z ] ) ]   ≈⟨⟩
+         (λ z → TMap g _ (A [ id1 A _  o z ] ))   ≈⟨ yg=yh (id1 A b) ⟩
+         Sets [ TMap h _  o (λ z → A [ sur Yoneda-surjective (id1 SetsAop _) o z ] ) ] ≈⟨  cdr (surjective Yoneda-surjective (id1 SetsAop _)) ⟩
+         Sets [ TMap h _  o id1  Sets _ ] ≈⟨ idR ⟩
          TMap h _
          ∎ where
              open ≈-Reasoning Sets
@@ -395,16 +405,25 @@
              s = Yoneda-surjective 
 
 
-postulate
-        eqObj1 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a a' b b' : Obj A}  → Hom A a b ≡ Hom A a' b' → b ≡ b'
+data [_]_~_ {c₁ c₂ ℓ} (C : Category c₁ c₂ ℓ) {A B : Obj C} (f : Hom C A B)
+     : ∀{X Y : Obj C} → Hom C X Y → Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
+  refl : {g : Hom C A B} → (eqv : C [ f ≈ g ]) → [ C ] f ~ g
+
+≃→a=a : {c₁ ℓ : Level}  (B : Category c₁ c₁ ℓ ) → {a b a' b' : Obj B }
+     → ( f : Hom B a b )
+     → ( g : Hom B a' b' )
+     → [_]_~_ B f g → a ≡ a'
+≃→a=a B f g (refl eqv) = refl
+
+a2 : {a : Obj A } → [ A ] id1 A a ~ id1 A a
+a2 = refl (≈-Reasoning.refl-hom A)
+
+postule
+   eqObj1 : {a b a' b' : Obj A } → Hom A a b ≡ Hom A a' b' → b ≡ b'
+--  eqObj1 = ≃→a=a A ? ? a2    close but ...
 
 open import  Relation.Binary.HeterogeneousEquality as HE using (_≅_) 
 
--- eqObj2 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a b : Obj A}  → Hom A a a ≡ Hom A a b → a ≡ b
--- eqObj2 A {a} {b}  eq = eqObj3  eq refl where
---      eqObj3 : {a  b : Obj A} {f : Hom A a a } {g : Hom A b b } → a ≡ b → id1 A a ≅ id1 A b 
---      eqObj3 refl = HE.refl
-
 a1 : { c₁ : Level} {A B : Set c₁ } {a : A } { b : B } → a ≅ b → A ≡ B 
 a1 HE.refl = refl