Mercurial > hg > Members > kono > Proof > category
diff universal-mapping.agda @ 66:51f653bd9656
distr
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 25 Jul 2013 12:58:21 +0900 |
| parents | 83ff8d48fdca |
| children | 5f331dfc000b |
line wrap: on
line diff
--- 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 )