Mercurial > hg > Members > kono > Proof > category

comparison equalizer.agda @ 219:2ae029454fb6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 04 Sep 2013 17:36:32 +0900
parents 749a1ecbc0b5
children 5d96be63053f
comparison
equal deleted inserted replaced
218:749a1ecbc0b5 219:2ae029454fb6
51 -- Equalizer is unique up to iso 51 -- Equalizer is unique up to iso
52 52
53 equalizer-iso : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' : Equalizer A {c'} f g ) 53 equalizer-iso : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' : Equalizer A {c'} f g )
54 → Hom A c c' --- != id1 A c 54 → Hom A c c' --- != id1 A c
55 equalizer-iso {c} eqa eqa' = k eqa' (e eqa) (ef=eg eqa) 55 equalizer-iso {c} eqa eqa' = k eqa' (e eqa) (ef=eg eqa)
56
57 equalizer-iso-eq : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' : Equalizer A {c'} f g ) → {eff : Equalizer A {c} f f}
58 → A [ A [ equalizer-iso eqa eqa' o equalizer-iso eqa' eqa ] ≈ id1 A c' ]
59 equalizer-iso-eq {c} {c'} {f} {g} eqa eqa' {eff} = let open ≈-Reasoning (A) in
60 begin
61 equalizer-iso eqa eqa' o equalizer-iso eqa' eqa
62 ≈⟨⟩
63 k eqa' (e eqa) (ef=eg eqa) o k eqa (e eqa') (ef=eg eqa')
64 ≈⟨ car (uniqueness eqa' {!!}) ⟩
65 {!!} o k eqa (e eqa') (ef=eg eqa')
66 ≈⟨ {!!} ⟩
67 id1 A c'
68 ∎
69
70 -- ke = e' k'e' = e → k k' = 1 , k' k = 1
71 -- ke = e'
72 -- k'ke = k'e' = e kk' = 1
73
74 -- x e = e -> x = id?
75
76 f1=g1 : { a b : Obj A } {f g : Hom A a b } → (eq : A [ f ≈ g ] ) → A [ A [ f o id1 A a ] ≈ A [ g o id1 A a ] ]
77 f1=g1 eq = let open ≈-Reasoning (A) in (resp refl-hom eq )
78
79
80 equalizer-eq-k : { a b : Obj A } {f g : Hom A a b } → (eq : A [ f ≈ g ] ) → ( eqa : Equalizer A {a} f g) →
81 A [ e eqa ≈ id1 A a ] →
82 A [ k eqa (id1 A a) (f1=g1 eq) ≈ id1 A a ]
83 equalizer-eq-k {a} {b} {f} {g} eq eqa e=1 = let open ≈-Reasoning (A) in
84 begin
85 k eqa (id1 A a) (f1=g1 eq)
86 ≈⟨ uniqueness eqa ( begin
87 e eqa o id1 A a
88 ≈⟨ idR ⟩
89 e eqa
90 ≈⟨ e=1 ⟩
91 id1 A a
92 ∎ )⟩
93 id1 A a
94 ∎
56 95
57 -- e eqa f g f 96 -- e eqa f g f
58 -- c ----------> a ------->b 97 -- c ----------> a ------->b
59 -- ^ ---> d ---> 98 -- ^ ---> d --->
60 -- | i h 99 -- | i h