Mercurial > hg > Members > kono > Proof > category
diff kleisli.agda @ 253:24e83b8b81be
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 11 Sep 2013 20:26:48 +0900 |
| parents | 3249aaddc405 |
| children | d6a6dd305da2 |
line wrap: on
line diff
--- a/kleisli.agda Mon Sep 09 16:15:09 2013 +0900 +++ b/kleisli.agda Wed Sep 11 20:26:48 2013 +0900 @@ -146,7 +146,7 @@ ( ( TMap μ d o FMap T h ) o ( (TMap μ c o FMap T g ) o f ) ) ≈⟨ assoc ⟩ ( ( ( TMap μ d o FMap T h ) o (TMap μ c o FMap T g ) ) o f ) - ≈⟨ car (sym assoc) ⟩ + ≈↑⟨ car assoc ⟩ ( ( TMap μ d o ( FMap T h o ( TMap μ c o FMap T g ) ) ) o f ) ≈⟨ car ( cdr (assoc) ) ⟩ ( ( TMap μ d o ( ( FMap T h o TMap μ c ) o FMap T g ) ) o f ) @@ -159,11 +159,11 @@ ∎ ))) ⟩ ( ( ( TMap μ d o ( TMap μ ( FObj T d) o FMap T ( FMap T h ) ) ) o FMap T g ) o f ) - ≈⟨ car (sym assoc) ⟩ + ≈↑⟨ car assoc ⟩ ( ( TMap μ d o ( ( TMap μ ( FObj T d) o FMap T ( FMap T h ) ) o FMap T g ) ) o f ) - ≈⟨ car ( cdr (sym assoc) ) ⟩ + ≈↑⟨ car ( cdr assoc ) ⟩ ( ( TMap μ d o ( TMap μ ( FObj T d) o ( FMap T ( FMap T h ) o FMap T g ) ) ) o f ) - ≈⟨ car ( cdr (cdr (sym (distr T )))) ⟩ + ≈↑⟨ car ( cdr (cdr (distr T ))) ⟩ ( ( TMap μ d o ( TMap μ ( FObj T d) o FMap T ( ( FMap T h o g ) ) ) ) o f ) ≈⟨ car assoc ⟩ ( ( ( TMap μ d o TMap μ ( FObj T d) ) o FMap T ( ( FMap T h o g ) ) ) o f ) @@ -175,11 +175,11 @@ ∎ )) ⟩ ( ( ( TMap μ d o FMap T ( TMap μ d) ) o FMap T ( ( FMap T h o g ) ) ) o f ) - ≈⟨ car (sym assoc) ⟩ + ≈↑⟨ car assoc ⟩ ( ( TMap μ d o ( FMap T ( TMap μ d ) o FMap T ( ( FMap T h o g ) ) ) ) o f ) - ≈⟨ sym assoc ⟩ + ≈↑⟨ assoc ⟩ ( TMap μ d o ( ( FMap T ( TMap μ d ) o FMap T ( ( FMap T h o g ) ) ) o f ) ) - ≈⟨ cdr ( car ( sym ( distr T ))) ⟩ + ≈↑⟨ cdr ( car ( distr T )) ⟩ ( TMap μ d o ( FMap T ( ( ( TMap μ d ) o ( FMap T h o g ) ) ) o f ) ) ≈⟨ refl-hom ⟩ join M ( ( TMap μ d o ( FMap T h o g ) ) ) f @@ -289,7 +289,7 @@ begin TMap μ (a) o FMap T (TMap η a) ≈⟨ IsMonad.unity2 (isMonad M) ⟩ - id1 A (FObj T a) + id (FObj T a) ∎ ≈-cong : {a b : Obj A} {f g : KHom a b} → A [ KMap f ≈ KMap g ] → A [ ufmap f ≈ ufmap g ] ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (A) in @@ -361,7 +361,7 @@ ≈⟨ car (sym (nat η)) ⟩ (FMap T g o TMap η (b)) o f ≈⟨ sym idL ⟩ - id1 A (FObj T c) o ((FMap T g o TMap η (b)) o f) + id (FObj T c) o ((FMap T g o TMap η (b)) o f) ≈⟨ sym (car (IsMonad.unity2 (isMonad M))) ⟩ (TMap μ c o FMap T (TMap η c)) o ((FMap T g o TMap η (b)) o f) ≈⟨ sym assoc ⟩ @@ -405,7 +405,7 @@ ≈⟨ assoc ⟩ (TMap μ (b) o FMap T (TMap η (b))) o FMap T f ≈⟨ car (IsMonad.unity2 (isMonad M)) ⟩ - id1 A (FObj T b) o FMap T f + id (FObj T b) o FMap T f ≈⟨ idL ⟩ FMap T f ∎ ) @@ -445,7 +445,7 @@ sym ( begin KMap (( tmap-ε b ) * ( FMap (F_T ○ U_T) f )) ≈⟨⟩ - TMap μ b o ( FMap T ( id1 A (FObj T b) ) o ( KMap (FMap (F_T ○ U_T) f ) )) + TMap μ b o ( FMap T ( id (FObj T b) ) o ( KMap (FMap (F_T ○ U_T) f ) )) ≈⟨ cdr ( cdr ( begin KMap (FMap (F_T ○ U_T) f ) @@ -455,19 +455,19 @@ TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f)) ∎ )) ⟩ - TMap μ b o ( FMap T ( id1 A (FObj T b) ) o (TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f)))) + TMap μ b o ( FMap T ( id (FObj T b) ) o (TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f)))) ≈⟨ cdr (car (IsFunctor.identity (isFunctor T))) ⟩ - TMap μ b o ( id1 A (FObj T (FObj T b) ) o (TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f)))) + TMap μ b o ( id (FObj T (FObj T b) ) o (TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f)))) ≈⟨ cdr idL ⟩ TMap μ b o (TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f))) ≈⟨ assoc ⟩ (TMap μ b o (TMap η (FObj T b))) o (TMap μ (b) o FMap T (KMap f)) ≈⟨ (car (IsMonad.unity1 (isMonad M))) ⟩ - id1 A (FObj T b) o (TMap μ (b) o FMap T (KMap f)) + id (FObj T b) o (TMap μ (b) o FMap T (KMap f)) ≈⟨ idL ⟩ TMap μ b o FMap T (KMap f) ≈⟨ cdr (sym idR) ⟩ - TMap μ b o ( FMap T (KMap f) o id1 A (FObj T a) ) + TMap μ b o ( FMap T (KMap f) o id (FObj T a) ) ≈⟨⟩ KMap (f * ( tmap-ε a )) ∎ ) @@ -516,9 +516,9 @@ sym ( begin FMap U_T ( TMap nat-ε ( FObj F_T x ) ) ≈⟨⟩ - TMap μ x o FMap T (id1 A (FObj T x) ) + TMap μ x o FMap T (id (FObj T x) ) ≈⟨ cdr (IsFunctor.identity (isFunctor T)) ⟩ - TMap μ x o id1 A (FObj T (FObj T x) ) + TMap μ x o id (FObj T (FObj T x) ) ≈⟨ idR ⟩ TMap μ x ∎ ) @@ -536,13 +536,13 @@ begin ( FMap U_T ( TMap nat-ε b)) o ( TMap nat-η ( FObj U_T b )) ≈⟨⟩ - (TMap μ (b) o FMap T (id1 A (FObj T b ))) o ( TMap η ( FObj T b )) + (TMap μ (b) o FMap T (id (FObj T b ))) o ( TMap η ( FObj T b )) ≈⟨ car ( cdr (IsFunctor.identity (isFunctor T))) ⟩ - (TMap μ (b) o (id1 A (FObj T (FObj T b )))) o ( TMap η ( FObj T b )) + (TMap μ (b) o (id (FObj T (FObj T b )))) o ( TMap η ( FObj T b )) ≈⟨ car idR ⟩ TMap μ (b) o ( TMap η ( FObj T b )) ≈⟨ IsMonad.unity1 (isMonad M) ⟩ - id1 A (FObj U_T b) + id (FObj U_T b) ∎ adjoint2 : {a : Obj A} → KleisliCategory [ KleisliCategory [ ( TMap nat-ε ( FObj F_T a )) o ( FMap F_T ( TMap nat-η a )) ] @@ -551,15 +551,15 @@ begin KMap (( TMap nat-ε ( FObj F_T a )) * ( FMap F_T ( TMap nat-η a )) ) ≈⟨⟩ - TMap μ a o (FMap T (id1 A (FObj T a) ) o ((TMap η (FObj T a)) o (TMap η a))) + TMap μ a o (FMap T (id (FObj T a) ) o ((TMap η (FObj T a)) o (TMap η a))) ≈⟨ cdr ( car ( IsFunctor.identity (isFunctor T))) ⟩ - TMap μ a o ((id1 A (FObj T (FObj T a) )) o ((TMap η (FObj T a)) o (TMap η a))) + TMap μ a o ((id (FObj T (FObj T a) )) o ((TMap η (FObj T a)) o (TMap η a))) ≈⟨ cdr ( idL ) ⟩ TMap μ a o ((TMap η (FObj T a)) o (TMap η a)) ≈⟨ assoc ⟩ (TMap μ a o (TMap η (FObj T a))) o (TMap η a) ≈⟨ car (IsMonad.unity1 (isMonad M)) ⟩ - id1 A (FObj T a) o (TMap η a) + id (FObj T a) o (TMap η a) ≈⟨ idL ⟩ TMap η a ≈⟨⟩