Mercurial > hg > Members > kono > Proof > category

changeset 960:062974e39cc7

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 21:39:01 +0900
parents d743fd968582
children 0719e76cd3b8
files src/equalizer.agda
diffstat 1 files changed, 2 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/equalizer.agda	Sun Feb 21 20:40:00 2021 +0900
+++ b/src/equalizer.agda	Sun Feb 21 21:39:01 2021 +0900
@@ -386,9 +386,9 @@
              ∎ 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 = ?
+                p = γ bur (f o ( α bur f g o k')) (g o ( α bur f g o k')) (id1 A _) o δ bur {!!} {!!} {!!} o {!!}
                 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 = ?
+                q = γ bur (f o h) (g o h) (id1 A _) o  δ bur {!!} {!!} {!!} o {!!} 
                 pq=1 : A [ A [ p o q ] ≈ id1 A _ ]
                 pq=1 = {!!}