Mercurial > hg > Members > kono > Proof > category

comparison freyd2.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 7a6ee564e3a8
children 232cea484067
comparison
equal deleted inserted replaced
780:b44c1c6ce646 781:340708e8d54f
16 -- 16 --
17 -- a : Obj A 17 -- a : Obj A
18 -- U : A → Sets 18 -- U : A → Sets
19 -- U ⋍ Hom (a,-) 19 -- U ⋍ Hom (a,-)
20 -- 20 --
21
22 open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym )
21 23
22 -- A is localy small 24 -- A is localy small
23 postulate ≡←≈ : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y 25 postulate ≡←≈ : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y
24 26
25 import Relation.Binary.PropositionalEquality 27 import Relation.Binary.PropositionalEquality