Mercurial > hg > Members > kono > Proof > category
changeset 649:4d742e13fb7c
module introdued
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 04 Jul 2017 10:26:38 +0900 |
parents | 10f2057c8bff |
children | 449025d1327f |
files | freyd2.agda |
diffstat | 1 files changed, 33 insertions(+), 91 deletions(-) [+] |
line wrap: on
line diff
--- a/freyd2.agda Tue Jul 04 10:16:07 2017 +0900 +++ b/freyd2.agda Tue Jul 04 10:26:38 2017 +0900 @@ -380,128 +380,70 @@ (In : (b : Obj B) → HasInitialObject ( K B A b ↓ U) (i b) ) (LP : LimitPreserve A I B U ) where - tmap-η' : (y : Obj B) → Hom B y (FObj U (obj (i y))) - tmap-η' y = hom (i y) + tmap-η : (y : Obj B) → Hom B y (FObj U (obj (i y))) + tmap-η y = hom (i y) -tmap-η : {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) - (U : Functor A B ) - (i : (b : Obj B) → Obj ( K B A b ↓ U) ) - (y : Obj B) → Hom B y (FObj U (obj (i y))) -tmap-η A B U i y = hom (i y) - -objB : {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) - (U : Functor A B ) - (i : (b : Obj B) → Obj ( K B A b ↓ U) ) - (a b : Obj B) → ( f : Hom B a b ) → Obj ( K B A a ↓ U) -objB A B U i a b f = record { obj = obj (i b) ; hom = B [ tmap-η A B U i b o f ] } + objB : (a b : Obj B) → ( f : Hom B a b ) → Obj ( K B A a ↓ U) + objB a b f = record { obj = obj (i b) ; hom = B [ tmap-η b o f ] } -solution : {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) - (U : Functor A B ) - (i : (b : Obj B) → Obj ( K B A b ↓ U) ) - (In : (b : Obj B) → HasInitialObject ( K B A b ↓ U) (i b) ) - (a b : Obj B) → ( f : Hom B a b ) → CommaHom (K B A a) U (i a) (objB A B U i a b f ) -solution A B U i In a b f = initial (In a) (objB A B U i a b f ) + solution : (a b : Obj B) → ( f : Hom B a b ) → CommaHom (K B A a) U (i a) (objB a b f ) + solution a b f = initial (In a) (objB a b f ) -FunctorF : {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I ) - (U : Functor A B ) - (SFS : (b : Obj B) → SmallFullSubcategory ((K B A b) ↓ U) ) - (PI : (b : Obj B) → PreInitial (K B A b ↓ U) (SFSF (SFS b))) - ( i : (b : Obj B) → Obj ( K B A b ↓ U) ) - (In : (b : Obj B) → HasInitialObject ( K B A b ↓ U) (i b) ) - (LP : LimitPreserve A I B U ) - → Functor B A -FunctorF A B I comp U SFS PI i In LP = record { + F : Functor B A + F = record { FObj = λ b → obj (i b) - ; FMap = λ {x} {y} (f : Hom B x y ) → arrow ( initial (In x) (objB A B U i x y f)) - ; isFunctor = record { + ; FMap = λ {x} {y} (f : Hom B x y ) → arrow ( initial (In x) (objB x y f)) + ; isFunctor = record { identity = {!!} ; distr = {!!} -- λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ; ; ≈-cong = {!!} -- λ eq → extensionality A ( λ x → lemma-y-obj3 x eq ) } - } where - identity1 : {a : Obj B} → A [ arrow (initial (In a) (objB A B U i a a (Id a))) ≈ Id (obj (i a)) ] + } where + identity1 : {a : Obj B} → A [ arrow (initial (In a) (objB a a (id1 B a))) ≈ id1 A (obj (i a)) ] identity1 = {!!} distr1 : {a b c : Obj B} {f : Hom B a b} {g : Hom B b c} → - A [ arrow (initial (In a) (objB A B U i a c (B [ g o f ]))) ≈ - A [ arrow (initial (In b) (objB A B U i b c g)) o arrow (initial (In a) (objB A B U i a b f)) ] ] + A [ arrow (initial (In a) (objB a c (B [ g o f ]))) ≈ + A [ arrow (initial (In b) (objB b c g)) o arrow (initial (In a) (objB a b f)) ] ] distr1 = {!!} cong1 : {a : Obj B} {b : Obj B} {f g : Hom B a b} → - B [ f ≈ g ] → A [ arrow (initial (In a) (objB A B U i a b f)) ≈ - arrow (initial (In a) (objB A B U i a b g)) ] + B [ f ≈ g ] → A [ arrow (initial (In a) (objB a b f)) ≈ + arrow (initial (In a) (objB a b g)) ] cong1 = {!!} -nat-ε : {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I ) - (U : Functor A B ) - (SFS : (b : Obj B) → SmallFullSubcategory ((K B A b) ↓ U) ) - (PI : (b : Obj B) → PreInitial (K B A b ↓ U) (SFSF (SFS b))) - ( i : (b : Obj B) → Obj ( K B A b ↓ U) ) - (In : (b : Obj B) → HasInitialObject ( K B A b ↓ U) (i b) ) - (LP : LimitPreserve A I B U ) - → NTrans A A ( (FunctorF A B I comp U SFS PI i In LP) ○ U ) identityFunctor -nat-ε A B I comp U SFS PI i In LP = - record { + nat-ε : NTrans A A ( F ○ U ) identityFunctor + nat-ε = record { TMap = λ x → arrow ( initial (In (FObj U x)) (record { obj = x ; hom = id1 B (FObj U x) })) ; isNTrans = record { commute = {!!} } } where - F : Functor B A - F = FunctorF A B I comp U SFS PI i In LP comm1 : {a b : Obj A} {f : Hom A a b} → - A [ A [ FMap identityFunctor f o + 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 (FunctorF A B I comp U SFS PI i In LP ○ U) f ] ] + o FMap (F ○ U) f ] ] comm1 = {!!} -nat-η : {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I ) - (U : Functor A B ) - (SFS : (b : Obj B) → SmallFullSubcategory ((K B A b) ↓ U) ) - (PI : (b : Obj B) → PreInitial (K B A b ↓ U) (SFSF (SFS b))) - ( i : (b : Obj B) → Obj ( K B A b ↓ U) ) - (In : (b : Obj B) → HasInitialObject ( K B A b ↓ U) (i b) ) - (LP : LimitPreserve A I B U ) - → NTrans B B identityFunctor (U ○ (FunctorF A B I comp U SFS PI i In LP) ) -nat-η A B I comp U SFS PI i In LP = - record { TMap = λ y → tmap-η A B U i y ; isNTrans = record { commute = comm1 } } where - F : Functor B A - F = FunctorF A B I comp U SFS PI i In LP + 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 ○ FunctorF A B I comp U SFS PI i In LP) f o tmap-η A B U i a ] - ≈ B [ tmap-η A B U i b o f ] ] + → 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 B U i a + FMap (U ○ F) f o tmap-η a ≈⟨⟩ - FMap U ( arrow ( initial (In a) (objB A B U i a b f ))) o hom ( i a ) - ≈⟨ comm ( initial (In a) (objB A B U i a b f)) ⟩ - ( tmap-η A B U i b o f ) o FMap (K B A a) (arrow (initial (In a) (objB A B U i a b f))) + FMap U ( arrow ( initial (In a) (objB a b f ))) o hom ( i a ) + ≈⟨ comm ( initial (In a) (objB a b f)) ⟩ + ( tmap-η b o f ) o FMap (K B A a) (arrow (initial (In a) (objB a b f))) ≈⟨ idR ⟩ hom (i b ) o f ≈⟨⟩ - tmap-η A B U i b o f + tmap-η b o f ∎ -IsLeftAdjoint : {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I ) - (U : Functor A B ) - (SFS : (b : Obj B) → SmallFullSubcategory ((K B A b) ↓ U) ) - (PI : (b : Obj B) → PreInitial (K B A b ↓ U) (SFSF (SFS b))) - ( i : (b : Obj B) → Obj ( K B A b ↓ U) ) - (In : (b : Obj B) → HasInitialObject ( K B A b ↓ U) (i b) ) - (LP : LimitPreserve A I B U ) - → Adjunction B A U (FunctorF A B I comp U SFS PI i In LP) - (nat-η A B I comp U SFS PI i In LP) (nat-ε A B I comp U SFS PI i In LP) -IsLeftAdjoint A B I comp U SFS PI i In LP = record { isAdjunction = record { + FisLeftAdjoint : Adjunction B A U F nat-η nat-ε + FisLeftAdjoint = record { isAdjunction = record { adjoint1 = {!!} ; adjoint2 = {!!} } } where - F : Functor B A - F = FunctorF A B I comp U SFS PI i In LP - η : NTrans B B identityFunctor (U ○ F ) - η = nat-η A B I comp U SFS PI i In LP - ε : NTrans A A ( F ○ U ) identityFunctor - ε = nat-ε A B I comp U SFS PI i In LP - adjoint1 : {b : Obj A} → B [ B [ FMap U (TMap (nat-ε A B I comp U SFS PI i In LP) b) o - TMap (nat-η A B I comp U SFS PI i In LP) (FObj U b) ] ≈ id1 B (FObj U b) ] + adjoint1 : {b : Obj A} → B [ B [ FMap U (TMap nat-ε b) o TMap nat-η (FObj U b) ] ≈ id1 B (FObj U b) ] adjoint1 = {!!} - adjoint2 : {a : Obj B} → A [ A [ TMap (nat-ε A B I comp U SFS PI i In LP) - (FObj (FunctorF A B I comp U SFS PI i In LP) a) - o FMap (FunctorF A B I comp U SFS PI i In LP) (TMap (nat-η A B I comp U SFS PI i In LP) a) ] - ≈ id1 A (FObj (FunctorF A B I comp U SFS PI i In LP) a) ] + adjoint2 : {a : Obj B} → A [ A [ TMap nat-ε (FObj F a) o FMap F (TMap nat-η a) ] ≈ id1 A (FObj F a) ] adjoint2 = {!!}