Mercurial > hg > Members > kono > Proof > category
changeset 44:a626fdd909c3
f replacement
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 23 Jul 2013 01:27:43 +0900 |
| parents | 5506abc832c7 |
| children | 659b8a21caf7 |
| files | universal-mapping.agda |
| diffstat | 1 files changed, 16 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/universal-mapping.agda Tue Jul 23 00:29:17 2013 +0900 +++ b/universal-mapping.agda Tue Jul 23 01:27:43 2013 +0900 @@ -95,9 +95,24 @@ ≈⟨ 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 ] + 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') -> A [ A [ FMap U g o TMap η a' ] ≈ f ] -> B [ solution f ≈ g ] - uniqness a b f g = {!!} + uniqness a b f g k = let open ≈-Reasoning (B) in + begin + solution f + ≈⟨⟩ + 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 ] ) + ≈⟨ {!!} ⟩ + g + ∎ + --