Mercurial > hg > Members > kono > Proof > category

comparison freyd.agda @ 436:ef37decef1ca

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
initialFullSubCategory
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 29 Aug 2016 17:02:03 +0900
parents 9f014f34b988
children 9be298a02c35
comparison
equal deleted inserted replaced
435:9f014f34b988 436:ef37decef1ca
14 record SmallFullSubcategory {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 14 record SmallFullSubcategory {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
15 (F : Functor A A ) ( FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b ) 15 (F : Functor A A ) ( FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b )
16 : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where 16 : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
17 field 17 field
18 ≈→≡ : {a b : Obj A } → { x y : Hom A (FObj F a) (FObj F b) } → 18 ≈→≡ : {a b : Obj A } → { x y : Hom A (FObj F a) (FObj F b) } →
19 (x≈y : A [ FMap F x ≈ FMap F y ]) → FMap F x ≡ FMap F y -- co-comain of FMap is local small 19 (x≈y : A [ FMap F x ≈ FMap F y ]) → FMap F x ≡ FMap F y -- codomain of FMap is local small
20 full→ : { a b : Obj A } { x : Hom A (FObj F a) (FObj F b) } → A [ FMap F ( FMap← x ) ≈ x ] 20 full→ : { a b : Obj A } { x : Hom A (FObj F a) (FObj F b) } → A [ FMap F ( FMap← x ) ≈ x ]
21 full← : { a b : Obj A } { x : Hom A a b } → A [ FMap← ( FMap F x ) ≈ x ]
22 21
23 -- pre-initial 22 -- pre-initial
24 23
25 record PreInitial {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 24 record PreInitial {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
26 (F : Functor A A ) : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where 25 (F : Functor A A ) : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
45 initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 44 initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
46 (F : Functor A A ) ( FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b ) 45 (F : Functor A A ) ( FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b )
47 (lim : ( Γ : Functor A A ) → { a0 : Obj A } { u : NTrans A A ( K A A a0 ) Γ } → Limit A A Γ a0 u ) -- completeness 46 (lim : ( Γ : Functor A A ) → { a0 : Obj A } { u : NTrans A A ( K A A a0 ) Γ } → Limit A A Γ a0 u ) -- completeness
48 ( equ : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → Equalizer A e f g ) 47 ( equ : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → Equalizer A e f g )
49 (SFS : SmallFullSubcategory A F FMap← ) → 48 (SFS : SmallFullSubcategory A F FMap← ) →
50 (PI : PreInitial A F ) → { a0 : Obj A } → { u : (a : Obj A) → NTrans A A (K A A a) F } 49 (PI : PreInitial A F ) → { a0 : Obj A } →
50 { u : (a : Obj A) → NTrans A A (K A A a) F } -- Does it exist?
51 → HasInitialObject A a0 51 → HasInitialObject A a0
52 initialFromPreInitialFullSubcategory A F FMap← lim equ SFS PI {a0} {u} = record { 52 initialFromPreInitialFullSubcategory A F FMap← lim equ SFS PI {a0} {u} = record {
53 initial = initialArrow ; 53 initial = initialArrow ;
54 uniqueness = λ a f → lemma1 a f 54 uniqueness = λ a f → lemma1 a f
55 } where 55 } where
56 initialArrow : ∀( a : Obj A ) → Hom A a0 a 56 initialArrow : ∀( a : Obj A ) → Hom A a0 a
57 initialArrow a = A [ preinitialArrow PI {a} o limit (lim F {FObj F (preinitialObj PI)} {u (FObj F (preinitialObj PI))} ) a0 (u a0 ) ] 57 initialArrow a = A [ preinitialArrow PI {a} o limit (lim F {FObj F (preinitialObj PI)} {u (FObj F (preinitialObj PI))} ) a0 (u a0 ) ]
58 lemma1 : (a : Obj A) (f : Hom A a0 a) → A [ f ≈ initialArrow a ] 58 equ-fi : { a c : Obj A} -> { p : Hom A c a0 } -> {f : Hom A a0 a} -> Equalizer A p ( A [ preinitialArrow PI {a} o limit (lim F) a0 (u a0) ] ) f
59 lemma1 a f = let open ≈-Reasoning (A) in 59 equ-fi {a} {c} {p} {f} = equ ( A [ preinitialArrow PI {a} o limit (lim F) a0 (u a0) ] ) f
60 sym ( 60 open Equalizer
61 begin 61 kfuc=1 : {k1 c : Obj A} -> A [ A [ equalizer (equ-fi {a0} {k1} {{!!}} {{!!}} ) o
62 initialArrow a 62 A [ preinitialArrow PI {k1} o TMap (u a0) (preinitialObj PI) ] ] ≈ id1 A a0 ]
63 ≈⟨⟩ 63 kfuc=1 {k1} {c} = {!!}
64 preinitialArrow PI {a} o limit (lim F) a0 (u a0)
65 ≈⟨ {!!} ⟩
66 f
67 ∎ )
68 -- if equalizer has right inverse, f = g 64 -- if equalizer has right inverse, f = g
69 lemma2 : (a b c : Obj A) ( f g : Hom A a b ) (e : Hom A c a ) (e' : Hom A a c ) ( equ : Equalizer A e f g ) (inv-e : A [ A [ e o e' ] ≈ id1 A a ] ) 65 lemma2 : (a b c : Obj A) ( f g : Hom A a b ) (e : Hom A c a ) (e' : Hom A a c ) ( equ : Equalizer A e f g ) (inv-e : A [ A [ e o e' ] ≈ id1 A a ] )
70 -> A [ f ≈ g ] 66 -> A [ f ≈ g ]
71 lemma2 a b c f g e e' equ inv-e = let open ≈-Reasoning (A) in 67 lemma2 a b c f g e e' equ inv-e = let open ≈-Reasoning (A) in
72 let open Equalizer in 68 let open Equalizer in
85 ≈⟨ cdr inv-e ⟩ 81 ≈⟨ cdr inv-e ⟩
86 g o id1 A a 82 g o id1 A a
87 ≈⟨ idR ⟩ 83 ≈⟨ idR ⟩
88 g 84 g
89 ∎ 85 ∎
86 lemma1 : (a : Obj A) (f : Hom A a0 a) → A [ f ≈ initialArrow a ]
87 lemma1 a f = let open ≈-Reasoning (A) in
88 sym (
89 begin
90 initialArrow a
91 ≈⟨⟩
92 preinitialArrow PI {a} o limit (lim F) a0 (u a0)
93 ≈⟨ lemma2 a0 a {!!} (A [ preinitialArrow PI {a} o limit (lim F) a0 (u a0) ]) f {!!} {!!} {!!} (kfuc=1 {{!!}} {{!!}} ) ⟩
94 f
95 ∎ )
90 96