# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1613911141 -32400
# Node ID 062974e39cc7d80685f26ddabc3da2a2f52b82cf
# Parent  d743fd9685820ecfcf5c1c6cd36cc18474dc2bdc
...

diff -r d743fd968582 -r 062974e39cc7 src/equalizer.agda
--- 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 = {!!}