Mercurial > hg > Members > kono > Proof > category

comparison 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
comparison
equal deleted inserted replaced
1033:a59c51b541a2 1034:40c39d3e6a75
113 ≡⟨ IsFunctor.distr (isFunctor S ) ⟩ 113 ≡⟨ IsFunctor.distr (isFunctor S ) ⟩
114 C [ FMap S (FMap T g) o FMap S (FMap T f) ] 114 C [ FMap S (FMap T g) o FMap S (FMap T f) ]
115 ∎ 115 ∎
116 116
117 117
118 import Axiom.Extensionality.Propositional 118 -- import Axiom.Extensionality.Propositional
119 postulate extensionality : { c₂ : Level} ( A : Category {c₂} ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ 119 -- postulate extensionality : { c₂ : Level} ( A : Category {c₂} ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂
120 120
121 -- 121 --
122 -- t a 122 -- t a
123 -- F a -----→ G a 123 -- F a -----→ G a
124 -- | | 124 -- | |