Mercurial > hg > Members > kono > Proof > category

comparison HomReasoning.agda @ 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 84a150c980ce
comparison
equal deleted inserted replaced
66:51f653bd9656 67:e75436075bf0
71 idR = IsCategory.identityR (Category.isCategory A) 71 idR = IsCategory.identityR (Category.isCategory A)
72 72
73 sym : {a b : Obj A } { f g : Hom A a b } → f ≈ g → g ≈ f 73 sym : {a b : Obj A } { f g : Hom A a b } → f ≈ g → g ≈ f
74 sym = IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A)) 74 sym = IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A))
75 75
76 -- How to prove this?
77 -- cong-≈ : { c₁′ c₂′ ℓ′ : Level} {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A } →
78 -- B [ a ≈ b ] → (f : Hom B x y → Hom A x' y' ) → f a ≈ f b
79 -- cong-≈ refl f = refl-hom
80
76 assoc : {a b c d : Obj A } {f : Hom A c d} {g : Hom A b c} {h : Hom A a b} 81 assoc : {a b c d : Obj A } {f : Hom A c d} {g : Hom A b c} {h : Hom A a b}
77 → f o ( g o h ) ≈ ( f o g ) o h 82 → f o ( g o h ) ≈ ( f o g ) o h
78 assoc = IsCategory.associative (Category.isCategory A) 83 assoc = IsCategory.associative (Category.isCategory A)
79 84
80 distr : { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′} (T : Functor D A) → {a b c : Obj D} {g : Hom D b c} { f : Hom D a b } 85 distr : { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′} (T : Functor D A) → {a b c : Obj D} {g : Hom D b c} { f : Hom D a b }