Mercurial > hg > Members > kono > Proof > category
changeset 66:51f653bd9656
distr
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 25 Jul 2013 12:58:21 +0900 |
| parents | a04219fa2e0a |
| children | e75436075bf0 |
| files | HomReasoning.agda cat-utility.agda nat.agda universal-mapping.agda |
| diffstat | 4 files changed, 21 insertions(+), 21 deletions(-) [+] |
line wrap: on
line diff
--- a/HomReasoning.agda Thu Jul 25 12:13:10 2013 +0900 +++ b/HomReasoning.agda Thu Jul 25 12:58:21 2013 +0900 @@ -77,15 +77,15 @@ → f o ( g o h ) ≈ ( f o g ) o h assoc = IsCategory.associative (Category.isCategory A) - distr : (T : Functor A A) → {a b c : Obj A} {g : Hom A b c} { f : Hom A a b } - → FMap T ( g o f ) ≈ FMap T g o FMap T f - distr T = IsFunctor.distr ( isFunctor T ) + 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 } + → FMap T ( D [ g o f ] ) ≈ FMap T g o FMap T f + distr {_} T = IsFunctor.distr ( isFunctor T ) open NTrans - nat : { c₁′ c₂′ ℓ′ : Level} (D : Category c₁′ c₂′ ℓ′) {a b : Obj D} {f : Hom D a b} {F G : Functor D A } + nat : { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′} {a b : Obj D} {f : Hom D a b} {F G : Functor D A } → (η : NTrans D A F G ) → FMap G f o TMap η a ≈ TMap η b o FMap F f - nat _ η = IsNTrans.naturality ( isNTrans η ) + nat {_} η = IsNTrans.naturality ( isNTrans η ) infixr 2 _∎
--- a/cat-utility.agda Thu Jul 25 12:13:10 2013 +0900 +++ b/cat-utility.agda Thu Jul 25 12:58:21 2013 +0900 @@ -90,11 +90,11 @@ naturality {a} {b} {f} = let open ≈-Reasoning (C) in begin (FMap F ( FMap H f )) o ( FMap F (TMap n a)) - ≈⟨ sym (IsFunctor.distr ( isFunctor F)) ⟩ + ≈⟨ sym (distr F) ⟩ FMap F ( B [ (FMap H f) o TMap n a ]) ≈⟨ IsFunctor.≈-cong (isFunctor F) ( IsNTrans.naturality ( isNTrans n) ) ⟩ FMap F ( B [ (TMap n b ) o FMap G f ] ) - ≈⟨ IsFunctor.distr ( isFunctor F) ⟩ + ≈⟨ distr F ⟩ (FMap F (TMap n b )) o (FMap F (FMap G f)) ∎
--- 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) )
--- a/universal-mapping.agda Thu Jul 25 12:13:10 2013 +0900 +++ b/universal-mapping.agda Thu Jul 25 12:58:21 2013 +0900 @@ -87,11 +87,11 @@ FMap U ( solution f) o TMap η a ≈⟨⟩ FMap U ( B [ TMap ε b o FMap F f ] ) o TMap η a - ≈⟨ car (IsFunctor.distr ( isFunctor U )) ⟩ + ≈⟨ car (distr U ) ⟩ ( (FMap U (TMap ε b)) o (FMap U ( FMap F f )) ) o TMap η a ≈⟨ sym assoc ⟩ (FMap U (TMap ε b)) o ((FMap U ( FMap F f )) o TMap η a ) - ≈⟨ cdr (nat A η) ⟩ + ≈⟨ cdr (nat η) ⟩ (FMap U (TMap ε b)) o ((TMap η (FObj U b )) o f ) ≈⟨ assoc ⟩ ((FMap U (TMap ε b)) o (TMap η (FObj U b))) o f @@ -113,11 +113,11 @@ TMap ε b o FMap F f ≈⟨ cdr (sym ( lemma1 a b f g k )) ⟩ TMap ε b o FMap F ( A [ FMap U g o TMap η a ] ) - ≈⟨ cdr (IsFunctor.distr ( isFunctor F )) ⟩ + ≈⟨ cdr (distr F ) ⟩ TMap ε b o ( FMap F ( FMap U g) o FMap F ( TMap η a ) ) ≈⟨ assoc ⟩ ( TMap ε b o FMap F ( FMap U g) ) o FMap F ( TMap η a ) - ≈⟨ sym ( car ( nat B ε )) ⟩ + ≈⟨ sym ( car ( nat ε )) ⟩ ( g o TMap ε ( FObj F a) ) o FMap F ( TMap η a ) ≈⟨ sym assoc ⟩ g o ( TMap ε ( FObj F a) o FMap F ( TMap η a ) ) @@ -182,7 +182,7 @@ lemma-distr2 a b c f g = let open ≈-Reasoning (A) in begin ( FMap U (B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b o f ]) ] ) ) o η a - ≈⟨ car (IsFunctor.distr ( isFunctor U )) ⟩ + ≈⟨ car (distr U ) ⟩ (( FMap U ((_* um) (A [ η c o g ])) o ( FMap U ((_* um)( A [ η b o f ])))) ) o η a ≈⟨ sym assoc ⟩ ( FMap U ((_* um) (A [ η c o g ])) o (( FMap U ((_* um)( A [ η b o f ])))) o η a ) @@ -253,7 +253,7 @@ lemma-nat1 a b f = let open ≈-Reasoning (A) in begin FMap U ( B [ (um *) (id1 A (FObj U b)) o ((um *) ( η (FObj U b) o FMap U f )) ] ) o η (FObj U a) - ≈⟨ car ( IsFunctor.distr ( isFunctor U ) ) ⟩ + ≈⟨ car ( distr U ) ⟩ ( FMap U ((um *) (id1 A (FObj U b))) o FMap U ((um *) ( η (FObj U b) o FMap U f )) ) o η (FObj U a) ≈⟨ sym assoc ⟩ FMap U ((um *) (id1 A (FObj U b))) o ( FMap U ((um *) ( η (FObj U b) o FMap U f ))) o η (FObj U a) @@ -273,7 +273,7 @@ lemma-nat2 a b f = let open ≈-Reasoning (A) in begin FMap U ( B [ f o ((um *) (id1 A (FObj U a ))) ]) o η (FObj U a) - ≈⟨ car ( IsFunctor.distr ( isFunctor U ) ) ⟩ + ≈⟨ car ( distr U ) ⟩ (FMap U f o FMap U ((um *) (id1 A (FObj U a )))) o η (FObj U a) ≈⟨ sym assoc ⟩ FMap U f o ( FMap U ((um *) (id1 A (FObj U a ))) o η (FObj U a) ) @@ -339,7 +339,7 @@ lemma-adj1 a = let open ≈-Reasoning (A) in begin FMap U ((B [((_* um) ( id1 A (FObj U ( FObj F a )))) o (_* um) (A [ η' (FObj U ( FObj F a )) o ( η' a ) ]) ])) o η' a - ≈⟨ car ( IsFunctor.distr ( isFunctor U)) ⟩ + ≈⟨ car (distr U) ⟩ (FMap U ((_* um) ( id1 A (FObj U ( FObj F a)))) o FMap U ((_* um) (A [ η' (FObj U ( FObj F a )) o ( η' a ) ]))) o η' a ≈⟨ sym assoc ⟩ FMap U ((_* um) ( id1 A (FObj U ( FObj F a)))) o ( FMap U ((_* um) (A [ η' (FObj U ( FObj F a )) o ( η' a ) ])) o η' a )