Mercurial > hg > Members > kono > Proof > category

comparison HomReasoning.agda @ 455:55a9b6177ed4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 02 Mar 2017 14:58:40 +0900
parents 3e44951b9bdb
children 961c236807f1
comparison
equal deleted inserted replaced
454:2f07f4dd9a6d 455:55a9b6177ed4
70 idR : {a b : Obj A } { f : Hom A a b } → f o id a ≈ f 70 idR : {a b : Obj A } { f : Hom A a b } → f o id a ≈ f
71 idR = IsCategory.identityR (Category.isCategory A) 71 idR = IsCategory.identityR (Category.isCategory A)
72 72
73 sym : {a b : Obj A } { f g : Hom A a b } → f ≈ g → g ≈ f 73 sym : {a b : Obj A } { f g : Hom A a b } → f ≈ g → g ≈ f
74 sym = IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A)) 74 sym = IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A))
75
76 sym-hom = sym
75 77
76 -- working on another cateogry 78 -- working on another cateogry
77 idL1 : { c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A b a } → A [ A [ Id {_} {_} {_} {A} a o f ] ≈ f ] 79 idL1 : { c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A b a } → A [ A [ Id {_} {_} {_} {A} a o f ] ≈ f ]
78 idL1 A = IsCategory.identityL (Category.isCategory A) 80 idL1 A = IsCategory.identityL (Category.isCategory A)
79 81