Mercurial > hg > Members > kono > Proof > category

changeset 954:6aa6cbf630a0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix Burroni
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 21 Feb 2021 03:34:36 +0900
parents eb62812b5885
children 5c8694236ff3
files src/CCC.agda src/CatExponetial.agda src/equalizer.agda
diffstat 3 files changed, 104 insertions(+), 55 deletions(-) [+]
line wrap: on
line diff
--- a/src/CCC.agda	Fri Feb 19 12:09:48 2021 +0900
+++ b/src/CCC.agda	Sun Feb 21 03:34:36 2021 +0900
@@ -125,8 +125,17 @@
 ----
 --
 -- Sub Object Classifier as Topos
+-- pull back on
+--                   ○ b
+--       b ----------------------→ 1
+--       |                         |
+--       |                         |
+--     m |                         | ⊤
+--       |                         |
+--       ↓                         ↓
+--       a ----------------------→ Ω
+--                    h
 --
-
 open Equalizer
 
 record Mono  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {b a : Obj A} (mono : Hom A b a) : Set  (c₁ ⊔ c₂ ⊔ ℓ)  where
@@ -143,9 +152,9 @@
         (Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (○ a) ]))
         (char : {a b : Obj A} → (m :  Hom A b a) → Mono A m  → Hom A a Ω) :  Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
      field
-         char-ker-id  : {a b : Obj A } {h : Hom A a Ω} → (m :  Hom A b a) → (mono : Mono A m)
+         char-ker  : {a b : Obj A } {h : Hom A a Ω} 
              → A [ char (equalizer (Ker h)) record { isMono = monic (Ker h) } ≈ h ]
-         ker-char-iso : {a b : Obj A} →  (m :  Hom A b a) → (mono : Mono A m)  → Iso A b (  equalizer-c (Ker ( char m mono ))) 
+         ker-char : {a b : Obj A} →  (m :  Hom A b a) → (mono : Mono A m)  → Iso A b (  equalizer-c (Ker ( char m mono ))) 
 
 record Topos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  ( １ : Obj A) (○ : (a : Obj A ) → Hom A a １) :  Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
      field
--- a/src/CatExponetial.agda	Fri Feb 19 12:09:48 2021 +0900
+++ b/src/CatExponetial.agda	Sun Feb 21 03:34:36 2021 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --allow-unsolved-metas #-} 
+
 ----
 --
 --  B^A
@@ -12,7 +14,9 @@
 
 open import HomReasoning
 open import cat-utility
-
+-- open import Relation.Binary  hiding (_⇔_)
+-- open import Relation.Binary.Core hiding (_⇔_)
+-- open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 
 -- Object is a Functor : A → B 
 -- Hom is a natural transformation
@@ -70,20 +74,16 @@
 open import Relation.Binary.Core  
 isB^A :  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ' ) → IsCategory (CObj A B) (CHom A B) _==_ _+_ (Cid A B)
 isB^A  {c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} A B =
-  record  { isEquivalence =  record {refl = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory B )); 
-                  sym = λ {i j} → sym1 {_} {_} {i} {j} ;
-                  trans = λ {i j k} → trans1 {_} {_} {i} {j} {k} }  
+  record  { isEquivalence =  record {refl = ≈-Reasoning.refl-hom B  
+              ;   sym = λ {i j} → sym1 {_} {_} {i} {j} 
+              ;   trans = λ {i j k} → trans1 {_} {_} {i} {j} {k} }  
         ; identityL = IsCategory.identityL ( Category.isCategory B )
         ; identityR = IsCategory.identityR ( Category.isCategory B )
         ; o-resp-≈ =  λ{a b c f g h i } → o-resp-≈1      {a} {b} {c} {f} {g} {h} {i}
         ; associative = IsCategory.associative ( Category.isCategory B )
         } where
             sym1 : {a b : CObj A B } {i j : CHom A B a b } → i == j → j == i
-            sym1 {a} {b} {i} {j} eq {x} = let open ≈-Reasoning B in begin
-                 TMap j x
-             ≈⟨ sym eq ⟩
-                 TMap i x
-             ∎ 
+            sym1 {a} {b} {i} {j} eq {x} = ≈-Reasoning.sym B eq 
             trans1 : {a b : CObj A B } {i j k : CHom A B a b} → i == j → j == k → i == k
             trans1 {a} {b} {i} {j} {k} i=j j=k {x} =  let open ≈-Reasoning B in begin
                  TMap i x
--- a/src/equalizer.agda	Fri Feb 19 12:09:48 2021 +0900
+++ b/src/equalizer.agda	Sun Feb 21 03:34:36 2021 +0900
@@ -1,4 +1,3 @@
-{-# OPTIONS --allow-unsolved-metas #-} 
 ---
 --
 --  Equalizer
@@ -21,18 +20,6 @@
 open import HomReasoning
 open import cat-utility
 
--- in cat-utility
--- record Equalizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {c a b : Obj A} (e : Hom A c a) (f g : Hom A a b)  : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
---    field
---       fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ]
---       k : {d : Obj A}  (h : Hom A d a) → A [ A [ f  o  h ] ≈ A [ g  o h ] ] → Hom A d c
---       ek=h : {d : Obj A}  → ∀ {h : Hom A d a} →  {eq : A [ A [ f  o  h ] ≈ A [ g  o h ] ] } →  A [ A [ e  o k {d} h eq ] ≈ h ]
---       uniqueness : {d : Obj A} →  ∀ {h : Hom A d a} →  {eq : A [ A [ f  o  h ] ≈ A [ g  o h ] ] } →  {k' : Hom A d c } →
---               A [ A [ e  o k' ] ≈ h ] → A [ k {d} h eq  ≈ k' ]
---    equalizer : Hom A c a
---    equalizer = e
-
-
 --
 -- Burroni's Flat Equational Definition of Equalizer
 --
@@ -56,6 +43,20 @@
    β : { d a b : Obj A}  → (f : Hom A a b) → (g : Hom A a b ) →  (h : Hom A d a ) → Hom A d c
    β {d} {a} {b} f g h =  A [ γ {a} {b} {c} f g h o δ {d} {b} {d} (id1 A d) (A [ f o h ]) ]
 
+record Burroni' { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A} (f g : Hom A a b) : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
+   field
+      equ : {a b : Obj A } → (f g : Hom A a b) →  Obj A
+      α : {a b : Obj A } → (f g : Hom A a b) →  Hom A (equ f g)  a
+      γ : {a b d : Obj A } → (f g : Hom A a b) → (h : Hom A d a ) →  Hom A (equ (A [ f o h ]) (A [ g o h ]))  (equ f g)
+      δ : {a b : Obj A } → (f g : Hom A a b) → A [ f ≈ g ] → Hom A a (equ f g)
+      b1 : A [ A [ f  o α f g ] ≈ A [ g  o α f g ] ]
+   b1k :  {d : Obj A } {k : Hom A d (equ f g)} →  A [ A [ f o A [ α f g o k ] ] ≈ A [ g o A [ α f g o k ] ] ]
+   b1k {d} {k} = ≈-Reasoning.trans-hom A (≈-Reasoning.assoc A) (≈-Reasoning.trans-hom A (≈-Reasoning.car A b1) (≈-Reasoning.sym A (≈-Reasoning.assoc A)))
+   field
+      b2 :  {d : Obj A } → {h : Hom A d a } → A [ A [ ( α f g ) o (γ f g h) ] ≈ A [ h  o α (A [ f o h ]) (A [ g o h ]) ] ]
+      b3 : {d : Obj A} → {h : Hom A d a } → A [ A [ α f f o δ f f (≈-Reasoning.refl-hom A) ] ≈ id1 A a ]
+      b4 :  {d : Obj A } {h : Hom A d a } {k : Hom A d (equ f g)} →
+           A [ A [ γ f g ( A [ α f g o k ] ) o ( δ (A [ f o A [ α f g o  k ] ] ) (A [ g o A [ α f g o  k ] ] ) b1k )] ≈ k ]
 
 open Equalizer
 open IsEqualizer
@@ -98,10 +99,10 @@
 --        ||
 --         d
 
-monic : { a b d : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A f g) 
-      →  ( i j : Hom A d (equalizer-c eqa) )
+monoic : { c a b d : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A f g) 
+      →  { i j : Hom A d (equalizer-c eqa) }
       →  A [ A [ equalizer eqa o i ]  ≈  A [ equalizer eqa o j ] ] →  A [ i  ≈ j  ]
-monic  {a} {b} {d} {f} {g} eqa i j ei=ej = let open ≈-Reasoning (A) in begin
+monoic {c} {a} {b} {d} {f} {g} eqa {i} {j} ei=ej = let open ≈-Reasoning (A) in begin
                  i
               ≈↑⟨ uniqueness (isEqualizer eqa) ( begin
                    equalizer eqa  o i
@@ -238,6 +239,22 @@
 
 -- c-iso-rl is obvious from the symmetry
 
+--
+-- we cannot have equalizer ≈ id. we only have Iso A (equalizer-c equ) a
+--
+equ-ff : {a b : Obj A} → (f : Hom A a b ) → IsEqualizer A (id1 A a) f f
+equ-ff {a} {b} f = record {
+      fe=ge = ≈-Reasoning.refl-hom A ;  
+      k = λ {d} h eq → h ;
+      ek=h = λ {d} {h} {eq} → ≈-Reasoning.idL A ;
+      uniqueness  = λ {d} {h} {eq} {k'} ek=h → begin
+            h
+         ≈↑⟨ ek=h ⟩
+            id1 A a o k'
+         ≈⟨ idL ⟩
+            k'
+         ∎ 
+   } where open  ≈-Reasoning A
 
 
 --------------------------------
@@ -247,25 +264,26 @@
 --
 ----
 
-lemma-equ1 : {a b c : Obj A} (f g : Hom A a b)  → (e : Hom A c a ) →
-         ( eqa-e : {a b c : Obj A} → (f g : Hom A a b)  → Hom A c a )
-         ( eqa : {a b c : Obj A} → (f g : Hom A a b)  → IsEqualizer A (eqa-e f g) f g ) 
-              → Burroni A {c} {a} {b} f g e
-lemma-equ1  {a} {b} {c} f g e eqa-e eqa  = record {
-      α = λ {a} {b} {c}  f g e  →  equalizer1 (eqa {a} {b} {c} f g ) ; -- Hom A c a -- eqa-e f g
-      γ = λ {a} {b} {c} {d} f g h → k (eqa {a} {b} {c} f g  ) {d} ( A [ h  o (equalizer1 ( eqa (A [ f  o  h ] ) (A [ g o h ] ))) ] ) 
+lemma-equ1 : {a b c : Obj A} (f g : Hom A a b)
+      → ( eqa-e : {a b c : Obj A} → (f g : Hom A a b)  → Hom A c a )
+      → ( eqa : {a b c : Obj A} → (f g : Hom A a b)  → IsEqualizer A (eqa-e f g) f g ) 
+              → Burroni A {c} {a} {b} f g (eqa-e f g)
+lemma-equ1  {a} {b} {c} f g eqa-e eqa  = record {
+      α = λ {a} {b} {c}  f g e  →  equalizer1 (eqa {a} {b} {c} f g  ) ; -- Hom A c a
+      γ = λ {a} {b} {c} {d} f g h → k (eqa {a} {b} {c} f g ) {d} ( A [ h  o (equalizer1 ( eqa (A [ f  o  h ] ) (A [ g o h ] ))) ] ) 
                             (lemma-equ4 {a} {b} {c} {d} f g h ) ;  -- Hom A c d
-      δ =  λ {a} {b} {c} e f → k (eqa {a} {b} {c} f f  ) {a} (id1 A a)  (f1=f1 f); -- Hom A a c
+      δ =  λ {a} {b} {c} e f → k (eqa {a} {b} {c} f f ) {a} (id1 A a)  (f1=f1 f); -- Hom A a c
       cong-α = λ {a b c e f g g'} eq → cong-α1 {a} {b} {c} {e} {f} {g} {g'} eq ;
       cong-γ = λ {a} {_} {c} {d} {f} {g} {h} {h'} eq → cong-γ1 {a}  {c} {d} {f} {g} {h} {h'} eq  ;
-      cong-δ = λ {a b c e f f'} f=f' → cong-δ1 {a} {b} {c} {e} {f} {f'} f=f'  ;
+      cong-δ = λ {a b c e f f'} f=f' → cong-δ1 {a} {b} {c}  {f} {f'} f=f'  ;
       b1 = fe=ge (eqa {a} {b} {c} f g ) ;
       b2 = λ {d} {h} → lemma-b2 {d} {h};
       b3 = lemma-b3 ;
       b4 = lemma-b4 
  } where
      --
-     --           e eqa f g        f --         c ---------→ a ------→b
+     --           e eqa f g        f
+     --         c ---------→ a ------→b
      --         ^                  g
      --         |
      --         |k₁  = e eqa (f o (e (eqa f g))) (g o (e (eqa f g))))
@@ -295,23 +313,45 @@
                    g o ( h o equalizer1 (eqa (f o h) ( g o h )))
              ∎
      cong-α1 : {a b c :  Obj A } → { e : Hom A c a }
-          → {f g g' : Hom A a b } →  A [ g ≈ g' ] → A [ equalizer1 (eqa {a} {b} {c} f g )≈ equalizer1 (eqa {a} {b} {c} f g' ) ] 
-     cong-α1 {a} {b} {c} {e} {f} {g} {g'} eq = {!!} -- let open ≈-Reasoning (A) in refl-hom 
-     cong-γ1 :  {a c d : Obj A } → {f g : Hom A a b} {h h' : Hom A d a } →  A [ h ≈ h' ] →  
-                     A [  k (eqa f g ) {d} ( A [ h  o (equalizer1 ( eqa (A [ f  o  h  ] ) (A [ g o h  ] )  )) ] ) (lemma-equ4 {a} {b} {c} {d} f g h ) 
-                       ≈  k (eqa f g ) {d} ( A [ h' o (equalizer1 ( eqa (A [ f  o  h' ] ) (A [ g o h' ] )  )) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' )  ]
+          → {f g g' : Hom A a b } →  A [ g ≈ g' ] → A [ equalizer1 (eqa {a} {b} {c} f g ) ≈ equalizer1 (eqa {a} {b} {c} f g'  ) ] 
+     cong-α1 {a} {b} {c} {e} {f} {g} {g'} eq = begin 
+                equalizer1 (eqa f g)   
+             ≈↑⟨ ek=h (eqa f g') ⟩
+                equalizer1 (eqa f g') o k (eqa f g') (eqa-e f g) {!!}
+             ≈⟨ cdr ( uniqueness (eqa f g') {!!})  ⟩
+                equalizer1 (eqa f g')   o id1 A c
+             ≈⟨ idR ⟩
+                equalizer1 (eqa f g')   
+             ∎ where open ≈-Reasoning (A) 
+     cong-γ1 :  {a c d : Obj A } → {f g : Hom A a b} {h h' : Hom A d a } →  A [ h ≈ h' ] → 
+                     A [  k (eqa f g  ) {d} ( A [ h  o (equalizer1 ( eqa (A [ f  o  h  ] ) (A [ g o h  ] )  )) ] ) (lemma-equ4 {a} {b} {c} {d} f g h ) 
+                       ≈  k (eqa f g  ) {d} ( A [ h' o (equalizer1 ( eqa (A [ f  o  h' ] ) (A [ g o h' ] )  )) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' )  ]
      cong-γ1 {a} {c} {d} {f} {g} {h} {h'} h=h'  = let open ≈-Reasoning (A) in begin
                  k (eqa f g ) {d} ( A [ h  o (equalizer1 ( eqa (A [ f  o  h  ] ) (A [ g o h  ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h )
-             ≈⟨ uniqueness (eqa f g) {!!} ⟩    
+             ≈⟨ {!!} ⟩
+                 k (eqa f g)       (A [ h o  (eqa-e (A [ f o h' ])  (A [ g o h' ])) ] ) {!!}
+             ≈⟨ uniqueness (eqa f g) ( begin
+                 eqa-e f g o k (eqa f g ) {d} ( A [ h' o (equalizer1 ( eqa (A [ f  o  h' ] ) (A [ g o h' ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' )
+             ≈⟨ ek=h (eqa f g ) ⟩
+                 h' o (equalizer1 ( eqa (A [ f  o  h' ] ) (A [ g o h' ] )))
+             ≈↑⟨ car h=h'  ⟩
+                 h o (equalizer1 ( eqa (A [ f  o  h' ] ) (A [ g o h' ] )))
+             ∎ )⟩    
                  k (eqa f g ) {d} ( A [ h' o (equalizer1 ( eqa (A [ f  o  h' ] ) (A [ g o h' ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' )
              ∎
-     cong-δ1 : {a b c : Obj A} {e : Hom A c a } {f f' : Hom A a b} → A [ f ≈ f' ] →  A [ k (eqa {a} {b} {c} f f ) (id1 A a)  (f1=f1 f)  ≈ 
-                                                                            k (eqa {a} {b} {c} f' f' ) (id1 A a)  (f1=f1 f') ]
-     cong-δ1 {a} {b} {c} {e} {f} {f'} f=f' =  let open ≈-Reasoning (A) in
+     cong-δ1 : {a b c : Obj A}  {f f' : Hom A a b} → A [ f ≈ f' ] →  A [ k (eqa {a} {b} {c} f f ) (id1 A a)  (f1=f1 f)  ≈ 
+                                                                            k (eqa {a} {b} {c} f' f'  ) (id1 A a)  (f1=f1 f') ]
+     cong-δ1 {a} {b} {c}  {f} {f'} f=f' =  let open ≈-Reasoning (A) in
              begin
-                 k (eqa {a} {b} {c} f  f  ) (id a)  (f1=f1 f) 
-             ≈⟨  uniqueness (eqa f f) {!!} ⟩
-                 k (eqa {a} {b} {c} f' f' ) (id a)  (f1=f1 f') 
+                 k (eqa {a} {b} {c} f  f   ) (id a)  (f1=f1 f) 
+             ≈⟨  uniqueness (eqa f f) ( begin
+                  eqa-e f f o k (eqa {a} {b} {c} f' f'  ) (id a)  (f1=f1 f') 
+             ≈⟨ {!!} ⟩ -- ≈⟨ ek=h (eqa {a} {b} {c} f' f'  ) ⟩
+                  eqa-e f' f' o k (eqa {a} {b} {c} f' f'  ) (id a)  (f1=f1 f') 
+             ≈⟨ ek=h (eqa {a} {b} {c} f' f'  ) ⟩
+                 id a
+             ∎ )⟩
+                 k (eqa {a} {b} {c} f' f'  ) (id a)  (f1=f1 f') 
              ∎
 
      lemma-b2 :  {d : Obj A} {h : Hom A d a} → A [
@@ -341,7 +381,7 @@
                 ≈↑⟨ idR  ⟩
                          (equalizer1 (eqa f g) o j )  o id d
                 ≈⟨ {!!} ⟩         -- here we decide e (fej) (gej)' is id d
-                        {!!}
+                        ((equalizer1 (eqa f g) o j) o equalizer1 (eqa (f o equalizer1 (eqa f g ) o j) (g o equalizer1 (eqa f g ) o j)))
              ∎ ))) ⟩
                     j o k (eqa (( f o ( equalizer1 (eqa f g) o j ) )) (( f o ( equalizer1 (eqa f g) o j ) ))) (id1 A d) (f1=f1 (( f o ( equalizer1 (eqa f g) o j ) ))) 
              ≈⟨ cdr ((uniqueness (eqa (( f o ( equalizer1 (eqa f g) o j ) )) (( f o ( equalizer1 (eqa f g) o j ) ))) ( begin
@@ -349,7 +389,7 @@
                 ≈⟨ idR ⟩
                      equalizer1 (eqa (f o equalizer1 (eqa f g ) o j) (f o equalizer1 (eqa f g ) o j))  
                 ≈⟨ {!!} ⟩         -- here we decide e (fej) (fej)' is id d
-                    {!!}
+                    id d
              ∎ ))) ⟩
                     j o id d
                 ≈⟨ idR ⟩
@@ -384,9 +424,9 @@
              ≈⟨ car (b2 bur) ⟩
                   ( h o ( α bur ( f o h ) ( g o h ) (id d))) o δ bur {d} {b} {d} (id d) (f o h) 
              ≈↑⟨ assoc ⟩
-                   h o ((( α bur ( f o h ) ( g o h ) (id d) )) o δ bur {d} {b} {d} (id d) (f o h)  )
-             ≈↑⟨ cdr ( car ( cong-α bur eq)) ⟩
-                   h o ((( α bur ( f o h ) ( f o h ) (id d)))o δ bur {d} {b} {d} (id d) (f o h)  )
+                   h o ((( α bur ( f o h ) ( g o h ) (id d ))) o δ bur {d} {b} {d} (id d) (f o h)  )
+             ≈⟨ {!!} ⟩
+                   h o ((( α bur ( f o h ) ( f o h ) (id d ))) o δ bur {d} {b} {d} (id d) (f o h)  )
              ≈⟨ cdr (b3 bur {d} {b} {d} (f  o h) {id d} ) ⟩
                    h o id d
              ≈⟨ idR ⟩