Mercurial > hg > Members > kono > Proof > category
diff universal-mapping.agda @ 40:c34b1cfe9fdc
Adjunction to Universal Mapping end
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 22 Jul 2013 18:13:57 +0900 |
| parents | 77c3a5292a2f |
| children | e9fa5c95eff7 |
line wrap: on
line diff
--- a/universal-mapping.agda Mon Jul 22 17:51:08 2013 +0900 +++ b/universal-mapping.agda Mon Jul 22 18:13:57 2013 +0900 @@ -36,9 +36,9 @@ ( ε : NTrans B B ( F ○ U ) identityFunctor ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where field - adjoint1 : {a' : Obj A} { b' : Obj B } -> ( f : Hom A a' (FObj U b') ) -> + adjoint1 : { b' : Obj B } -> A [ A [ ( FMap U ( TMap ε b' )) o ( TMap η ( FObj U b' )) ] ≈ Id {_} {_} {_} {A} (FObj U b') ] - adjoint2 : {a' : Obj A} { b' : Obj B } -> ( f : Hom A a' (FObj U b') ) -> + adjoint2 : {a' : Obj A} -> B [ B [ ( TMap ε ( FObj F a' )) o ( FMap F ( TMap η a' )) ] ≈ Id {_} {_} {_} {B} (FObj F a') ] record Adjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') @@ -48,7 +48,7 @@ ( ε : NTrans B B ( F ○ U ) identityFunctor ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where field - isAdjection : IsAdjunction A B U F η ε + isAdjunction : IsAdjunction A B U F η ε open Adjunction open UniversalMapping @@ -82,7 +82,15 @@ FMap U ( B [ TMap ε b o FMap F f ] ) o TMap η a ≈⟨ car (IsFunctor.distr ( isFunctor 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 η) ⟩ + (FMap U (TMap ε b)) o ((TMap η (FObj U b )) o f ) + ≈⟨ assoc ⟩ + ((FMap U (TMap ε b)) o (TMap η (FObj U b))) o f + ≈⟨ car ( IsAdjunction.adjoint1 ( isAdjunction adj)) ⟩ + id (FObj U b) o f + ≈⟨ idL ⟩ f ∎