Mercurial > hg > Members > kono > Proof > category
diff HomReasoning.agda @ 420:3e44951b9bdb
refl in free-monoid trouble
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 24 Mar 2016 11:31:14 +0900 |
| parents | 8c72f5284bc8 |
| children | 55a9b6177ed4 |
line wrap: on
line diff
--- a/HomReasoning.agda Thu Mar 24 02:53:25 2016 +0900 +++ b/HomReasoning.agda Thu Mar 24 11:31:14 2016 +0900 @@ -87,8 +87,8 @@ -- ≈-≡ : {a b : Obj A } { x y : Hom A a b } → (x≈y : x ≈ y ) → x ≡ y -- ≈-≡ x≈y = irr x≈y ≡-cong : { c₁′ c₂′ ℓ′ : Level} {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A } → - a ≡ b → (f : Hom B x y → Hom A x' y' ) → f a ≈ f b - ≡-cong refl f = ≡-≈ refl + (f : Hom B x y → Hom A x' y' ) → a ≡ b → f a ≈ f b + ≡-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