Mercurial > hg > Members > kono > Proof > category

changeset 959:d743fd968582

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 20:40:00 +0900
parents 9089540fe89d
children 062974e39cc7
files src/equalizer.agda
diffstat 1 files changed, 20 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/equalizer.agda	Sun Feb 21 16:49:01 2021 +0900
+++ b/src/equalizer.agda	Sun Feb 21 20:40:00 2021 +0900
@@ -364,16 +364,33 @@
              ∎
       uniqueness1 : {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 [ (α bur f g ) o k' ] ≈ h ] → A [ k1 {d} h eq  ≈ k' ]
-      uniqueness1 {d} {h} {eq} {k'} ek=h =   let open ≈-Reasoning (A) in
+      uniqueness1 {d} {h} {eq} {k'} ek=h =  
              begin
                 k1 {d} h eq
              ≈⟨⟩
                 γ bur f g h o δ bur (f o h) (g o h) eq
-             ≈⟨ {!!} ⟩
+             ≈⟨ cdr {!!} ⟩
+                γ bur f g h  o (q o (δ bur ( f o ( α bur f g o k' )) ( g o ( α bur f g o k' )) (f1=gh (b1 bur f g )))) 
+             ≈⟨ car {!!} ⟩
+                (γ bur f g (α bur f g o k' ) o p ) o (q o (δ bur ( f o ( α bur f g o k' )) ( g o ( α bur f g o k' )) (f1=gh (b1 bur f g ))))
+             ≈↑⟨ assoc ⟩
+                γ bur f g (α bur f g o k' ) o (p  o (q o (δ bur ( f o ( α bur f g o k' )) ( g o ( α bur f g o k' )) (f1=gh (b1 bur f g )))))
+             ≈⟨ cdr assoc ⟩
+                γ bur f g (α bur f g o k' ) o ((p  o q ) o (δ bur ( f o ( α bur f g o k' )) ( g o ( α bur f g o k' )) (f1=gh (b1 bur f g ))))
+             ≈⟨ cdr (car pq=1) ⟩
+                γ bur f g (α bur f g o k' ) o (id1 A _ o (δ bur ( f o ( α bur f g o k' )) ( g o ( α bur f g o k' )) (f1=gh (b1 bur f g ))))
+             ≈⟨ cdr idL ⟩
                 γ 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'
-             ∎
+             ∎ where
+                open ≈-Reasoning A
+                p : Hom A (equ bur (f o h) (g o h)) (equ bur (f o ( α bur f g o k'))(g o ( α bur f g o k')))
+                p = ?
+                q : Hom A (equ bur (f o ( α bur f g o k'))(g o ( α bur f g o k'))) (equ bur (f o h) (g o h)) 
+                q = ?
+                pq=1 : A [ A [ p o q ] ≈ id1 A _ ]
+                pq=1 = {!!}
 
 
 -- end