Mercurial > hg > Members > kono > Proof > category

changeset 958:9089540fe89d

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 16:49:01 +0900
parents e29b6488b179
children d743fd968582
files src/equalizer.agda
diffstat 1 files changed, 32 insertions(+), 26 deletions(-) [+]
line wrap: on
line diff
--- a/src/equalizer.agda	Sun Feb 21 12:57:05 2021 +0900
+++ b/src/equalizer.agda	Sun Feb 21 16:49:01 2021 +0900
@@ -47,20 +47,20 @@
 -- Burroni's Flat Equational Definition of Equalizer
 --
 
-record Burroni {a b : Obj A} (f g : Hom A a b) : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
+record Burroni : 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)))
+      b1 : {a b : Obj A } → (f g : Hom A a b) → A [ A [ f  o α f g ] ≈ A [ g  o α f g ] ]
+   b1k :  {a b : Obj A } → (f g : Hom A a b) → {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 f g {d} {k} = ≈-Reasoning.trans-hom A (≈-Reasoning.assoc A) (≈-Reasoning.trans-hom A (≈-Reasoning.car A (b1 f g)) (≈-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 ]
+      b2 : {a b d : Obj A} {h : Hom A d a } → (f g : Hom A a b) → A [ A [ ( α f g ) o (γ f g h) ] ≈ A [ h  o α (A [ f o h ]) (A [ g o h ]) ] ]
+      b3 : {a b   : Obj A} (f g : Hom A a b) → (f=g : A [ f ≈ g ]) → A [ A [ α f g o δ f g f=g ] ≈ id1 A a ]
+      b4 : {a b d : Obj A} (f g : Hom A a b) → {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 f g) ) )] ≈ 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 ]
 
@@ -247,22 +247,21 @@
 --
 ----
 
-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 f g 
-lemma-equ1  {a} {b}  f g eqa  = record {
+lemma-equ1 : ({a b : Obj A} (f g : Hom A a b) → Equalizer A f g ) → Burroni 
+lemma-equ1  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 ] ))) ] )
            (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 ))
+    ; b1 = λ f g → fe=ge (isEqualizer (eqa f g ))
     ; b2 = lemma-b2 
-    ; b3 = λ {d} {h} → lemma-b3 f f {h} (≈-Reasoning.refl-hom A)
+    ; b3 = λ {a } {b} f g f=g → lemma-b3 f g f=g 
     ; 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 }
+     lemma-b3 : {a b : Obj A} (f g : Hom A a b ) 
         → (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
@@ -282,25 +281,25 @@
              ≈↑⟨ assoc ⟩
                    g o ( h o equalizer (eqa (f o h) ( g o h )))
              ∎
-     lemma-b2 :  {d : Obj A} {h : Hom A d a} → A [
+     lemma-b2 : {a b d : Obj A} {h : Hom A d a} → (f g : Hom A a b) → 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
+     lemma-b2 {a} {b} {d} {h} f g = 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 [
+     lemma-b4 : {a b d : Obj A} (f g : Hom A a b) → {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 ]
      --   h = equalizer (eqa f g) o j 
-     lemma-b4 {d} {j} = 
+     lemma-b4 {a} {b} {d} f g  {j} = 
              begin
-                 k (ieqa f g) (( h o equalizer (eqa (( f o h )) (( g o h ))) )) (lemma-equ4 {a} {b} {d} f g (h))
+                 k (ieqa f g) ( h o equalizer (eqa ( f o h ) ( g o h )) ) (lemma-equ4 {a} {b} {d} f g h)
                  o    k (ieqa (f o h) ( g o h)) (id1 A _) (f1=g1 (f1=gh (fe=ge (ieqa f g))) (id1 A _))
              ≈↑⟨ uniqueness (ieqa f g) ( begin
                   equalizer (eqa f g) o ( k (ieqa f g) (( h o equalizer (eqa ( f o h ) ( g o h )) )) (lemma-equ4 {a} {b} {d} f g h)
@@ -333,8 +332,7 @@
 -- Bourroni equations gives an Equalizer
 --
 
-lemma-equ2 : {a b : Obj A} (f g : Hom A a b)  
-         → ( bur : Burroni f g ) → IsEqualizer A {equ bur f g} {a} {b} (α bur f g ) f g 
+lemma-equ2 : {a b : Obj A} (f g : Hom A a b) → ( bur : Burroni ) → 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 ;
@@ -348,12 +346,18 @@
       k1 :  {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c
       k1 {d} h fh=gh = β bur {d} {a} {b} f g h fh=gh
       fe=ge1 : A [ A [ f o (α bur f g ) ] ≈ A [ g o (α bur f g ) ] ]
-      fe=ge1 = b1 bur
+      fe=ge1 = b1 bur f g
       ek=h1 : {d : Obj A}  → ∀ {h : Hom A d a} →  {eq : A [ A [ f  o  h ] ≈ A [ g  o h ] ] } →  A [ A [ (α bur f g )  o k1 {d} h eq ] ≈ h ]
       ek=h1 {d} {h} {eq} =  let open ≈-Reasoning (A) in
              begin
                  α bur f g  o k1 h eq 
-             ≈⟨ {!!} ⟩
+             ≈⟨ assoc ⟩
+                 (α bur f g o γ bur f g h) o δ bur (f o h) (g o h) eq
+             ≈⟨ car (b2 bur f g) ⟩
+                 ( h o α bur ( f o h ) ( g o h ) ) o δ bur (f o h) (g o h) eq
+             ≈↑⟨ assoc ⟩
+                   h o α bur (f o h) (g o h) o δ bur (f o h) (g o h) eq
+             ≈⟨ cdr ( b3 bur (f o h) (g o h) eq ) ⟩
                    h o id d
              ≈⟨ idR ⟩
                  h 
@@ -363,10 +367,12 @@
       uniqueness1 {d} {h} {eq} {k'} ek=h =   let open ≈-Reasoning (A) in
              begin
                 k1 {d} h eq
+             ≈⟨⟩
+                γ bur f g h o δ bur (f o h) (g o 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'
+                γ 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 f g )))
+             ≈⟨ b4 bur f g ⟩
+                k'
              ∎