Mercurial > hg > Members > kono > Proof > category
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)