Mercurial > hg > Members > kono > Proof > category

changeset 1100:56c88ca85d07

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 Sun, 30 Jan 2022 20:40:19 +0900
parents 321f0fef54c2
children f485f725b2d3
files src/Polynominal.agda src/ToposIL.agda src/freyd2.agda src/yoneda.agda
diffstat 4 files changed, 41 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/src/Polynominal.agda	Sat Jul 31 06:58:48 2021 +0900
+++ b/src/Polynominal.agda	Sun Jan 30 20:40:19 2022 +0900
@@ -34,7 +34,12 @@
   -- from page. 51
   --
 
+  open Functor
   open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+  open import Relation.Binary.PropositionalEquality hiding ( [_] ; resp ) renaming ( sym to ≡sym )
+
+  data _H≈_ {a b c d : Obj A } ( x : Hom A a b ) (y : Hom A c d ) : Set ( c₁  ⊔  c₂ ⊔ ℓ) where
+     feq : a ≡ c → b ≡ d → (z : Hom A a b) → z ≅ y → A [ x ≈ z ] → x H≈ y
 
   data  φ  {a ⊤ : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁  ⊔  c₂ ⊔ ℓ) where
      i   : {b c : Obj A} (k : Hom A b c ) →  φ x k   
@@ -76,11 +81,33 @@
   -- an assuption needed in k x phi ≈ k x phi'
   --   k x (i x) ≈ k x ii  
   postulate 
-       xf :  {a b c : Obj A } → ( x : Hom A １ a ) → {z : Hom A b c } → ( y  : φ {a} x z ) → ( x ∙ π' ) ≈ π 
+       xf :  {a b c : Obj A } → ( x : Hom A １ a ) → {f : Hom A b c } → ( fp  : φ {a} x f ) →  A [ k x (i f) ≈ k x fp ]
+       -- ( x ∙ π' ) ≈ π 
   --   
   --   this is justified equality f ≈ g in A[x] is used in f ∙ < x , id1 A _> ≈  f ∙ < x , id1 A _>
   --   ( x ∙ π' ) ∙ < x , id1 A _ > ≈ π ∙ < x , id1 A _ >
 
+
+  --
+  -- Subcategory of A without x
+  --
+  -- Since A is CCC, ∀ f : Hom A b c ,  φ x {b} {c} (FMap F f) is an arrow of CCC A.
+  --
+
+  --
+  -- If no x in SA (Subcategory of CCC A), we may have xf.
+  --
+  record SA  {a ⊤ : Obj A } ( x : Hom A ⊤ a ) : Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ) where
+     field
+       F : Functor A A
+       CF : CCCFunctor A A C C F
+       FObj-iso : (x : Obj A) → FObj F x ≡ x
+       without-x : {b c : Obj A} → (f : Hom A b c) → ¬ ( FMap F f H≈ x  )
+
+  xf-in-SA : {a ⊤ : Obj A } ( x : Hom A ⊤ a ) → (sa : SA x) → 
+       {b c : Obj A } → {f : Hom A b c } → ( fp  : φ {a} x (FMap (SA.F sa) f) ) →  Set ℓ
+  xf-in-SA {a} {⊤} x sa {b} {c} {f} fp = A [ k x (i (FMap (SA.F sa) f)) ≈ k x fp ]
+
   -- since we have A[x] now, we can proceed the proof on p.64 in some possible future
 
   --
@@ -144,6 +171,7 @@
                ( (f ∙ π')  ∙  < π ∙ π , < π' ∙  π , π' > > ) *  ≈⟨ *-cong ( car ( ki x _ fp )) ⟩
                ( k x fp ∙  < π ∙ π , < π' ∙  π , π' > > ) *  ≈⟨⟩
                k x (v fp )  ∎  
+
   k-cong : {a b c : Obj A}  → (f g :  Poly a c b )
         → A [ Poly.f f ≈ Poly.f g ] → A [ k (Poly.x f) (Poly.phi f)   ≈ k (Poly.x g) (Poly.phi g) ]
   k-cong {a} {b} {c} f g f=f = begin
--- a/src/ToposIL.agda	Sat Jul 31 06:58:48 2021 +0900
+++ b/src/ToposIL.agda	Sun Jan 30 20:40:19 2022 +0900
@@ -153,7 +153,7 @@
         tt :  (q : Poly a  (Topos.Ω t) b ) → A [ char t (equalizer (Ker t (Poly.f q))) (eMonic A (Ker t (Poly.f q)))  ≈  Poly.f q ]
         tt q = IsTopos.char-uniqueness (Topos.isTopos t) {b} {a} 
 
-  module IL1 (Ω : Obj A) (⊤ : Hom A １ Ω) (P  : Obj A → Obj A) (il : InternalLanguage  Ω ⊤ P) (t : Topos A c) where
+  module IL1 (Ω : Obj A) (⊤ : Hom A １ Ω) (P  : Obj A → Obj A) (il : InternalLanguage  Ω ⊤ P)  where
      open InternalLanguage il
      il00 : {a : Obj A}  (p : Poly a  Ω １ )  → p  ⊢ p
      il00 {a}  p h eq = eq
--- a/src/freyd2.agda	Sat Jul 31 06:58:48 2021 +0900
+++ b/src/freyd2.agda	Sun Jan 30 20:40:19 2022 +0900
@@ -19,7 +19,7 @@
 --    U ⋍ Hom (a,-)
 --
 
-open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym )
+open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym ; resp )
 
 -- A is localy 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
--- a/src/yoneda.agda	Sat Jul 31 06:58:48 2021 +0900
+++ b/src/yoneda.agda	Sun Jan 30 20:40:19 2022 +0900
@@ -349,9 +349,7 @@
      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
+     h ∎ where open ≈-Reasoning Sets
      -- sj : B [ FMap F ( CatSurjective.sur s (FMap F (f g h))) ≈ FMap F (f g h) ]
      -- sj  = CatSurjective.surjective s (FMap F (f g h)) 
 
@@ -376,10 +374,7 @@
          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
-             s : CatSurjective A SetsAop YonedaFunctor 
-             s = Yoneda-surjective 
+         ∎ where open ≈-Reasoning Sets
 
 --- How to prove it? from smallness?
 
@@ -395,16 +390,18 @@
 
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
+--
+-- if Hom A a a ≡ Hom A a b, b must be a cod of id1 A a, so a ≡ b
+--
 postulate  -- ?
      ylem0 : {a b : Obj A } → Hom A a a ≡ Hom A a b → a ≡ b
 
+-- Obj : Set c₂
+-- Hom : Obj → Obj → Set c₂
+-- cod : {A B : Obj} → Hom A B → Obj
+-- cod {a} {b} _ = b
+
 Yoneda-full-embed : {a b : Obj A } → FObj YonedaFunctor a ≡ FObj YonedaFunctor b → a ≡ b
 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
-     f : Hom A a b
-     f = subst (λ k → k ) ylem1 (id1 A a)
-     -- f1 : id1 A a ≅ f
-     -- f1 = {!!}
-     -- f2 : id1 A a ≅ f → Category.cod A (id1 A a) ≡  Category.cod A f
-     -- f2 = {!!}