Mercurial > hg > Members > kono > Proof > category
diff HomReasoning.agda @ 781:340708e8d54f
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 | 984518c56e96 |
| children | ca5eba647990 |
line wrap: on
line diff
--- a/HomReasoning.agda Mon Oct 08 16:48:27 2018 +0900 +++ b/HomReasoning.agda Fri Mar 08 17:46:59 2019 +0900 @@ -6,7 +6,6 @@ open import Level open Functor - -- F(f) -- F(a) ---→ F(b) -- | | @@ -82,8 +81,9 @@ idR1 : { c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b } → A [ A [ f o Id {_} {_} {_} {A} a ] ≈ f ] idR1 A = IsCategory.identityR (Category.isCategory A) + open import Relation.Binary.PropositionalEquality using ( _≡_ ) ≈←≡ : {a b : Obj A } { x y : Hom A a b } → (x≈y : x ≡ y ) → x ≈ y - ≈←≡ refl = refl-hom + ≈←≡ _≡_.refl = refl-hom -- Ho← to prove this? -- ≡←≈ : {a b : Obj A } { x y : Hom A a b } → (x≈y : x ≈ y ) → x ≡ y @@ -91,7 +91,7 @@ ≡-cong : { c₁′ c₂′ ℓ′ : Level} {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A } → (f : Hom B x y → Hom A x' y' ) → a ≡ b → f a ≈ f b - ≡-cong f refl = ≈←≡ refl + ≡-cong f _≡_.refl = ≈←≡ _≡_.refl -- cong-≈ : { c₁′ c₂′ ℓ′ : Level} {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A } → -- B [ a ≈ b ] → (f : Hom B x y → Hom A x' y' ) → f a ≈ f b