Mercurial > hg > Members > kono > Proof > category
diff universal-mapping.agda @ 51:adc6bd3c9270
on going...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 23 Jul 2013 16:01:25 +0900 |
| parents | b518af3a9b07 |
| children | 0fc0dbda7b55 |
line wrap: on
line diff
--- a/universal-mapping.agda Tue Jul 23 10:27:24 2013 +0900 +++ b/universal-mapping.agda Tue Jul 23 16:01:25 2013 +0900 @@ -16,9 +16,9 @@ ( _* : { a : Obj A}{ b : Obj B} -> ( Hom A a (FObj U b) ) -> Hom B (F a ) b ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where field - universalMapping : (a' : Obj A) ( b' : Obj B ) -> { f : Hom A a' (FObj U b') } -> + universalMapping : {a' : Obj A} { b' : Obj B } -> { f : Hom A a' (FObj U b') } -> A [ A [ FMap U ( f * ) o η a' ] ≈ f ] - unique-universalMapping : (a' : Obj A) ( b' : Obj B ) -> ( f : Hom A a' (FObj U b') ) -> ( g : Hom B (F a') b') -> + uniquness : (a' : Obj A) ( b' : Obj B ) -> { f : Hom A a' (FObj U b') } -> { g : Hom B (F a') b' } -> A [ A [ FMap U g o η a' ] ≈ f ] -> B [ f * ≈ g ] record UniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') @@ -72,14 +72,14 @@ _* = solution ; isUniversalMapping = record { universalMapping = universalMapping; - unique-universalMapping = uniqness + uniquness = uniqness } } where solution : { a : Obj A} { b : Obj B} -> ( f : Hom A a (FObj U b) ) -> Hom B (FObj F a ) b solution {_} {b} f = B [ TMap ε b o FMap F f ] - universalMapping : (a' : Obj A) ( b' : Obj B ) -> { f : Hom A a' (FObj U b') } -> + universalMapping : {a' : Obj A} { b' : Obj B } -> { f : Hom A a' (FObj U b') } -> A [ A [ FMap U ( solution f) o TMap η a' ] ≈ f ] - universalMapping a b {f} = + universalMapping {a} {b} {f} = let open ≈-Reasoning (A) in begin FMap U ( solution f) o TMap η a @@ -102,9 +102,9 @@ A [ A [ FMap U g o TMap η a ] ≈ f ] -> B [ (FMap F (A [ FMap U g o TMap η a ] )) ≈ FMap F f ] lemma1 a b f g k = IsFunctor.≈-cong (isFunctor F) k - uniqness : (a' : Obj A) ( b' : Obj B ) -> ( f : Hom A a' (FObj U b') ) -> ( g : Hom B (FObj F a') b') -> + uniqness : (a' : Obj A) ( b' : Obj B ) -> { f : Hom A a' (FObj U b') } -> { g : Hom B (FObj F a') b'} -> A [ A [ FMap U g o TMap η a' ] ≈ f ] -> B [ solution f ≈ g ] - uniqness a b f g k = let open ≈-Reasoning (B) in + uniqness a b {f} {g} k = let open ≈-Reasoning (B) in begin solution f ≈⟨⟩ @@ -160,21 +160,19 @@ η a o id a ∎ lemma-id : {a : Obj A} → B [ ( (_* um) (A [ (η a) o (id1 A a)] )) ≈ (id1 B (F a)) ] - lemma-id {a} = ( IsUniversalMapping.unique-universalMapping ( isUniversalMapping um ) ) - a (F a) ((A [ (η a) o (id1 A a)] )) ((id1 B (F a))) lemma-id1 + lemma-id {a} = ( IsUniversalMapping.uniquness ( isUniversalMapping um ) ) a (F a) lemma-id1 lemma-cong2 : (a b : Obj A) (f g : Hom A a b) → A [ f ≈ g ] → A [ A [ FMap U ((_* um) (A [ η b o g ]) ) o η a ] ≈ A [ η b o f ] ] lemma-cong2 a b f g eq = let open ≈-Reasoning (A) in begin ( FMap U ((_* um) (A [ η b o g ]) )) o η a - ≈⟨ ( IsUniversalMapping.universalMapping ( isUniversalMapping um )) a (F b) ⟩ + ≈⟨ ( IsUniversalMapping.universalMapping ( isUniversalMapping um )) ⟩ η b o g ≈⟨ ( IsCategory.o-resp-≈ ( Category.isCategory A ) (sym eq) (refl-hom) ) ⟩ η b o f ∎ lemma-cong1 : (a b : Obj A) (f g : Hom A a b) → A [ f ≈ g ] → B [ (_* um) (A [ η b o f ] ) ≈ (_* um) (A [ η b o g ]) ] - lemma-cong1 a b f g eq = ( IsUniversalMapping.unique-universalMapping ( isUniversalMapping um ) ) - a (F b) (A [ η b o f ]) ((_* um) (A [ η b o g ])) ( lemma-cong2 a b f g eq ) + lemma-cong1 a b f g eq = ( IsUniversalMapping.uniquness ( isUniversalMapping um ) ) a (F b) ( lemma-cong2 a b f g eq ) lemma-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → B [ myFMap f ≈ myFMap g ] lemma-cong {a} {b} {f} {g} eq = lemma-cong1 a b f g eq lemma-distr2 : (a b c : Obj A) (f : Hom A a b) (g : Hom A b c) → @@ -186,19 +184,18 @@ (( 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 ) - ≈⟨ cdr ( ( IsUniversalMapping.universalMapping ( isUniversalMapping um )) a (F b)) ⟩ + ≈⟨ cdr ( IsUniversalMapping.universalMapping ( isUniversalMapping um )) ⟩ ( FMap U ((_* um) (A [ η c o g ])) o ( η b o f) ) ≈⟨ assoc ⟩ ( FMap U ((_* um) (A [ η c o g ])) o η b) o f - ≈⟨ car (( IsUniversalMapping.universalMapping ( isUniversalMapping um )) b (F c)) ⟩ + ≈⟨ car ( IsUniversalMapping.universalMapping ( isUniversalMapping um )) ⟩ ( η c o g ) o f ≈⟨ sym assoc ⟩ η c o ( g o f ) ∎ lemma-distr1 : (a b c : Obj A) (f : Hom A a b) (g : Hom A b c) → B [ (_* um) (A [ η c o A [ g o f ] ]) ≈ (B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b o f ]) ] )] - lemma-distr1 a b c f g = ( IsUniversalMapping.unique-universalMapping ( isUniversalMapping um ) a (F c) - (A [ η c o A [ g o f ] ]) ((B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b o f ]) ] )) ) (lemma-distr2 a b c f g ) + lemma-distr1 a b c f g = ( IsUniversalMapping.uniquness ( isUniversalMapping um ) a (F c)) (lemma-distr2 a b c f g ) lemma-distr : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → B [ myFMap (A [ g o f ]) ≈ (B [ myFMap g o myFMap f ] )] lemma-distr {a} {b} {c} {f} {g} = lemma-distr1 a b c f g myIsFunctor : IsFunctor A B F myFMap @@ -229,7 +226,7 @@ (FMap U (FMap F' f)) o ( η a ) ≈⟨⟩ (FMap U ((_* um) (A [ η b o f ]))) o ( η a ) - ≈⟨ (IsUniversalMapping.universalMapping ( isUniversalMapping um )) a ( F b ) ⟩ + ≈⟨ (IsUniversalMapping.universalMapping ( isUniversalMapping um )) ⟩ (η b ) o f ∎ myIsNTrans : IsNTrans A A identityFunctor ( U ○ F' ) η @@ -248,6 +245,27 @@ F' = FunctorF A B U F η um ε : ( b : Obj B ) -> Hom B ( FObj F' ( FObj U b) ) b ε b = (_* um) ( id1 A (FObj U b)) + lemma-nat1 : (a b : Obj B) (f : Hom B a b ) -> + A [ A [ FMap U ( B [ (um *) (id1 A (FObj U b)) o ((um *) (A [ η (FObj U b) o FMap U f ])) ] ) o η (FObj U a) ] + ≈ A [ FMap U f o id1 A (FObj U a) ] ] + 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 ) ) ⟩ + ( 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) + ≈⟨ cdr ((IsUniversalMapping.universalMapping ( isUniversalMapping um )) ) ⟩ + FMap U ((um *) (id1 A (FObj U b))) o ( η (FObj U b) o FMap U f ) + ≈⟨ assoc ⟩ + (FMap U ((um *) (id1 A (FObj U b))) o η (FObj U b)) o FMap U f + ≈⟨ car ((IsUniversalMapping.universalMapping ( isUniversalMapping um )) ) ⟩ + id1 A (FObj U b) o FMap U f + ≈⟨ idL ⟩ + FMap U f + ≈⟨ sym idR ⟩ + FMap U f o id (FObj U a) + ∎ naturality : {a b : Obj B} {f : Hom B a b } → B [ B [ f o (ε a) ] ≈ B [(ε b) o (FMap F' (FMap U f)) ] ] naturality {a} {b} {f} = let open ≈-Reasoning (B) in @@ -257,6 +275,8 @@ ε b o ((_* um) (A [ η (FObj U b) o (FMap U f) ])) ≈⟨⟩ ((_* um) ( id1 A (FObj U b))) o ((_* um) (A [ η (FObj U b) o (FMap U f) ])) + ≈⟨ sym ( ( IsUniversalMapping.uniquness ( isUniversalMapping um ) (FObj U a) b ) (lemma-nat1 a b f)) ⟩ + (_* um) ( A [ FMap U f o id1 A (FObj U a) ] ) ≈⟨ {!!} ⟩ f o ((_* um) ( id1 A (FObj U a))) ≈⟨⟩