Mercurial > hg > Members > kono > Proof > category

comparison yoneda.agda @ 781:340708e8d54f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix for 2.5.4.2
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 08 Mar 2019 17:46:59 +0900
parents 984518c56e96
children bded2347efa4
comparison
equal deleted inserted replaced
780:b44c1c6ce646 781:340708e8d54f
14 14
15 open import HomReasoning 15 open import HomReasoning
16 open import cat-utility 16 open import cat-utility
17 open import Relation.Binary.Core 17 open import Relation.Binary.Core
18 open import Relation.Binary 18 open import Relation.Binary
19 open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym )
20
19 21
20 22
21 -- Contravariant Functor : op A → Sets ( Obj of Sets^{A^op} ) 23 -- Contravariant Functor : op A → Sets ( Obj of Sets^{A^op} )
22 -- Obj and Hom of Sets^A^op 24 -- Obj and Hom of Sets^A^op
23 25