Mercurial > hg > Members > kono > Proof > category

diff src/stdalone-kleisli.agda @ 1034:40c39d3e6a75

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 31 Mar 2021 15:58:02 +0900
parents e7b0db851a70
children 5620d4a85069
line wrap: on
line diff
--- a/src/stdalone-kleisli.agda	Tue Mar 30 23:31:10 2021 +0900
+++ b/src/stdalone-kleisli.agda	Wed Mar 31 15:58:02 2021 +0900
@@ -115,8 +115,8 @@
            ∎
 
 
-import Axiom.Extensionality.Propositional
-postulate extensionality : {  c₂  : Level} ( A : Category  {c₂} ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂
+-- import Axiom.Extensionality.Propositional
+-- postulate extensionality : {  c₂  : Level} ( A : Category  {c₂} ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂
 
 --
 --            t a