Mercurial > hg > Members > kono > Proof > category
changeset 659:372205f40ab0
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 16 Jul 2017 14:05:18 +0900 |
| parents | 9242298cffa8 |
| children | b9358172faf2 |
| files | freyd1.agda freyd2.agda |
| diffstat | 2 files changed, 17 insertions(+), 185 deletions(-) [+] |
line wrap: on
line diff
--- a/freyd1.agda Thu Jul 06 13:50:45 2017 +0900 +++ b/freyd1.agda Sun Jul 16 14:05:18 2017 +0900 @@ -227,7 +227,7 @@ ≈↑⟨ assoc ⟩ hom ( FObj Γ i ) o ((FMap F ( TMap (t0 ( climit comp (FIA Γ))) i) ) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) ) - ≈↑⟨ cdr ( distr F ) ⟩ + ≈↑⟨ cdr ( distr F) ⟩ hom ( FObj Γ i ) o FMap F ( A [ TMap (t0 ( climit comp (FIA Γ))) i o limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t) ] ) ≈⟨ cdr ( fcong F ( t0f=t (isLimit (climit comp (FIA Γ))))) ⟩
--- a/freyd2.agda Thu Jul 06 13:50:45 2017 +0900 +++ b/freyd2.agda Sun Jul 16 14:05:18 2017 +0900 @@ -421,190 +421,22 @@ uniquness = unique }} - F : Functor B A - F = record { - FObj = λ b → obj (i b) - ; FMap = λ {x} {y} (f : Hom B x y ) → arrow (solution ( B [ tmap-η y o f ] )) - ; isFunctor = record { - identity = identity1 - ; distr = distr1 - ; ≈-cong = cong1 - } - } where - id1comm : {a : Obj B} → B [ B [ FMap U (arrow (initial (In a) (ηf a a (id1 B a)))) o hom (i a) ] - ≈ B [ hom (i a) o FMap (K B A a) (arrow (initial (In a) (ηf a a (id1 B a)))) ] ] - id1comm {a} = let open ≈-Reasoning B in begin - FMap U (arrow (initial (In a) (ηf a a (id1 B a)))) o hom (i a) - ≈⟨ comm (initial (In a) (ηf a a (id1 B a))) ⟩ - hom (ηf a a (id1 B a)) o FMap (K B A a) (arrow (initial (In a) (ηf a a (id1 B a)))) - ≈⟨ idR ⟩ - hom (ηf a a (id1 B a)) - ≈⟨⟩ - hom (i a) o id1 B a - ≈⟨ idR ⟩ - hom (i a) - ≈↑⟨ idR ⟩ - hom (i a) o FMap (K B A a) (arrow (initial (In a) (ηf a a (id1 B a)))) - ∎ - identity1 : {a : Obj B} → A [ arrow (initial (In a) (ηf a a (id1 B a))) ≈ id1 A (obj (i a)) ] - identity1 {a} = let open ≈-Reasoning A in begin - arrow (initial (In a) (ηf a a (id1 B a))) - ≈⟨ uniqueness (In a) (record { arrow = arrow (initial (In a) (ηf a a (id1 B a))); comm = id1comm }) ⟩ - arrow (initial (In a) (i a)) - ≈↑⟨ uniqueness (In a) (id1 ( K B A a ↓ U) (i a) ) ⟩ - id1 A (obj (i a)) - ∎ - distr1 : {a b c : Obj B} {f : Hom B a b} {g : Hom B b c} → - A [ arrow (initial (In a) (ηf a c (B [ g o f ]))) ≈ - A [ arrow (initial (In b) (ηf b c g)) o arrow (initial (In a) (ηf a b f)) ] ] - distr1 {a} {b} {c} {f} {g} = unique ( - let open ≈-Reasoning B in begin - FMap U (A [ arrow (initial (In b) (ηf b c g)) o arrow (initial (In a) (ηf a b f)) ] ) o tmap-η a - ≈⟨ car (IsFunctor.distr (isFunctor U )) ⟩ - ( FMap U (arrow (initial (In b) (ηf b c g))) o FMap U (arrow (initial (In a) (ηf a b f))) ) - o tmap-η a - ≈↑⟨ assoc ⟩ - FMap U (arrow (initial (In b) (ηf b c g))) o - (FMap U (arrow (initial (In a) (ηf a b f))) o tmap-η a ) - ≈⟨ cdr (univ ( tmap-η b o f )) ⟩ - FMap U (arrow (initial (In b) (ηf b c g))) o ( tmap-η b o f ) - ≈⟨ assoc ⟩ - (FMap U (arrow (initial (In b) (ηf b c g))) o tmap-η b ) o f - ≈⟨ car ( univ (tmap-η c o g )) ⟩ - (tmap-η c o g ) o f - ≈↑⟨ assoc ⟩ - tmap-η c o ( g o f ) - ∎ - ) - cong1 : {a : Obj B} {b : Obj B} {f g : Hom B a b} → - B [ f ≈ g ] → A [ arrow (initial (In a) (ηf a b f)) ≈ arrow (initial (In a) (ηf a b g)) ] - cong1 {a} {b} {f} {g} f≈g = unique ( - let open ≈-Reasoning B in begin - FMap U (arrow (initial (In a) (ηf a b g))) o tmap-η a - ≈⟨ univ ( tmap-η b o g ) ⟩ - tmap-η b o g - ≈↑⟨ cdr f≈g ⟩ - tmap-η b o f - ∎ - ) + -- Adjoint can be built as follows (same as univeral-mapping.agda ) + -- + -- F : Functor B A + -- F = record { + -- FObj = λ b → obj (i b) + -- ; FMap = λ {x} {y} (f : Hom B x y ) → arrow (solution ( B [ tmap-η y o f ] )) - nat-ε : NTrans A A (F ○ U) identityFunctor - nat-ε = record { - TMap = λ x → arrow ( solution (id1 B (FObj U x))) - ; isNTrans = record { commute = comm1 } } where - lemma-nat1 : {a b : Obj A} {f : Hom A a b} → - B [ B [ FMap U (A [ FMap (identityFunctor {_} {_} {_} {A}) f o arrow (initial (In (FObj U a)) - (record { obj = a ; hom = id1 B (FObj U a) })) ] ) o tmap-η (FObj U a) ] - ≈ B [ FMap U f o id1 B (FObj U a) ] ] - lemma-nat1 {a} {b} {f} = let open ≈-Reasoning B in begin - FMap U (A [ FMap (identityFunctor {_} {_} {_} {A}) f o arrow (initial (In (FObj U a)) - (record { obj = a ; hom = id1 B (FObj U a) })) ] ) o tmap-η (FObj U a) - ≈⟨ 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)) - ≈↑⟨ 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} → - B [ B [ 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) ] - ≈ B [ FMap U f o id1 B (FObj U a) ] ] - 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} → - A [ A [ FMap (identityFunctor {_} {_} {_} {A}) f o - arrow (initial (In (FObj U a)) (record { obj = a ; hom = id1 B (FObj U a) })) ] - ≈ A [ arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f ] ] - comm1 {a} {b} {f} = let open ≈-Reasoning A in begin - FMap (identityFunctor {_} {_} {_} {A}) f o - arrow (initial (In (FObj U a)) (record { obj = a ; hom = id1 B (FObj U a) })) - ≈↑⟨ unique lemma-nat1 ⟩ - arrow (initial (In (FObj U a)) (record { obj = b ; hom = B [ FMap U f o id1 B (FObj U a) ] })) - ≈⟨ unique lemma-nat2 ⟩ - arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f - ∎ + -- nat-ε : NTrans A A (F ○ U) identityFunctor + -- nat-ε = record { + -- TMap = λ x → arrow ( solution (id1 B (FObj U x))) - nat-η : NTrans B B identityFunctor (U ○ F) - nat-η = record { TMap = λ y → tmap-η y ; isNTrans = record { commute = comm1 } } where - comm1 : {a b : Obj B} {f : Hom B a b} → B [ B [ FMap (U ○ F) f o tmap-η a ] ≈ B [ tmap-η b o f ] ] - comm1 {a} {b} {f} = let open ≈-Reasoning B in begin - FMap (U ○ F) f o tmap-η a - ≈⟨⟩ - FMap U ( arrow ( initial (In a) (ηf a b f ))) o hom ( i a ) - ≈⟨ comm ( initial (In a) (ηf a b f)) ⟩ - ( tmap-η b o f ) o FMap (K B A a) (arrow (initial (In a) (ηf a b f))) - ≈⟨ idR ⟩ - hom (i b ) o f - ≈⟨⟩ - tmap-η b o f - ∎ + -- nat-η : NTrans B B identityFunctor (U ○ F) + -- nat-η = record { TMap = λ y → tmap-η y ; isNTrans = record { commute = comm1 } } where - FisLeftAdjoint : Adjunction B A U F nat-η nat-ε - FisLeftAdjoint = record { isAdjunction = record { - adjoint1 = adjoint1 - ; 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 {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 {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) - ∎ + -- FisLeftAdjoint : Adjunction B A U F nat-η nat-ε + -- FisLeftAdjoint = record { isAdjunction = record { + +-- end +