Mercurial > hg > Members > kono > Proof > category
changeset 27:d9c2386a18a8
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 12 Jul 2013 22:17:23 +0900 |
| parents | ad62c87659ef |
| children | 5289c46d8eef |
| files | nat.agda |
| diffstat | 1 files changed, 11 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/nat.agda Fri Jul 12 20:45:54 2013 +0900 +++ b/nat.agda Fri Jul 12 22:17:23 2013 +0900 @@ -181,6 +181,9 @@ infixr 2 _≈⟨_⟩_ infix 1 begin_ +------ If we have this, for example, as an axiom of a category, we can use ≡-Reasoning directly +-- ≈-to-≡ : {a b : Obj A } { x y : Hom A a b } -> A [ x ≈ y ] -> x ≡ y +-- ≈-to-≡ refl-hom = refl data _IsRelatedTo_ { a b : Obj A } ( x y : Hom A a b ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where @@ -290,7 +293,7 @@ A [ Trans μ d o A [ FMap T h o A [ Trans μ c o A [ FMap T g o f ] ] ] ] ≈⟨ cdr-eq ( Trans μ d ) ( cdr-eq ( FMap T h ) ( assoc )) ⟩ A [ Trans μ d o A [ FMap T h o A [ A [ Trans μ c o FMap T g ] o f ] ] ] - ≈⟨ assoc ⟩ --- A [ f x A [ g x h ] ] = A [ A [ f x g ] x h ] + ≈⟨ assoc ⟩ --- A [ f o A [ g o h ] ] = A [ A [ f o g ] o h ] A [ A [ Trans μ d o FMap T h ] o A [ A [ Trans μ c o FMap T g ] o f ] ] ≈⟨ assoc ⟩ A [ A [ A [ Trans μ d o FMap T h ] o A [ Trans μ c o FMap T g ] ] o f ] @@ -315,7 +318,13 @@ A [ A [ Trans μ d o A [ Trans μ ( FObj T d) o FMap T ( A [ FMap T h o g ] ) ] ] o f ] ≈⟨ car-eq f assoc ⟩ A [ A [ A [ Trans μ d o Trans μ ( FObj T d) ] o FMap T ( A [ FMap T h o g ] ) ] o f ] - ≈⟨ car-eq f ( car-eq (FMap T ( A [ FMap T h o g ] )) ( IsMonad.assoc ( isMonad m ))) ⟩ + ≈⟨ car-eq f ( car-eq (FMap T ( A [ FMap T h o g ] )) ( + begin + A [ Trans μ d o Trans μ (FObj T d) ] + ≈⟨ IsMonad.assoc ( isMonad m) ⟩ + A [ Trans μ d o FMap T (Trans μ d) ] + ∎ + )) ⟩ A [ A [ A [ Trans μ d o FMap T ( Trans μ d) ] o FMap T ( A [ FMap T h o g ] ) ] o f ] ≈⟨ car-eq f (sym assoc) ⟩ A [ A [ Trans μ d o A [ FMap T ( Trans μ d ) o FMap T ( A [ FMap T h o g ] ) ] ] o f ]