diff HomReasoning.agda @ 787:ca5eba647990

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 18 Apr 2019 20:07:22 +0900
parents 340708e8d54f
children dca4b29553cb
line wrap: on
line diff
--- a/HomReasoning.agda	Thu Apr 18 10:00:20 2019 +0900
+++ b/HomReasoning.agda	Thu Apr 18 20:07:22 2019 +0900
@@ -54,11 +54,19 @@
 
   car : {a b c : Obj A } {x y : Hom A a b } { f : Hom A c a } →
           x ≈ y  → ( x o f ) ≈ ( y  o f )
-  car {f} eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( refl-hom  ) eq
+  car  eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( refl-hom  ) eq
+
+  car1 : { c₁ c₂ ℓ : Level}  (A : Category c₁ c₂ ℓ) {a b c : Obj A } {x y : Hom A a b } { f : Hom A c a } →
+          A [ x ≈ y ] → A [ A [  x o f ] ≈ A [  y  o f  ] ]
+  car1 A  eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory A ))  ) eq
 
   cdr : {a b c : Obj A } {x y : Hom A a b } { f : Hom A b c } →
           x ≈ y  →  f o x  ≈  f  o y 
-  cdr {f} eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (refl-hom  ) 
+  cdr eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (refl-hom  ) 
+
+  cdr1 : { c₁ c₂ ℓ : Level}  (A : Category c₁ c₂ ℓ) {a b c : Obj A } {x y : Hom A a b } { f : Hom A b c } →
+          A [ x ≈ y ] →  A [ A [ f o x ]  ≈  A [ f  o y  ] ]
+  cdr1 A eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory A ))  ) 
 
   id :  (a  : Obj A ) →  Hom A a a
   id a =  (Id {_} {_} {_} {A} a)