Mercurial > hg > Members > kono > Proof > category

comparison equalizer.agda @ 217:306f07bece85

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add equalizer+h
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 04 Sep 2013 12:13:27 +0900
parents 0135419f375c
children 749a1ecbc0b5
comparison
equal deleted inserted replaced
216:0135419f375c 217:306f07bece85
46 β {d} {e} {a} {b} f g h = A [ γ {a} {b} {c} f g h o δ (A [ f o h ]) ] 46 β {d} {e} {a} {b} f g h = A [ γ {a} {b} {c} f g h o δ (A [ f o h ]) ]
47 47
48 open Equalizer 48 open Equalizer
49 open EqEqualizer 49 open EqEqualizer
50 50
51 -- Equalizer is unique up to iso
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 )
54 → Hom A c c' --- != id1 A c
55 equalizer-iso {c} eqa eqa' = k eqa' (e eqa) (ef=eg eqa)
56
57 -- e eqa f g f
58 -- c ----------> a ------->b
59 -- ---> d --->
60 -- i h
61
62 equalizer+h : {a b c d : Obj A } {f g : Hom A a b } ( eqa : Equalizer A {c} f g) (i : Hom A c d ) → (h : Hom A d a )
63 → A [ A [ h o i ] ≈ e eqa ]
64 → Equalizer A {c} (A [ f o h ]) (A [ g o h ] )
65 equalizer+h {a} {b} {c} {d} {f} {g} eqa i h eq = record {
66 e = i ; -- Hom A a d
67 ef=eg = ef=eg1 ;
68 k = λ j eq' → k eqa (A [ h o j ]) (fhj=ghj j eq' ) ;
69 ek=h = ek=h1 ;
70 uniqueness = uniqueness1
71 } where
72 fhj=ghj : {d' : Obj A } → (j : Hom A d' d ) →
73 A [ A [ A [ f o h ] o j ] ≈ A [ A [ g o h ] o j ] ] →
74 A [ A [ f o A [ h o j ] ] ≈ A [ g o A [ h o j ] ] ]
75 fhj=ghj j eq' = let open ≈-Reasoning (A) in
76 begin
77 f o ( h o j )
78 ≈⟨ assoc ⟩
79 (f o h ) o j
80 ≈⟨ eq' ⟩
81 (g o h ) o j
82 ≈↑⟨ assoc ⟩
83 g o ( h o j )
84 ∎
85 ef=eg1 : A [ A [ A [ f o h ] o i ] ≈ A [ A [ g o h ] o i ] ]
86 ef=eg1 = let open ≈-Reasoning (A) in
87 begin
88 ( f o h ) o i
89 ≈↑⟨ assoc ⟩
90 f o (h o i )
91 ≈⟨ cdr eq ⟩
92 f o (e eqa)
93 ≈⟨ ef=eg eqa ⟩
94 g o (e eqa)
95 ≈↑⟨ cdr eq ⟩
96 g o (h o i )
97 ≈⟨ assoc ⟩
98 ( g o h ) o i
99 ∎
100 ek=h1 : {d' : Obj A} {h' : Hom A d' d} {eq' : A [ A [ A [ f o h ] o h' ] ≈ A [ A [ g o h ] o h' ] ]} →
101 A [ A [ i o k eqa (A [ h o h' ]) (fhj=ghj h' eq') ] ≈ h' ]
102 ek=h1 {d'} {h'} {eq'} = let open ≈-Reasoning (A) in
103 begin
104 i o k eqa (h o h' ) (fhj=ghj h' eq')
105 ≈⟨ {!!} ⟩
106 h'
107 ∎
108 uniqueness1 : {d' : Obj A} {h' : Hom A d' d} {eq' : A [ A [ A [ f o h ] o h' ] ≈ A [ A [ g o h ] o h' ] ]} {k' : Hom A d' c} →
109 A [ A [ i o k' ] ≈ h' ] → A [ k eqa (A [ h o h' ]) (fhj=ghj h' eq') ≈ k' ]
110 uniqueness1 {d'} {h'} {eq'} {k'} ik=h = let open ≈-Reasoning (A) in
111 begin
112 k eqa (A [ h o h' ]) (fhj=ghj h' eq')
113 ≈⟨ uniqueness eqa ( begin
114 e eqa o k'
115 ≈↑⟨ car eq ⟩
116 (h o i ) o k'
117 ≈↑⟨ assoc ⟩
118 h o (i o k')
119 ≈⟨ cdr ik=h ⟩
120 h o h'
121 ∎ ) ⟩
122 k'
123 ∎
51 124
52 lemma-equ1 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a b c : Obj A} (f g : Hom A a b) → 125 lemma-equ1 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a b c : Obj A} (f g : Hom A a b) →
53 ( {a b c : Obj A} → (f g : Hom A a b) → Equalizer A {c} f g ) → EqEqualizer A {c} f g 126 ( {a b c : Obj A} → (f g : Hom A a b) → Equalizer A {c} f g ) → EqEqualizer A {c} f g
54 lemma-equ1 A {a} {b} {c} f g eqa = record { 127 lemma-equ1 A {a} {b} {c} f g eqa = record {
55 α = λ f g → e (eqa f g ) ; -- Hom A c a 128 α = λ f g → e (eqa f g ) ; -- Hom A c a
69 -- | 142 -- |
70 -- d 143 -- d
71 -- 144 --
72 -- 145 --
73 -- e o id1 ≈ e → k e ≈ id 146 -- e o id1 ≈ e → k e ≈ id
74 ff-equal4 : A [ A [ e (eqa f g ) o (e (eqa (A [ f o e (eqa f g) ] ) (A [ g o e (eqa f g) ] ))) ] ≈ 147
75 e (eqa f g )
76 ] →
77 A [ k (eqa f g ) (e (eqa f g)) (ef=eg (eqa f g)) ≈ e (eqa (A [ f o e (eqa f g) ] ) (A [ g o e (eqa f g) ] )) ]
78 ff-equal4 eq = uniqueness (eqa f g) eq
79
80 ff-equal3 : A [ e (eqa (A [ f o e (eqa f g) ] ) (A [ g o e (eqa f g) ] ) ) ≈ k (eqa f g ) (e (eqa f g)) (ef=eg (eqa f g)) ]
81 ff-equal3 = let open ≈-Reasoning (A) in
82 begin
83 e (eqa (A [ f o e (eqa f g) ] ) (A [ g o e (eqa f g) ] ) )
84 ≈↑⟨ uniqueness (eqa f g) {!!} ⟩
85 k (eqa f g ) (e (eqa f g)) (ef=eg (eqa f g))
86 ∎
87 ff-equal2 : A [ k (eqa f g) (e (eqa f g)) (ef=eg (eqa f g)) ≈ id1 A a ]
88 ff-equal2 = let open ≈-Reasoning (A) in
89 begin
90 k (eqa f g) (e (eqa f g)) (ef=eg (eqa f g))
91 ≈⟨ uniqueness (eqa f g) idR ⟩
92 id1 A a
93 ∎
94 ff-equal1 : A [ e (eqa (A [ f o e (eqa f g) ] ) (A [ g o e (eqa f g) ] ) ) ≈ id1 A a ]
95 ff-equal1 = let open ≈-Reasoning (A) in
96 begin
97 e (eqa (f o e (eqa f g) ) (g o e (eqa f g) ))
98 ≈⟨ {!!} ⟩
99 id1 A a
100 ∎
101 ff-equal : {d : Obj A} {k₁ : Hom A d c} → A [ e (eqa (A [ f o A [ e (eqa f g) o k₁ ] ] ) (A [ f o A [ e (eqa f g) o k₁ ] ] ) ) ≈ id1 A d ]
102 ff-equal {d} {k₁} = let open ≈-Reasoning (A) in
103 begin
104 e (eqa (f o e (eqa f g) o k₁) (f o e (eqa f g) o k₁))
105 ≈⟨ {!!} ⟩
106 id1 A d
107 ∎
108 fg-equal : {d : Obj A} {k₁ : Hom A d c} → A [ e (eqa (A [ f o A [ e (eqa f g) o k₁ ] ] ) (A [ g o A [ e (eqa f g) o k₁ ] ] ) ) ≈ id1 A d ]
109 fg-equal = {!!}
110 lemma-equ2 : {a b : Obj A} (f : Hom A a b) → A [ A [ f o id1 A a ] ≈ A [ f o id1 A a ] ] 148 lemma-equ2 : {a b : Obj A} (f : Hom A a b) → A [ A [ f o id1 A a ] ≈ A [ f o id1 A a ] ]
111 lemma-equ2 f = let open ≈-Reasoning (A) in refl-hom 149 lemma-equ2 f = let open ≈-Reasoning (A) in refl-hom
112 lemma-equ3 : A [ A [ e (eqa f f) o k (eqa f f) (id1 A a) (lemma-equ2 f) ] ≈ id1 A a ] 150 lemma-equ3 : A [ A [ e (eqa f f) o k (eqa f f) (id1 A a) (lemma-equ2 f) ] ≈ id1 A a ]
113 lemma-equ3 = let open ≈-Reasoning (A) in 151 lemma-equ3 = let open ≈-Reasoning (A) in
114 begin 152 begin