Mercurial > hg > Members > kono > Proof > category

changeset 67:e75436075bf0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
cong-hom ?
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 25 Jul 2013 13:08:49 +0900
parents 51f653bd9656
children 829e0698f87f
files HomReasoning.agda
diffstat 1 files changed, 5 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/HomReasoning.agda	Thu Jul 25 12:58:21 2013 +0900
+++ b/HomReasoning.agda	Thu Jul 25 13:08:49 2013 +0900
@@ -73,6 +73,11 @@
   sym :  {a b : Obj A } { f g : Hom A a b } →  f ≈ g  →  g ≈ f
   sym   =  IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A))
 
+-- How to prove this?
+--  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
+--  cong-≈ refl f = refl-hom
+
   assoc :   {a b c d : Obj A }  {f : Hom A c d}  {g : Hom A b c} {h : Hom A a b}
                                   →  f o ( g o h )  ≈ ( f o g ) o h
   assoc =  IsCategory.associative (Category.isCategory A)