Mercurial > hg > Members > kono > Proof > category

changeset 956:468288f3dfe5

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, 21 Feb 2021 10:26:00 +0900
parents 5c8694236ff3
children e29b6488b179
files src/equalizer.agda
diffstat 1 files changed, 87 insertions(+), 34 deletions(-) [+]
line wrap: on
line diff
--- a/src/equalizer.agda	Sun Feb 21 04:23:24 2021 +0900
+++ b/src/equalizer.agda	Sun Feb 21 10:26:00 2021 +0900
@@ -21,31 +21,6 @@
 open import cat-utility
 
 --
--- Burroni's Flat Equational Definition of Equalizer
---
-
-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 ]
-   β : { d a b : Obj A}  → (f g : Hom A a b) → (h : Hom A d a ) → A [ A [ f o h ]  ≈ A [ g o h ] ] → Hom A d (equ f g)
-   β {d} {a} {b} f g h eq =  A [ γ f g h o δ (A [ f o h ]) (A [ g o h ]) eq ]
-
-open Equalizer
-open IsEqualizer
-open Burroni
-
---
 -- Some obvious conditions for k  (fe = ge) → ( fh = gh )
 --
 
@@ -68,6 +43,31 @@
                   g o ( e  o h )
              ∎
 
+--
+-- Burroni's Flat Equational Definition of Equalizer
+--
+
+record Burroni {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 ] ] ) (f1=gh b1 ) )] ≈ k ]
+   β : { d a b : Obj A}  → (f g : Hom A a b) → (h : Hom A d a ) → A [ A [ f o h ]  ≈ A [ g o h ] ] → Hom A d (equ f g)
+   β {d} {a} {b} f g h eq =  A [ γ f g h o δ (A [ f o h ]) (A [ g o h ]) eq ]
+
+open Equalizer
+open IsEqualizer
+open Burroni
+
 -------------------------------
 -- 
 -- Every equalizer is monic
@@ -248,18 +248,71 @@
 ----
 
 lemma-equ1 : {a b : Obj A} (f g : Hom A a b)
-      → ({a b : Obj A} (f g : Hom A a b) → Equalizer A f g ) → Burroni A f g 
+      → ({a b : Obj A} (f g : Hom A a b) → Equalizer A f g ) → Burroni f g 
 lemma-equ1  {a} {b}  f g eqa  = record {
       equ = λ f g → equalizer-c (eqa f g)
     ; α = λ f g   →  equalizer (eqa f g)
     ; γ = λ f g h → k (isEqualizer (eqa f g )) ( A [ h  o (equalizer ( eqa (A [ f  o  h ] ) (A [ g o h ] ))) ] )
-           {!!} -- (fe=ge (isEqualizer (eqa  (A [ f  o  h ] ) (A [ g o h ] )))) 
-    ; δ =  {!!} 
+           (lemma-equ4 f g h) 
+    ; δ =   λ {a} {b} f g f=g → k (isEqualizer (eqa {a} {b} f g )) {a} (id1 A a) (f1=g1 f=g _ )
     ; b1 = fe=ge (isEqualizer (eqa f g ))
-    ; b2 = λ {d} {h} → {!!}
-    ; b3 = {!!} 
-    ; b4 = {!!}
- } 
+    ; b2 = lemma-b2 
+    ; b3 = λ {d} {h} → lemma-b3 f f {h} (≈-Reasoning.refl-hom A)
+    ; b4 = lemma-b4
+ }  where
+     ieqa : {a b : Obj A} (f g : Hom A a b) → IsEqualizer A ( equalizer (eqa f g )) f g 
+     ieqa f g = isEqualizer (eqa f g) 
+     lemma-b3 : {a b d : Obj A} (f g : Hom A a b ) { h : Hom A d a }
+        → (f=g : A [ f ≈ g ] ) → A [ A [ equalizer (eqa f g ) o k (isEqualizer (eqa f g)) (id1 A a) (f1=g1 f=g _ ) ] ≈ id1 A a  ]
+     lemma-b3 {a} f g f=g = let open ≈-Reasoning (A) in
+             begin
+                  equalizer (eqa f g) o k (isEqualizer (eqa f g)) (id a) (f1=g1 f=g _ )
+             ≈⟨ ek=h (isEqualizer (eqa f g ))  ⟩
+                  id a
+             ∎
+     lemma-equ4 :  {a b d : Obj A}  → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) →
+                      A [ A [ f o A [ h o equalizer (eqa (A [ f o h ]) (A [ g o h ])) ] ] ≈ A [ g o A [ h o equalizer (eqa (A [ f o h ]) (A [ g o h ])) ] ] ]
+     lemma-equ4 {a} {b} {d} f g h  = let open ≈-Reasoning (A) in
+             begin
+                   f o ( h o equalizer (eqa (f o h) ( g o h )))
+             ≈⟨ assoc ⟩
+                   (f o h) o equalizer (eqa (f o h) ( g o h ))
+             ≈⟨ fe=ge (isEqualizer (eqa (A [ f o h ]) (A [ g o h ]))) ⟩
+                   (g o h) o equalizer (eqa (f o h) ( g o h ))
+             ≈↑⟨ assoc ⟩
+                   g o ( h o equalizer (eqa (f o h) ( g o h )))
+             ∎
+     lemma-b2 :  {d : Obj A} {h : Hom A d a} → A [
+                      A [ equalizer (eqa f g) o k (isEqualizer (eqa f g)) (A [ h o equalizer (eqa (A [ f o h ]) (A [ g o h ])) ]) (lemma-equ4 {a} {b} f g h) ]
+                    ≈ A [ h o equalizer (eqa (A [ f o h ]) (A [ g o h ])) ] ]
+     lemma-b2 {d} {h} = let open ≈-Reasoning (A) in
+             begin
+                    equalizer (eqa f g) o k (isEqualizer (eqa f g)) (h o equalizer (eqa (f o h) (g o h))) (lemma-equ4 {a} {b} f g h)
+             ≈⟨ ek=h (isEqualizer (eqa f g))  ⟩
+                    h o equalizer (eqa (f o h ) ( g o h ))
+             ∎
+     lemma-b4 : {d : Obj A} {j : Hom A d (equalizer-c (eqa f g))} → A [
+              A [ k (ieqa f g) (A [ A [ equalizer (eqa f g) o j ] o 
+                              equalizer (eqa (A [ f o A [ equalizer (eqa f g ) o j ] ]) (A [ g o A [ equalizer (eqa f g  ) o j ] ])) ])
+                     (lemma-equ4 {a} {b} {d} f g (A [ equalizer (eqa f g) o j ])) 
+                 o    k (ieqa (A [ f o A [ equalizer (eqa f g) o j ] ]) (A [ g o A [ equalizer (eqa f g) o j ] ])) (id1 A _)
+                     (f1=g1 (f1=gh (fe=ge (ieqa f g))) (id1 A _))] ≈ j ]
+     lemma-b4 {d} {j} = let open ≈-Reasoning (A) in
+             begin
+                 k (ieqa f g) (( ( equalizer (eqa f g) o j ) o equalizer (eqa (( f o ( equalizer (eqa f g ) o j ) )) (( g o ( equalizer (eqa f g ) o j ) ))) ))
+                            (lemma-equ4 {a} {b} {d} f g (( equalizer (eqa f g) o j )))
+                 o    k (ieqa (f o ( equalizer (eqa f g) o j )) ( g o (equalizer (eqa f g) o j ))) (id1 A _)
+                     (f1=g1 (f1=gh (fe=ge (ieqa f g))) (id1 A _))
+             ≈⟨ car (uniqueness (ieqa f g) {!!}) ⟩
+                 {!!} o {!!}
+             ≈⟨ cdr (uniqueness (ieqa (f o ( equalizer (eqa f g) o j )) ( g o (equalizer (eqa f g) o j ))) {!!}) ⟩
+                 {!!} o {!!}
+             ≈⟨ {!!} ⟩
+                 j
+             ∎ 
+
+
+
 
 --------------------------------
 --
@@ -267,7 +320,7 @@
 --
 
 lemma-equ2 : {a b : Obj A} (f g : Hom A a b)  
-         → ( bur : Burroni A f g ) → IsEqualizer A {equ bur f g} {a} {b} (α bur f g ) f g 
+         → ( bur : Burroni f g ) → IsEqualizer A {equ bur f g} {a} {b} (α bur f g ) f g 
 lemma-equ2 {a} {b} f g bur = record {
       fe=ge = fe=ge1 ;  
       k = k1 ;
@@ -297,7 +350,7 @@
              begin
                 k1 {d} h eq
              ≈⟨ {!!} ⟩
-                 {!!}
+                 γ bur f g (α bur f g o k' ) o (δ bur ( f o ( α bur f g o k' )) ( g o ( α bur f g o k' )) (f1=gh (b1 bur)))
              ≈⟨ b4 bur ⟩
                  k'
              ∎