Mercurial > hg > Members > kono > Proof > category

diff deductive.agda @ 830:232cea484067

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
graph to CCC again
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 15 Mar 2020 14:26:39 +0900
parents 6c5cfb9b333e
children
line wrap: on
line diff
--- a/deductive.agda	Sat Jul 13 00:18:17 2019 +0900
+++ b/deductive.agda	Sun Mar 15 14:26:39 2020 +0900
@@ -44,3 +44,6 @@
   k x∈a (iii ψ χ ) = < k x∈a ψ  , k x∈a χ  >
   k x∈a (iv ψ χ ) = k x∈a ψ  ・ < π , k x∈a χ  >
   k x∈a (v ψ ) = ( k x∈a ψ  ・ α ) *
+
+--  toφ : {a b c : Obj A } → ( x∈a : Hom A ⊤ a ) → (z : Hom A b c ) → φ {a} x∈a z  
+--  toφ {a} {b} {c} x∈a z = {!!}