Members/kono/Proof/category: freyd.agda annotate

annotate freyd.agda @ 350:c483374f542b

try equalizer from limit

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Wed, 24 Dec 2014 12:00:16 +0900
parents	0d7fa6fc5979
children	9f014f34b988

rev	line source
304 bd7b3f3d1d4c Freyd Adjoint Functor Theorem Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	1 open import Category -- https://github.com/konn/category-agda
bd7b3f3d1d4c Freyd Adjoint Functor Theorem Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	2 open import Level
bd7b3f3d1d4c Freyd Adjoint Functor Theorem Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	3
bd7b3f3d1d4c Freyd Adjoint Functor Theorem Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	4 module freyd {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
bd7b3f3d1d4c Freyd Adjoint Functor Theorem Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	5 where
bd7b3f3d1d4c Freyd Adjoint Functor Theorem Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	6
307 9872bddec072 small full subcategory done. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 306 diff changeset	7 open import cat-utility
312 702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 311 diff changeset	8 open import HomReasoning
304 bd7b3f3d1d4c Freyd Adjoint Functor Theorem Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	9 open import Relation.Binary.Core
307 9872bddec072 small full subcategory done. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 306 diff changeset	10 open Functor
304 bd7b3f3d1d4c Freyd Adjoint Functor Theorem Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	11
311 cf278f4d0b32 on going... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 310 diff changeset	12 -- C is small full subcategory of A ( C is image of F )
304 bd7b3f3d1d4c Freyd Adjoint Functor Theorem Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	13
307 9872bddec072 small full subcategory done. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 306 diff changeset	14 record SmallFullSubcategory {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
9872bddec072 small full subcategory done. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 306 diff changeset	15 (F : Functor A A ) ( FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b )
9872bddec072 small full subcategory done. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 306 diff changeset	16 : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
306 92475fe5f59e Small Full Subcategory (underconstruction) Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 305 diff changeset	17 field
307 9872bddec072 small full subcategory done. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 306 diff changeset	18 ≈→≡ : {a b : Obj A } → { x y : Hom A (FObj F a) (FObj F b) } →
9872bddec072 small full subcategory done. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 306 diff changeset	19 (x≈y : A [ FMap F x ≈ FMap F y ]) → FMap F x ≡ FMap F y -- co-comain of FMap is local small
9872bddec072 small full subcategory done. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 306 diff changeset	20 full→ : { a b : Obj A } { x : Hom A (FObj F a) (FObj F b) } → A [ FMap F ( FMap← x ) ≈ x ]
9872bddec072 small full subcategory done. Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 306 diff changeset	21 full← : { a b : Obj A } { x : Hom A a b } → A [ FMap← ( FMap F x ) ≈ x ]
305 211f6bec9b4a subset Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 304 diff changeset	22
309 e213595b845e preinitial problem written Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 308 diff changeset	23 -- pre-initial
e213595b845e preinitial problem written Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 308 diff changeset	24
311 cf278f4d0b32 on going... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 310 diff changeset	25 record PreInitial {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
cf278f4d0b32 on going... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 310 diff changeset	26 (F : Functor A A ) : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
308 7f00cd09274c pre-initial Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 307 diff changeset	27 field
314 d1af69c4aaf8 on going... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 313 diff changeset	28 preinitialObj : ∀{ a : Obj A } → Obj A
d1af69c4aaf8 on going... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 313 diff changeset	29 preinitialArrow : ∀{ a : Obj A } → Hom A ( FObj F (preinitialObj {a} )) a
309 e213595b845e preinitial problem written Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 308 diff changeset	30
e213595b845e preinitial problem written Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 308 diff changeset	31 -- initial object
308 7f00cd09274c pre-initial Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 307 diff changeset	32
309 e213595b845e preinitial problem written Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 308 diff changeset	33 record HasInitialObject {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (i : Obj A) : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
e213595b845e preinitial problem written Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 308 diff changeset	34 field
314 d1af69c4aaf8 on going... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 313 diff changeset	35 initial : ∀( a : Obj A ) → Hom A i a
309 e213595b845e preinitial problem written Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 308 diff changeset	36 uniqueness : ( a : Obj A ) → ( f : Hom A i a ) → A [ f ≈ initial a ]
e213595b845e preinitial problem written Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 308 diff changeset	37
e213595b845e preinitial problem written Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 308 diff changeset	38
350 c483374f542b try equalizer from limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 315 diff changeset	39
315 0d7fa6fc5979 System T and System F Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 314 diff changeset	40 -- A complete catagory has initial object if it has PreInitial-SmallFullSubcategory
309 e213595b845e preinitial problem written Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 308 diff changeset	41
312 702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 311 diff changeset	42 open NTrans
702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 311 diff changeset	43 open Limit
313 d72730946ba5 ??? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 312 diff changeset	44 open SmallFullSubcategory
d72730946ba5 ??? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 312 diff changeset	45 open PreInitial
312 702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 311 diff changeset	46
309 e213595b845e preinitial problem written Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 308 diff changeset	47 initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
e213595b845e preinitial problem written Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 308 diff changeset	48 (F : Functor A A ) ( FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b )
312 702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 311 diff changeset	49 (lim : ( Γ : Functor A A ) → { a0 : Obj A } { u : NTrans A A ( K A A a0 ) Γ } → Limit A A Γ a0 u ) -- completeness
309 e213595b845e preinitial problem written Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 308 diff changeset	50 (SFS : SmallFullSubcategory A F FMap← ) →
313 d72730946ba5 ??? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 312 diff changeset	51 (PI : PreInitial A F ) → { a0 : Obj A } → { u : (a : Obj A) → NTrans A A (K A A a) F }
312 702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 311 diff changeset	52 → HasInitialObject A a0
702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 311 diff changeset	53 initialFromPreInitialFullSubcategory A F FMap← lim SFS PI {a0} {u} = record {
314 d1af69c4aaf8 on going... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 313 diff changeset	54 initial = initialArrow ;
312 702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 311 diff changeset	55 uniqueness = λ a f → lemma1 a f
702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 311 diff changeset	56 } where
314 d1af69c4aaf8 on going... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 313 diff changeset	57 initialArrow : ∀( a : Obj A ) → Hom A a0 a
d1af69c4aaf8 on going... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 313 diff changeset	58 initialArrow a = A [ preinitialArrow PI {a} o limit (lim F {FObj F (preinitialObj PI)} {u (FObj F (preinitialObj PI))} ) a0 (u a0 ) ]
d1af69c4aaf8 on going... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 313 diff changeset	59 lemma1 : (a : Obj A) (f : Hom A a0 a) → A [ f ≈ initialArrow a ]
312 702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 311 diff changeset	60 lemma1 a f = let open ≈-Reasoning (A) in
350 c483374f542b try equalizer from limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 315 diff changeset	61 sym (
312 702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 311 diff changeset	62 begin
350 c483374f542b try equalizer from limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 315 diff changeset	63 initialArrow a
c483374f542b try equalizer from limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 315 diff changeset	64 ≈⟨⟩
c483374f542b try equalizer from limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 315 diff changeset	65 preinitialArrow PI {a} o limit (lim F) a0 (u a0)
313 d72730946ba5 ??? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 312 diff changeset	66 ≈⟨ {!!} ⟩
350 c483374f542b try equalizer from limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 315 diff changeset	67 f
c483374f542b try equalizer from limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 315 diff changeset	68 ∎ )
312 702adc45704f is this right direction? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 311 diff changeset	69

Mercurial > hg > Members > kono > Proof > category

annotate freyd.agda @ 350:c483374f542b