Mercurial > hg > Members > kono > Proof > category

changeset 655:26a28b1cee6f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
universal mapping
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 05 Jul 2017 10:35:17 +0900
parents 2872af3b32cc
children 18431b63893b
files freyd2.agda
diffstat 1 files changed, 8 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/freyd2.agda	Wed Jul 05 10:30:17 2017 +0900
+++ b/freyd2.agda	Wed Jul 05 10:35:17 2017 +0900
@@ -413,6 +413,14 @@
          comm1 : B [ B [ FMap U g o hom (i a) ] ≈ B [ B [ FMap U g o tmap-η a ] o FMap (K B A a) g ] ]
          comm1 = let open ≈-Reasoning B in sym idR
 
+   UM : UniversalMapping B A U (λ b → obj (i b)) (tmap-η)
+   UM = record {
+         _* = λ f → arrow (solution f)  ;
+         isUniversalMapping = record {
+            universalMapping  = λ {a} {b} {f} → univ f ;
+            uniquness = unique
+      }}
+
    F : Functor B A
    F = record {
     FObj = λ b →  obj (i b)