Mercurial > hg > Members > kono > Proof > category
changeset 658:9242298cffa8
adjoint functor theorem done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 06 Jul 2017 13:50:45 +0900 |
| parents | 0d029674eb59 |
| children | 372205f40ab0 |
| files | freyd2.agda |
| diffstat | 1 files changed, 60 insertions(+), 6 deletions(-) [+] |
line wrap: on
line diff
--- a/freyd2.agda Thu Jul 06 12:22:54 2017 +0900 +++ b/freyd2.agda Thu Jul 06 13:50:45 2017 +0900 @@ -502,9 +502,12 @@ ≈⟨ car (distr U) ⟩ ( FMap U (FMap (identityFunctor {_} {_} {_} {A}) f) o FMap U (arrow (initial (In (FObj U a)) (record { obj = a ; hom = id1 B (FObj U a) })))) o (tmap-η (FObj U a)) - ≈⟨ {!!} ⟩ - FMap U f - ≈↑⟨ idR ⟩ + ≈↑⟨ assoc ⟩ + FMap U (FMap (identityFunctor {_} {_} {_} {A}) f) o (FMap U (arrow (initial (In (FObj U a)) + (record { obj = a ; hom = id1 B (FObj U a) }))) o tmap-η (FObj U a) ) + ≈⟨ cdr ( univ (id1 B (FObj U a))) ⟩ + FMap U (FMap (identityFunctor {_} {_} {_} {A}) f) o id1 B (FObj U a) + ≈⟨⟩ FMap U f o id1 B (FObj U a) ∎ lemma-nat2 : {a b : Obj A} {f : Hom A a b} → @@ -514,7 +517,23 @@ lemma-nat2 {a} {b} {f} = let open ≈-Reasoning B in begin FMap U (A [ arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f ] ) o tmap-η (FObj U a) - ≈⟨ {!!} ⟩ + ≈⟨ car (distr U) ⟩ + ( FMap U (arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) }))) + o FMap U ( FMap (F ○ U) f )) o tmap-η (FObj U a) + ≈↑⟨ assoc ⟩ + FMap U (arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) }))) + o ( FMap U ( FMap (F ○ U) f ) o tmap-η (FObj U a) ) + ≈⟨ cdr ( univ ( tmap-η (FObj U b) o FMap U f ) ) ⟩ + FMap U (arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) }))) + o ( tmap-η (FObj U b) o FMap U f ) + ≈⟨ assoc ⟩ + ( FMap U (arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) }))) + o tmap-η (FObj U b) ) o FMap U f + ≈⟨ car (univ (id1 B (FObj U b))) ⟩ + id1 B (FObj U b) o FMap U f + ≈⟨ idL ⟩ + FMap U f + ≈↑⟨ idR ⟩ FMap U f o id1 B (FObj U a) ∎ comm1 : {a b : Obj A} {f : Hom A a b} → @@ -551,6 +570,41 @@ ; adjoint2 = adjoint2 } } where adjoint1 : {b : Obj A} → B [ B [ FMap U (TMap nat-ε b) o TMap nat-η (FObj U b) ] ≈ id1 B (FObj U b) ] - adjoint1 = {!!} + adjoint1 {b} = let open ≈-Reasoning B in begin + FMap U (TMap nat-ε b) o TMap nat-η (FObj U b) + ≈⟨ univ (id1 B (FObj U b)) ⟩ + id1 B (FObj U b) + ∎ + adj2comm1 : {a : Obj B} → B [ B [ FMap U (A [ TMap nat-ε (FObj F a) o FMap F (TMap nat-η a) ]) o + tmap-η (FObj (identityFunctor {_} {_} {_} {B}) a) ] ≈ tmap-η a ] + adj2comm1 {a} = let open ≈-Reasoning B in begin + FMap U (A [ TMap nat-ε (FObj F a) o FMap F (TMap nat-η a) ]) o tmap-η a + ≈⟨ car (distr U) ⟩ + (FMap U (TMap nat-ε (FObj F a)) o FMap U (FMap F (TMap nat-η a) )) o tmap-η a + ≈↑⟨ assoc ⟩ + FMap U (TMap nat-ε (FObj F a)) o (FMap U (FMap F (TMap nat-η a) ) o tmap-η a ) + ≈⟨ cdr ( univ (tmap-η (FObj U (obj (i a))) o tmap-η a )) ⟩ + FMap U (TMap nat-ε (FObj F a)) o (tmap-η (FObj U (obj (i a))) o tmap-η a ) + ≈⟨ assoc ⟩ + ( FMap U (TMap nat-ε (FObj F a)) o tmap-η (FObj U (obj (i a)))) o tmap-η a + ≈⟨ car (univ (id1 B (FObj U (FObj F a)))) ⟩ + id1 B (FObj U (FObj F a)) o tmap-η a + ≈⟨ idL ⟩ + tmap-η a + ∎ + adj2comm2 : {a : Obj B} → B [ B [ FMap U (id1 A (FObj F a)) o tmap-η a ] ≈ tmap-η a ] + adj2comm2 {a} = let open ≈-Reasoning B in begin + FMap U (id1 A (FObj F a)) o tmap-η a + ≈⟨ car (IsFunctor.identity (isFunctor U)) ⟩ + id1 B (FObj U (obj (i a))) o tmap-η a + ≈⟨ idL ⟩ + tmap-η a + ∎ adjoint2 : {a : Obj B} → A [ A [ TMap nat-ε (FObj F a) o FMap F (TMap nat-η a) ] ≈ id1 A (FObj F a) ] - adjoint2 = {!!} + adjoint2 {a} = let open ≈-Reasoning A in begin + TMap nat-ε (FObj F a) o FMap F (TMap nat-η a) + ≈↑⟨ unique adj2comm1 ⟩ + arrow (solution ( tmap-η a ) ) + ≈⟨ unique adj2comm2 ⟩ + id1 A (FObj F a) + ∎