Mercurial > hg > Members > kono > Proof > category

diff CCCGraph.agda @ 948:dca4b29553cb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
mp-flatten
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 22 Aug 2020 10:45:40 +0900
parents 095fd0829ccf
children
line wrap: on
line diff
--- a/CCCGraph.agda	Mon May 18 23:13:14 2020 +0900
+++ b/CCCGraph.agda	Sat Aug 22 10:45:40 2020 +0900
@@ -457,7 +457,7 @@
 ccc-graph-univ :  {c₁ c₂ : Level} → UniversalMapping (Grph {c₁} {c₂}) (Cart {suc c₁ } {c₁ ⊔ c₂} {c₁ ⊔ c₂}) forgetful.UX 
 ccc-graph-univ {c₁} {c₂} = record {
      F = F ;
-     η = η ; -- λ a → record { vmap = λ y →  graphtocat.Chain {!!} {!!} {!!}  ; emap = λ f x →  {!!} } ; -- 
+     η = η ; 
      _* = solution ;
      isUniversalMapping = record {
          universalMapping = {!!} ;