Mercurial > hg > Members > kono > Proof > category

changeset 693:984518c56e96

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 13 Nov 2017 12:39:30 +0900
parents 3ca3b5a4ab45
children 2043f7fd4273
files HomReasoning.agda SetsCompleteness.agda freyd.agda freyd2.agda pullback.agda yoneda.agda
diffstat 6 files changed, 47 insertions(+), 52 deletions(-) [+]
line wrap: on
line diff
--- a/HomReasoning.agda	Sun Nov 12 10:01:06 2017 +0900
+++ b/HomReasoning.agda	Mon Nov 13 12:39:30 2017 +0900
@@ -82,15 +82,16 @@
   idR1 :  { c₁ c₂ ℓ : Level}  (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b } →  A [ A [ f o Id {_} {_} {_} {A} a ] ≈ f  ]
   idR1 A =  IsCategory.identityR (Category.isCategory A)
 
--- How to prove this?
-  ≡-≈ : {a b : Obj A } { x y : Hom A a b } →  (x≈y : x ≡ y ) → x ≈ y
-  ≡-≈  refl = refl-hom
+  ≈←≡ : {a b : Obj A } { x y : Hom A a b } →  (x≈y : x ≡ y ) → x ≈ y
+  ≈←≡  refl = refl-hom
 
---  ≈-≡ : {a b : Obj A } { x y : Hom A a b } →  (x≈y : x ≈ y ) → x ≡ y
---  ≈-≡  x≈y = irr x≈y
+-- Ho← to prove this?
+--  ≡←≈ : {a b : Obj A } { x y : Hom A a b } →  (x≈y : x ≈ y ) → x ≡ y
+--  ≡←≈  x≈y = irr x≈y
+
   ≡-cong : { c₁′ c₂′ ℓ′ : Level}  {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A }  →
              (f : Hom B x y → Hom A x' y' ) →  a ≡ b  → f a  ≈  f b
-  ≡-cong f refl =  ≡-≈ refl
+  ≡-cong f refl =  ≈←≡ refl
 
 --  cong-≈ :  { c₁′ c₂′ ℓ′ : Level}  {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A }  → 
 --             B [ a ≈ b ] → (f : Hom B x y → Hom A x' y' ) →  f a ≈ f b
--- a/SetsCompleteness.agda	Sun Nov 12 10:01:06 2017 +0900
+++ b/SetsCompleteness.agda	Mon Nov 13 12:39:30 2017 +0900
@@ -152,7 +152,9 @@
    field
      hom→ : {i j : Obj C } →    Hom C i j →  I
      hom← : {i j : Obj C } →  ( f : I ) →  Hom C i j
-     hom-iso : {i j : Obj C } →  { f : Hom C i j } →   hom← ( hom→ f )  ≡ f
+     hom-iso : {i j : Obj C } →  { f : Hom C i j } →   C [ hom← ( hom→ f )  ≈ f ]
+     hom-rev : {i j : Obj C } →  { f : I } →   hom→ ( hom← {i} {j} f )  ≡ f
+     ≡←≈ : {i j : Obj C } →  { f g : Hom C i j } →  C [ f ≈ g ] →   f ≡ g
 
 open Small
 
@@ -203,7 +205,7 @@
         Sets [ (λ sn →  (snmap sn b)) o FMap (K C Sets (snat (ΓObj s Γ) (ΓMap s Γ))) f ] ]
     comm1 {a} {b} {f} = extensionality Sets  ( λ  sn  →  begin
                  FMap Γ f  (snmap sn  a )
-             ≡⟨ ≡cong ( λ f → ( FMap Γ f (snmap sn  a ))) (sym ( hom-iso s  )) ⟩
+             ≡⟨ ≡cong ( λ f → ( FMap Γ f (snmap sn  a ))) (sym ( ≡←≈ s ( hom-iso s ))) ⟩
                  FMap Γ ( hom← s ( hom→ s f))  (snmap sn  a )
              ≡⟨⟩
                  ΓMap s Γ (hom→ s f) (snmap sn a )
--- a/freyd.agda	Sun Nov 12 10:01:06 2017 +0900
+++ b/freyd.agda	Mon Nov 13 12:39:30 2017 +0900
@@ -9,17 +9,15 @@
 open Functor
 
 -- C is small full subcategory of A ( C is image of F )
+--    but we don't use smallness in this proof
 
-record SmallFullSubcategory {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
+record FullSubcategory {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
            : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
    field
-      SFSF : Functor A A  
-      SFSFMap← : { a b : Obj A } → Hom A (FObj SFSF a) (FObj SFSF b ) → Hom A a b 
-      full→ : { a b : Obj A } { x : Hom A (FObj SFSF a) (FObj SFSF b) } → A [ FMap SFSF ( SFSFMap← x ) ≈ x ]
-      full← : { a b : Obj A } { x : Hom A (FObj SFSF a) (FObj SFSF b) } → A [ SFSFMap← ( FMap SFSF x ) ≈ x ]
-
-      -- ≈→≡ : {a b : Obj A } →  { x y : Hom A (FObj SFSF a) (FObj SFSF b) } → 
-      --          (x≈y : A [ FMap SFSF x ≈ FMap SFSF y  ]) → FMap SFSF x ≡ FMap SFSF y   -- codomain of FMap is local small
+      FSF : Functor A A  
+      FSFMap← : { a b : Obj A } → Hom A (FObj FSF a) (FObj FSF b ) → Hom A a b 
+      full→ : { a b : Obj A } { x : Hom A (FObj FSF a) (FObj FSF b) } → A [ FMap FSF ( FSFMap← x ) ≈ x ]
+      full← : { a b : Obj A } { x : Hom A (FObj FSF a) (FObj FSF b) } → A [ FSFMap← ( FMap FSF x ) ≈ x ]
 
 -- pre-initial
 
@@ -36,12 +34,12 @@
 --       initial :  ∀( a : Obj A ) →  Hom A i a
 --       uniqueness  : { a : Obj A } →  ( f : Hom A i a ) → A [ f ≈  initial a ]
 
--- A complete catagory has initial object if it has PreInitial-SmallFullSubcategory
+-- A complete catagory has initial object if it has PreInitial-FullSubcategory
 
 open NTrans
 open Limit
 open IsLimit
-open SmallFullSubcategory
+open FullSubcategory
 open PreInitial
 open Complete
 open Equalizer
@@ -49,16 +47,16 @@
 
 initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
       (comp : Complete A A)
-      (SFS : SmallFullSubcategory A ) → 
-      (PI : PreInitial A  (SFSF SFS )) → IsInitialObject A (limit-c comp (SFSF SFS))
+      (SFS : FullSubcategory A ) → 
+      (PI : PreInitial A  (FSF SFS )) → IsInitialObject A (limit-c comp (FSF SFS))
 initialFromPreInitialFullSubcategory A comp SFS PI = record {
       initial = initialArrow ; 
       uniqueness  = λ {a} f → lemma1 a f
     } where
       F : Functor A A 
-      F = SFSF SFS   
+      F = FSF SFS   
       FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b 
-      FMap←  = SFSFMap←  SFS
+      FMap←  = FSFMap←  SFS
       a00 : Obj A
       a00 = limit-c comp F
       lim : ( Γ : Functor A A ) → Limit A A Γ 
--- a/freyd2.agda	Sun Nov 12 10:01:06 2017 +0900
+++ b/freyd2.agda	Mon Nov 13 12:39:30 2017 +0900
@@ -12,19 +12,20 @@
 
 ----------
 --
+-- A is locally small complete and K{*}↓U has preinitial full subcategory, U is an adjoint functor
+--
 --    a : Obj A
 --    U : A → Sets
 --    U ⋍ Hom (a,-)
 --
 
--- maybe this is a part of local smallness
-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 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
 
 import Relation.Binary.PropositionalEquality
 -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )
 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
 
-
 ----
 --
 --  Hom ( a, - ) is Object mapping in Yoneda Functor
@@ -48,10 +49,10 @@
         } 
     }  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-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
+        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 ] ]
@@ -59,7 +60,7 @@
                ( λ 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
+        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 ]
@@ -119,7 +120,7 @@
                  FMap Γ f o TMap t a₁ x
              ≈⟨⟩
                  ( ( FMap (Yoneda A b  ○ Γ ) f )  *  TMap t a₁ ) x
-             ≈⟨ ≡-≈ ( cong (λ k → k x ) (IsNTrans.commute (isNTrans t)) ) ⟩
+             ≈⟨ ≈←≡ ( cong (λ k → k x ) (IsNTrans.commute (isNTrans t)) ) ⟩
                  ( TMap t b₁ * ( FMap (K I Sets a) f ) ) x
              ≈⟨⟩
                  ( TMap t b₁ * id1 Sets a ) x
@@ -135,7 +136,7 @@
       ψ 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 
+      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
              ≈⟨⟩
                 FMap (Yoneda A b) ( TMap (t0 lim) i) (FMap (Yoneda A b) (limit (isLimit lim) b (ta a x t )) (id1 A b ))
@@ -151,7 +152,7 @@
       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 ]) →
         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 A in extensionality A ( λ x →  ≡←≈ A ( begin 
                   ψ a t x
              ≈⟨⟩
                  FMap (Yoneda A b) (limit (isLimit lim) b (ta a x t )) (id1 A b )
@@ -159,7 +160,7 @@
                  limit (isLimit lim) b (ta a x t ) o id1 A b 
              ≈⟨ idR ⟩
                  limit (isLimit lim) b (ta a x t ) 
-             ≈⟨ limit-uniqueness (isLimit lim) ( λ {i} → ≡-≈ ( cong ( λ g → g x )( t0f=t {i} ))) ⟩
+             ≈⟨ limit-uniqueness (isLimit lim) ( λ {i} → ≈←≡ ( cong ( λ g → g x )( t0f=t {i} ))) ⟩
                   f x
              ∎  ))
 
@@ -191,7 +192,7 @@
          initObj  : Obj (K A Sets * ↓ Yoneda 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
+         comm2 b OneObj = let open ≈-Reasoning A in  ≡←≈ A ( begin
                 ( Sets [ FMap (Yoneda A a) (hom b OneObj) o (λ x₁ → id1 A a) ] ) OneObj
              ≈⟨⟩
                 FMap (Yoneda A a) (hom b OneObj) (id1 A a)
@@ -228,7 +229,7 @@
                 ( Sets [ FMap  (Yoneda A a) (arrow f) o id1 Sets (FObj (Yoneda A a) a)  ] ) (id1 A a)
              ≈⟨⟩
                ( Sets [ FMap  (Yoneda A a) (arrow f) o ( λ x → id1 A a ) ] ) OneObj
-             ≈⟨ ≡-≈ ( cong (λ k → k OneObj ) (comm f )) ⟩
+             ≈⟨ ≈←≡ ( cong (λ k → k OneObj ) (comm f )) ⟩
                ( Sets [ hom b  o  FMap  (K A Sets *) (arrow f) ]  ) OneObj
              ≈⟨⟩
                 hom b OneObj
@@ -294,7 +295,7 @@
                  A [ f o arrow (initial In (ob A 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)] ) ) ⟩
+             ≡⟨  ≡←≈ 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) ))
              ≡⟨⟩
                 (Sets [ ( λ x → arrow (initial In (ob A U b x))) o FMap U f ] ) y
@@ -342,7 +343,7 @@
          → ( 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 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} = let open ≈-Reasoning A in extensionality Sets ( λ ( y : Hom A (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 ) ))) 
@@ -397,7 +398,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 
--- a/pullback.agda	Sun Nov 12 10:01:06 2017 +0900
+++ b/pullback.agda	Mon Nov 13 12:39:30 2017 +0900
@@ -240,8 +240,7 @@
        U = λ b → a0 ( lim b) ;
        ε = λ b → t0 (lim b) ;
        _*' = λ {b} {a} k → limit (isLimit (lim b )) a k ; 
-       iscoUniversalMapping = record {
-           couniversalMapping = λ{ b a f} → couniversalMapping1 {b} {a} {f} ;
+       iscoUniversalMapping = record { couniversalMapping = λ{ b a f} → couniversalMapping1 {b} {a} {f} ;
            couniquness = couniquness2
        }
   } where
@@ -263,8 +262,6 @@
             g
         ∎
 
-open import Category.Cat
-
 univ2limit :
      ( univ :   coUniversalMapping A (A ^ I) (KI I) ) →
      ( Γ : Functor I A ) →   Limit I A Γ 
--- a/yoneda.agda	Sun Nov 12 10:01:06 2017 +0900
+++ b/yoneda.agda	Mon Nov 13 12:39:30 2017 +0900
@@ -311,16 +311,12 @@
 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
+open import  Relation.Binary.HeterogeneousEquality
 -- 
--- a1 : { c₁ : Level} {A B : Set c₁ } {a : A } { b : B } → a ≅ b → A ≡ B 
--- a1 refl = refl
+a1 : { c₁ : Level} {A B : Set c₁ } {a : A } { b : B } → a ≅ b → A ≡ B 
+a1 refl = refl
 -- 
--- YonedaInjective :   { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a b : Obj A}
---     → FObj (YonedaFunctor A ) a ≡ FObj (YonedaFunctor A ) b 
---     → a ≡ b
--- YonedaInjective A {a} {b} eq = y1 ( ≡-cong ( λ k → FObj k a) eq ) 
---   where
---     y1 : Hom A a a ≡ Hom A a b  → a ≡ b
---     y1 eq = {!!}
-
+-- YonedaInjective :   { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a b x : Obj A}
+--      → FObj (FObj (YonedaFunctor A ) a ) x ≡ FObj (FObj (YonedaFunctor A ) b ) x
+--      → a ≡ b
+-- YonedaInjective A eq =  ≡-cong ( λ y → inv A y ) eq