Mercurial > hg > Members > kono > Proof > category

changeset 418:7091104a8cb4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
assoc passed
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 24 Mar 2016 02:07:45 +0900
parents 1e76e611d454
children 8919c162b894
files limit-to.agda
diffstat 1 files changed, 37 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Thu Mar 24 01:48:13 2016 +0900
+++ b/limit-to.agda	Thu Mar 24 02:07:45 2016 +0900
@@ -178,19 +178,43 @@
 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just id-t1   | just id-t1   | just arrow-g = ==refl
 assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} {f} {g} {h} | just id-t1   | just id-t1   | just id-t1  = ==refl
 --  remaining all failure case
-assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} | just _ | just _ | nothing = {!!}
-assoc-× {c₁} {c₂} {t1} {t0} {_} {_} {f} {g} {h} | just _   | just _   | just _  = let open ==-Reasoning  {c₁}  {c₂} in
-                begin
-                   {!!}
-                ==⟨ {!!}  ⟩
-                  {!!}
-                ∎
-... | just _ | just _ | just _ =  let open ==-Reasoning  {c₁}  {c₂} in
-                begin
-                   {!!}
-                ==⟨ {!!}  ⟩
-                  {!!}
-                ∎
+assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} {f} {g} {h} | just id-t0 | just id-t0 | nothing = nothing
+assoc-× {c₁} {c₂} {t1} {t0} {t0} {t0} {f} {g} {h} | just id-t0 | just id-t0 | nothing = nothing
+assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | nothing = nothing
+assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | nothing = nothing
+assoc-× {c₁} {c₂} {t0} {t1} {t0} {t0} {f} {g} {h} | just id-t0 | just inv-f | nothing = nothing
+assoc-× {c₁} {c₂} {t1} {t1} {t0} {t0} {f} {g} {h} | just id-t0 | just inv-f | nothing = nothing
+assoc-× {c₁} {c₂} {t1} {t0} {t0} {t1} {f} {g} {h} | just arrow-f | just id-t0 | nothing = nothing
+assoc-× {c₁} {c₂} {t1} {t0} {t0} {t1} {f} {g} {h} | just arrow-g | just id-t0 | nothing = nothing
+assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-f | just id-t0 | nothing = nothing
+assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-g | just id-t0 | nothing = nothing
+assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-f | nothing = nothing
+assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-g | nothing = nothing
+assoc-× {c₁} {c₂} {t1} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-f | nothing = nothing
+assoc-× {c₁} {c₂} {t1} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-g | nothing = nothing
+assoc-× {c₁} {c₂} {t0} {t1} {t1} {t0} {f} {g} {h} | just inv-f | just id-t1 | nothing = nothing
+assoc-× {c₁} {c₂} {t1} {t1} {t1} {t0} {f} {g} {h} | just inv-f | just id-t1 | nothing = nothing
+assoc-× {_} {_} {t0} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just _) | nothing = nothing
+assoc-× {_} {_} {t0} {t1} {t0} {t1} {_} {_} {_} | (just _) | (just _) | nothing = nothing
+assoc-× {_} {_} {t1} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just _) | nothing = nothing
+assoc-× {_} {_} {t1} {t1} {t0} {t1} {_} {_} {_} | (just _) | (just _) | nothing = nothing
+assoc-× {_} {_} {t0} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just arrow-f) | (just id-t0) = nothing
+assoc-× {_} {_} {t0} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just arrow-g) | (just id-t0) = nothing
+assoc-× {_} {_} {t0} {t1} {t0} {t0} {_} {_} {_} | (just id-t0) | (just inv-f) | (just _) = nothing
+assoc-× {_} {_} {t0} {t1} {t0} {t1} {_} {_} {_} | (just _) | (just _) | (just _) = nothing
+assoc-× {_} {_} {t0} {t1} {t1} {t0} {_} {_} {_} | (just inv-f) | (just id-t1) | (just arrow-f) = nothing
+assoc-× {_} {_} {t0} {t1} {t1} {t0} {_} {_} {_} | (just inv-f) | (just id-t1) | (just arrow-g) = nothing
+assoc-× {_} {_} {t1} {t0} {t0} {t0} {_} {_} {_} | (just id-t0) | (just id-t0) | (just inv-f) = ==refl
+assoc-× {_} {_} {t1} {t0} {t0} {t1} {_} {_} {_} | (just arrow-f) | (just id-t0) | (just inv-f) = nothing
+assoc-× {_} {_} {t1} {t0} {t0} {t1} {_} {_} {_} | (just arrow-g) | (just id-t0) | (just inv-f) = nothing
+assoc-× {_} {_} {t1} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just _) | (just _) = nothing
+assoc-× {_} {_} {t1} {t0} {t1} {t1} {_} {_} {_} | (just id-t1) | (just arrow-f) | (just _) = nothing
+assoc-× {_} {_} {t1} {t0} {t1} {t1} {_} {_} {_} | (just id-t1) | (just arrow-g) | (just _) = nothing
+assoc-× {_} {_} {t1} {t1} {t0} {t0} {_} {_} {_} | (just id-t0) | (just inv-f) | (just id-t1) = ==refl
+assoc-× {_} {_} {t1} {t1} {t0} {t1} {_} {_} {_} | (just arrow-f) | (just inv-f) | (just id-t1) = ==refl
+assoc-× {_} {_} {t1} {t1} {t0} {t1} {_} {_} {_} | (just arrow-g) | (just inv-f) | (just id-t1) = ==refl
+assoc-× {_} {_} {t1} {t1} {t1} {t0} {_} {_} {_} | (just inv-f) | (just id-t1) | (just id-t1) = ==refl
+
 
 
 TwoId :  {c₁  c₂ : Level } (a : TwoObject  {c₁} ) ->  (TwoHom {c₁}  {c₂ } a a )