Mercurial > hg > Members > kono > Proof > category

comparison equalizer.agda @ 213:f2faee0897c7

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 Tue, 03 Sep 2013 01:25:21 +0900
parents 8b3d3f69b725
children f8afdb9ed99a
comparison
equal deleted inserted replaced
212:8b3d3f69b725 213:f2faee0897c7
34 record EqEqualizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where 34 record EqEqualizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where
35 field 35 field
36 α : {a b c : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → Hom A c a 36 α : {a b c : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → Hom A c a
37 γ : {a b d : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → Hom A c d 37 γ : {a b d : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → Hom A c d
38 δ : {a b c : Obj A } → (f : Hom A a b) → Hom A a c 38 δ : {a b c : Obj A } → (f : Hom A a b) → Hom A a c
39 b1 : A [ A [ f o α f g ] ≈ A [ g o α f g ] ] 39 b1 : A [ A [ f o α {a} {b} {a} f g ] ≈ A [ g o α f g ] ]
40 b2 : {d : Obj A } → {h : Hom A d a } → A [ A [ ( α f g) o (γ f g h) ] ≈ A [ h o α (A [ f o h ]) (A [ g o h ]) ] ] 40 b2 : {d : Obj A } → {h : Hom A d a } → A [ A [ ( α f g) o (γ f g h) ] ≈ A [ h o α (A [ f o h ]) (A [ g o h ]) ] ]
41 b3 : {e : Obj A} → A [ A [ α f f o δ f ] ≈ id1 A a ] 41 b3 : A [ A [ α f f o δ {a} {b} {a} f ] ≈ id1 A a ]
42 -- b4 : {c d : Obj A } {k : Hom A c a} → A [ β f g ( A [ α f g o k ] ) ≈ k ] 42 -- b4 : {c d : Obj A } {k : Hom A c a} → A [ β f g ( A [ α f g o k ] ) ≈ k ]
43 b4 : {d : Obj A } {k : Hom A d c} → A [ A [ γ f g ( A [ α f g o k ] ) o δ (A [ f o A [ α f g o k ] ] ) ] ≈ ? ] 43 b4 : {d : Obj A } {k : Hom A d c} → A [ A [ γ f g ( A [ α f g o k ] ) o δ (A [ f o A [ α f g o k ] ] ) ] ≈ {!!} ]
44 -- A [ α f g o β f g h ] ≈ h 44 -- A [ α f g o β f g h ] ≈ h
45 -- β : { d e a b : Obj A} → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → Hom A a d 45 -- β : { d e a b : Obj A} → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → Hom A a d
46 -- β {d} {e} {a} {b} f g h = A [ γ {a} {b} {d} f g h o δ (A [ f o h ]) ] 46 -- β {d} {e} {a} {b} f g h = A [ γ {a} {b} {d} f g h o δ (A [ f o h ]) ]
47 47
48 open Equalizer 48 open Equalizer
51 lemma-equ1 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a b c : Obj A} (f g : Hom A a b) → 51 lemma-equ1 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a b c : Obj A} (f g : Hom A a b) →
52 ( {a b c : Obj A} → (f g : Hom A a b) → Equalizer A {c} f g ) → EqEqualizer A {c} f g 52 ( {a b c : Obj A} → (f g : Hom A a b) → Equalizer A {c} f g ) → EqEqualizer A {c} f g
53 lemma-equ1 A {a} {b} {c} f g eqa = record { 53 lemma-equ1 A {a} {b} {c} f g eqa = record {
54 α = λ f g → e (eqa f g ) ; -- Hom A c a 54 α = λ f g → e (eqa f g ) ; -- Hom A c a
55 γ = λ {a} {b} {d} f g h → ( k (eqa f g ) ( A [ h o (e ( eqa (A [ f o h ] ) (A [ g o h ] ))) ] ) (lemma-equ4 {a} {b} {d} f g h ) ) ; -- Hom A c d 55 γ = λ {a} {b} {d} f g h → ( k (eqa f g ) ( A [ h o (e ( eqa (A [ f o h ] ) (A [ g o h ] ))) ] ) (lemma-equ4 {a} {b} {d} f g h ) ) ; -- Hom A c d
56 δ = λ f → k (eqa f f) (id1 A (Category.dom A f)) (lemma-equ2 f); -- Hom A a c 56 δ = λ {a} f → k (eqa f f) (id1 A a) (lemma-equ2 f); -- Hom A a c
57 b1 = ef=eg (eqa f g) ; 57 b1 = ef=eg (eqa f g) ;
58 b2 = lemma-equ5 ; 58 b2 = lemma-equ5 ;
59 b3 = lemma-equ3 ; 59 b3 = lemma-equ3 ;
60 b4 = {!!} 60 b4 = {!!}
61 } where 61 } where
62 lemma-equ2 : {a b : Obj A} (f : Hom A a b) → A [ A [ f o id1 A a ] ≈ A [ f o id1 A a ] ] 62 lemma-equ2 : {a b : Obj A} (f : Hom A a b) → A [ A [ f o id1 A a ] ≈ A [ f o id1 A a ] ]
63 lemma-equ2 f = let open ≈-Reasoning (A) in refl-hom 63 lemma-equ2 f = let open ≈-Reasoning (A) in refl-hom
64 lemma-equ3 : {e' : Obj A} → A [ A [ e (eqa f f) o k (eqa f f) (id1 A a) (lemma-equ2 f) ] ≈ id1 A a ] 64 lemma-equ3 : A [ A [ e (eqa f f) o k (eqa f f) (id1 A a) (lemma-equ2 f) ] ≈ id1 A a ]
65 lemma-equ3 {e'} = let open ≈-Reasoning (A) in 65 lemma-equ3 = let open ≈-Reasoning (A) in
66 begin 66 begin
67 e (eqa f f) o k (eqa f f) (id1 A a) (lemma-equ2 f) 67 e (eqa f f) o k (eqa f f) (id1 A a) (lemma-equ2 f)
68 ≈⟨ ke=h (eqa f f ) (lemma-equ2 f) ⟩ 68 ≈⟨ ke=h (eqa f f ) (lemma-equ2 f) ⟩
69 id1 A a 69 id1 A a
70 ∎ 70 ∎