Mercurial > hg > Members > kono > Proof > category

comparison freyd.agda @ 350:c483374f542b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
349:5858351ac1b9 350:c483374f542b
34 field 34 field
35 initial : ∀( a : Obj A ) → Hom A i a 35 initial : ∀( a : Obj A ) → Hom A i a
36 uniqueness : ( a : Obj A ) → ( f : Hom A i a ) → A [ f ≈ initial a ] 36 uniqueness : ( a : Obj A ) → ( f : Hom A i a ) → A [ f ≈ initial a ]
37 37
38 38
39
39 -- A complete catagory has initial object if it has PreInitial-SmallFullSubcategory 40 -- A complete catagory has initial object if it has PreInitial-SmallFullSubcategory
40 41
41 open NTrans 42 open NTrans
42 open Limit 43 open Limit
43 open SmallFullSubcategory 44 open SmallFullSubcategory
55 } where 56 } where
56 initialArrow : ∀( a : Obj A ) → Hom A a0 a 57 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 ) ] 58 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 ] 59 lemma1 : (a : Obj A) (f : Hom A a0 a) → A [ f ≈ initialArrow a ]
59 lemma1 a f = let open ≈-Reasoning (A) in 60 lemma1 a f = let open ≈-Reasoning (A) in
61 sym (
60 begin 62 begin
63 initialArrow a
64 ≈⟨⟩
65 preinitialArrow PI {a} o limit (lim F) a0 (u a0)
66 ≈⟨ {!!} ⟩
61 f 67 f
62 ≈↑⟨ idR ⟩ 68 ∎ )
63 f o id1 A a0
64 ≈⟨ {!!} ⟩
65 ( preinitialArrow PI {a} o limit (lim F) a0 (u a0)) o id1 A a0
66 ≈⟨ idR ⟩
67 preinitialArrow PI {a} o limit (lim F) a0 (u a0)
68 ≈⟨⟩
69 initialArrow a
70 ∎
71 69