Mercurial > hg > Members > kono > Proof > category
changeset 45:659b8a21caf7
uniq-univeralMapping from Adjunction
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 23 Jul 2013 01:45:56 +0900 |
| parents | a626fdd909c3 |
| children | 5d1b0fd2ad21 |
| files | universal-mapping.agda |
| diffstat | 1 files changed, 12 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/universal-mapping.agda Tue Jul 23 01:27:43 2013 +0900 +++ b/universal-mapping.agda Tue Jul 23 01:45:56 2013 +0900 @@ -95,7 +95,6 @@ ≈⟨ idL ⟩ f ∎ - open import Relation.Binary.Core lemma1 : (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 [ (FMap F (A [ FMap U g o TMap η a ] )) ≈ FMap F f ] @@ -107,14 +106,22 @@ solution f ≈⟨⟩ TMap ε b o FMap F f - ≈⟨ cdr (sym ( lemma1 a b f g k )) ⟩ + ≈⟨ 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 )) ⟩ + 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 ε )) ⟩ + ( g o TMap ε ( FObj F a) ) o FMap F ( TMap η a ) + ≈⟨ sym assoc ⟩ + g o ( TMap ε ( FObj F a) o FMap F ( TMap η a ) ) + ≈⟨ cdr ( IsAdjunction.adjoint2 ( isAdjunction adj )) ⟩ + g o id (FObj F a) + ≈⟨ idR ⟩ g ∎ - - -- -- -- Universal mapping yields Adjunction