Mercurial > hg > Members > kono > Proof > category
diff nat.agda @ 66:51f653bd9656
distr
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 25 Jul 2013 12:58:21 +0900 |
| parents | 97eb12318048 |
| children | 829e0698f87f |
line wrap: on
line diff
--- a/nat.agda Thu Jul 25 12:13:10 2013 +0900 +++ b/nat.agda Thu Jul 25 12:58:21 2013 +0900 @@ -125,7 +125,7 @@ join k b f (TMap η a) ≈⟨ refl-hom ⟩ c [ TMap μ b o c [ FMap T f o (TMap η a) ] ] - ≈⟨ cdr ( IsNTrans.naturality ( isNTrans η )) ⟩ + ≈⟨ cdr ( nat η ) ⟩ c [ TMap μ b o c [ (TMap η ( FObj T b)) o f ] ] ≈⟨ IsCategory.associative (Category.isCategory c) ⟩ c [ c [ TMap μ b o (TMap η ( FObj T b)) ] o f ] @@ -170,7 +170,7 @@ ( ( ( TMap μ d o ( FMap T h o TMap μ c ) ) o FMap T g ) o f ) ≈⟨ car (car ( cdr ( begin ( FMap T h o TMap μ c ) - ≈⟨ nat A μ ⟩ + ≈⟨ nat μ ⟩ ( TMap μ (FObj T d) o FMap T (FMap T h) ) ∎ ))) ⟩ @@ -271,7 +271,7 @@ UεF A B U F ε = lemma11 ( Functor*Nat A {B} A U {( F ○ U) ○ F} {identityFunctor ○ F} ( Nat*Functor A {B} B { F ○ U} {identityFunctor} ε F) ) where lemma11 : NTrans A A ( U ○ ((F ○ U) ○ F )) ( U ○ (identityFunctor ○ F) ) - → NTrans A A (( U ○ F ) ○ ( U ○ F )) ( U ○ F ) + → NTrans A A (( U ○ F ) ○ ( U ○ F )) ( U ○ F ) lemma11 n = record { TMap = \a → TMap n a; isNTrans = record { naturality = IsNTrans.naturality ( isNTrans n ) }} Adj2Monad : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') @@ -300,11 +300,11 @@ TMap μ a o TMap μ ( FObj T a ) ≈⟨⟩ (FMap U (TMap ε ( FObj F a ))) o (FMap U (TMap ε ( FObj F ( FObj U (FObj F a ))))) - ≈⟨ sym (IsFunctor.distr (isFunctor U)) ⟩ + ≈⟨ sym (distr U) ⟩ FMap U (B [ TMap ε ( FObj F a ) o TMap ε ( FObj F ( FObj U (FObj F a ))) ] ) ≈⟨ (IsFunctor.≈-cong (isFunctor U)) (lemma-assoc1 ( TMap ε (FObj F a ))) ⟩ FMap U (B [ (TMap ε ( FObj F a )) o FMap F (FMap U (TMap ε ( FObj F a ))) ] ) - ≈⟨ IsFunctor.distr (isFunctor U) ⟩ + ≈⟨ distr U ⟩ (FMap U (TMap ε ( FObj F a ))) o FMap U (FMap F (FMap U (TMap ε ( FObj F a )))) ≈⟨⟩ TMap μ a o FMap T (TMap μ a) @@ -326,7 +326,7 @@ TMap μ a o (FMap T (TMap η a )) ≈⟨⟩ (FMap U (TMap ε ( FObj F a ))) o (FMap U ( FMap F (TMap η a ))) - ≈⟨ sym (IsFunctor.distr ( isFunctor U )) ⟩ + ≈⟨ sym (distr U ) ⟩ FMap U ( B [ (TMap ε ( FObj F a )) o ( FMap F (TMap η a )) ]) ≈⟨ (IsFunctor.≈-cong (isFunctor U)) (IsAdjunction.adjoint2 ( isAdjunction adj )) ⟩ FMap U ( id1 B (FObj F a) )