Mercurial > hg > Members > kono > Proof > category

changeset 621:19f31d22e790

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add desciptive lemma
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 22 Jun 2017 08:56:32 +0900
parents c95add5b7cbe
children bd890a43ef5b
files freyd2.agda
diffstat 1 files changed, 21 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/freyd2.agda	Tue Jun 20 22:44:09 2017 +0900
+++ b/freyd2.agda	Thu Jun 22 08:56:32 2017 +0900
@@ -194,28 +194,36 @@
 KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
       (a : Obj A )
       → HasInitialObject {c₁} {c₂} {ℓ}  ( K (Sets) A (FObj (Yoneda A a) a) ↓ (Yoneda A a) ) ( record  { obj = a ; hom = id1 Sets (FObj (Yoneda A a) a) } )
-KUhasInitialObj A a = record {
+KUhasInitialObj {c₁} {c₂} {ℓ} A a = record {
            initial =  λ b → initial0 b
          ; uniqueness =  λ b f → unique b f
      } where
+         commaCat : Category  (c₂ ⊔ c₁) c₂ ℓ
+         commaCat = K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a
+         initObj  : Obj (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a)
+         initObj = record { obj = a ; hom = id1 Sets (FObj (Yoneda A a) a) }
          hom1 : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) → 
                  Hom Sets (FObj (K Sets A (FObj (Yoneda A a) a)) (obj b)) (FObj (Yoneda A a) (obj b))
-         hom1 b = λ x → hom b x  
+         hom1 b = λ (x : Hom A a a ) → hom b x  
+         hom2 : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) → Hom A a a → Hom A a (obj b )
+         hom2 b x = hom b x  
+         comm1 : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) (x : FObj (Yoneda A a ) a )
+             → A [ ( Sets [ FMap (Yoneda A a) (id1 A (obj b) ) o hom b ] ) x ≈ hom b x ]
+         comm1 b x = let open ≈-Reasoning A in ≡-≈ ( cong ( λ k -> k x ) ( comm ( id1 (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a)) b ) ) )
+         --  hom b is  Hom A a a → Hom A a (obj b)
+         --  hom b is  Hom A a a → Hom A a (obj b)
+         --  hom b x is  ( x : Hom A a a ) → Hom A a (obj b)
+         --  hom b (id1 A a)  is  ( id1 A a : Hom A a a ) → Hom A a (obj b)
+         --  hom b (id1 A a) o x is  ( x : Hom A a a ) → Hom A a (obj b)
          initial0comm1 :  (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) → (x :  FObj (Yoneda A a) a )
             →  FMap (Yoneda A a) (hom b (id1 A a)) x ≡ hom b x
          initial0comm1 b x =  let open ≈-Reasoning A in ≈-≡ A ( begin
                FMap (Yoneda A a) (hom b (id1 A a)) x  
              ≈⟨⟩
                hom b (id1 A a ) o x
-             ≈↑⟨ cdr ( ≡-≈ ( cong (λ k → k x ) (IsFunctor.identity (isFunctor (Yoneda A a))))) ⟩
-               hom b (id1 A a ) o FMap (Yoneda A a) (id1 A a) x
              ≈⟨ {!!} ⟩
-               (Sets [ hom b o FMap (K Sets A (FObj (Yoneda A a) a)) (arrow (id1 (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) b)) ]) x
-             ≈↑⟨ ≡-≈ ( cong (λ k → k x) (comm (id1 ((K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) b ))) ⟩
-               (Sets [ FMap (Yoneda A a) (arrow (id1 (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) b)) o hom1 b ]) x
-             ≈⟨⟩
-               arrow  (id1 (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) b) o  hom b x
-             ≈⟨ idL ⟩
+               ( Sets [ FMap (Yoneda A a) (id1 A (obj b) ) o hom b ] ) x 
+             ≈⟨ comm1 b x ⟩
                hom b x
              ∎ )
          initial0comm :  (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) →
@@ -233,19 +241,18 @@
                    hom b o FMap (K Sets A (FObj (Yoneda A a) a)) (hom b (id1 A a)) 
              ∎ 
          initial0 : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) →
-            Hom ((K Sets A (FObj (Yoneda A a) a)) ↓ (Yoneda A a))
-              (record { obj = a ; hom = id1 Sets (FObj (Yoneda A a) a) }) b
+            Hom ((K Sets A (FObj (Yoneda A a) a)) ↓ (Yoneda A a)) initObj b
          initial0 b = record {
                 arrow = hom b (id1 A a) 
               ; comm = initial0comm b }
          -- what is comm f ?
          comm-f :  (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a)))
-            (f : Hom (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) (record { obj = a ; hom = id1 Sets (FObj (Yoneda A a) a) }) b)
+            (f : Hom (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) initObj b)
             → Sets [ Sets [ FMap  (Yoneda A a) (arrow f) o id1 Sets (FObj (Yoneda A a) a) ]
             ≈ Sets [ hom b  o  FMap  (K Sets A (FObj (Yoneda A a) a)) (arrow f) ]  ] 
          comm-f b f = comm f
          unique : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a))
-                (f : Hom (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) (record { obj = a ; hom = id1 Sets (FObj (Yoneda A a) a) }) b)
+                (f : Hom (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) initObj b)
                 → (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) [ f ≈ initial0 b ]
          unique b f = let open ≈-Reasoning A in begin
                 arrow f
@@ -261,7 +268,6 @@
             
 
 -- K{*}↓U has preinitial full subcategory then U is representable
---    K{*}↓U is complete, so it has initial object
 
 open SmallFullSubcategory
 open PreInitial