Mercurial > hg > Members > kono > Proof > category
changeset 358:cf9c0f12cec5
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 13 May 2015 13:28:16 +0900 |
| parents | 71c817f28bc6 |
| children | 6d803a4708bf |
| files | yoneda.agda |
| diffstat | 1 files changed, 5 insertions(+), 18 deletions(-) [+] |
line wrap: on
line diff
--- a/yoneda.agda Tue May 12 11:17:38 2015 +0900 +++ b/yoneda.agda Wed May 13 13:28:16 2015 +0900 @@ -68,28 +68,15 @@ ; identityR = refl ; o-resp-≈ = λ{a b c f g h i } → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ; associative = refl - } where + } where + open ≈-Reasoning (Sets {c₂}) sym1 : {a b : YObj A } {i j : YHom A a b } → i == j → j == i - sym1 {a} {b} {i} {j} eq {x} = let open ≈-Reasoning (Sets {c₂}) in begin - TMap j x - ≈⟨ sym eq ⟩ - TMap i x - ∎ + sym1 {a} {b} {i} {j} eq {x} = sym eq trans1 : {a b : YObj A } {i j k : YHom A a b} → i == j → j == k → i == k - trans1 {a} {b} {i} {j} {k} i=j j=k {x} = let open ≈-Reasoning (Sets {c₂}) in begin - TMap i x - ≈⟨ i=j ⟩ - TMap j x - ≈⟨ j=k ⟩ - TMap k x - ∎ + trans1 {a} {b} {i} {j} {k} i=j j=k {x} = trans-hom i=j j=k o-resp-≈ : {A₁ B C : YObj A} {f g : YHom A A₁ B} {h i : YHom A B C} → f == g → h == i → h + f == i + g - o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f=g h=i {x} = let open ≈-Reasoning (Sets {c₂}) in begin - (Sets {c₂}) [ TMap h x o TMap f x ] - ≈⟨ resp f=g h=i ⟩ - (Sets {c₂}) [ TMap i x o TMap g x ] - ∎ + o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f=g h=i {x} = resp f=g h=i SetsAop : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Category (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) (c₂ ⊔ c₁) SetsAop {_} {c₂} {_} A =