Mercurial > hg > Members > kono > Proof > category

diff 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
line wrap: on
line diff
--- a/HomReasoning.agda	Thu Mar 02 13:25:05 2017 +0900
+++ b/HomReasoning.agda	Thu Mar 02 14:58:40 2017 +0900
@@ -73,6 +73,8 @@
   sym :  {a b : Obj A } { f g : Hom A a b } →  f ≈ g  →  g ≈ f
   sym   =  IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A))
 
+  sym-hom = sym
+
   -- working on another cateogry
   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  ]
   idL1 A =  IsCategory.identityL (Category.isCategory A)