Mercurial > hg > Members > kono > Proof > category

changeset 653:893ae9a95ee1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
solution
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 05 Jul 2017 09:55:31 +0900
parents 236e916760e6
children 2872af3b32cc
files freyd2.agda
diffstat 1 files changed, 8 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/freyd2.agda	Wed Jul 05 09:39:58 2017 +0900
+++ b/freyd2.agda	Wed Jul 05 09:55:31 2017 +0900
@@ -388,9 +388,15 @@
    solution : {a : Obj B} {b : Obj A}  → ( f : Hom B a (FObj U b) ) → CommaHom (K B A a) U (i a) (sobj f)
    solution {a} {b} f = initial (In a) (sobj f)
 
-   univ : (a : Obj B) (b : Obj A)  → (f : Hom B a (FObj U b))
+   univ : {a : Obj B} {b : Obj A}  → (f : Hom B a (FObj U b))
        → B [ B [ FMap U (arrow (solution f)) o tmap-η a ]  ≈ f ]
-   univ = {!!}
+   univ {a} {b} f = let open ≈-Reasoning B in begin
+        FMap U (arrow (solution f)) o tmap-η a 
+      ≈⟨ comm (initial (In a) (sobj f))  ⟩
+        hom (sobj f) o FMap (K B A a) (arrow (initial (In a) (sobj f)))
+      ≈⟨ idR ⟩
+        f 
+      ∎  
 
    ηf : (a b  : Obj B)  → ( f : Hom B a b ) → Obj ( K B A a ↓ U)
    ηf a b f  = sobj ( B [ tmap-η b o f ]  )