Mercurial > hg > Members > kono > Proof > category

changeset 209:4e138cc953f3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
equalizer difinition
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 02 Sep 2013 21:59:37 +0900
parents a1e5d2a3d3bd
children 51c57efe89b9
files equalizer.agda
diffstat 1 files changed, 25 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/equalizer.agda	Mon Sep 02 17:13:14 2013 +0900
+++ b/equalizer.agda	Mon Sep 02 21:59:37 2013 +0900
@@ -21,33 +21,39 @@
 open import HomReasoning
 open import cat-utility
 
-record Equalizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a b : Obj A} (f g : Hom A a b) : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
+record Equalizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {c a b : Obj A} (f g : Hom A a b)  : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
    field
-      equalizer : {c d : Obj A} (e : Hom  A c a) (h : Hom A d a) →  Hom A d c 
-      equalize : {c d : Obj A} (e : Hom  A c a) (h : Hom A d a) →
-           A [ A [ A [ f  o  e ] o equalizer e h ]  ≈ A [ g  o h ] ]
-      uniqueness : {c d : Obj A} (e : Hom  A c a) (h : Hom A d a) ( k : Hom A d c ) → 
-           A [ A [ A [ f  o  e ] o k ]  ≈ A [ g  o h ] ] → A [ equalizer e h  ≈ k ]
+      e : Hom A c a 
+      ef=eg : A [ A [ f  o  e ] ≈ A [ g  o e ] ]
+      k : {d : Obj A}  (h : Hom A d a) → A [ A [ f  o  h ] ≈ A [ g  o h ] ] → Hom A d c
+      ke=h : {d : Obj A}  → ∀ {h : Hom A d a} →  (eq : A [ A [ f  o  h ] ≈ A [ g  o h ] ] ) →  A [ A [ e  o k {d} h eq ] ≈ h ]
+      uniqueness : {d : Obj A} →  ∀ {h : Hom A d a} →  (eq : A [ A [ f  o  h ] ≈ A [ g  o h ] ] ) →  {k' : Hom A d c } → A [ A [ e  o k' ] ≈ h ] →
+                       A [ k {d} h eq  ≈ k' ]
+   equalizer : Hom A c a
+   equalizer = e
 
-record EqEqualizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a b : Obj A} (f g : Hom A a b) : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
+record EqEqualizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {c a b : Obj A} (f g : Hom A a b) : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
    field
-      α : {e a b : Obj A}  → (f : Hom A a b) → (g : Hom A a b ) →  Hom A e a
-      γ : {c d e a b : Obj A}  → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) →  Hom A c e 
-      δ : {e a b : Obj A}  → (f : Hom A a b) → Hom A a e 
-      b1 :  {e : Obj A} → A [ A [ f  o α {e} f g ] ≈ A [ g  o α {e} f g ] ]
-      b2 :  {c d : Obj A } → {h : Hom A d a } → A [ A [ α {c} f g o γ {c} f g h ] ≈ A [ h  o α  (A [ f o h ]) (A [ g o h ]) ] ]
-      b3 :  {e : Obj A} → A [ A [ α {e} f f o δ {e} f ] ≈ id1 A a ]
+      α : {e a : Obj A } → (f : Hom A a b) → (g : Hom A a b ) →  Hom A e a
+      γ : {d e a b : Obj A}  → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) →  Hom A c e 
+      δ : {a b : Obj A}  → (f : Hom A a b) → Hom A a c 
+      b1 : {e : Obj A } →  A [ A [ f  o α {e} {a} f g ] ≈ A [ g  o α {e} {a} f g ] ]
+      b2 :  {e d : Obj A } → {h : Hom A d a } → A [ A [ α {e} f g o γ f g h ] ≈ A [ h  o α {c} (A [ f o h ]) (A [ g o h ]) ] ]
+      b3 :  {e : Obj A} → A [ A [ α f f o δ f ] ≈ id1 A a ]
       -- b4 :  {c d : Obj A } {k : Hom A c a} → A [ β f g ( A [ α f g o  k ] ) ≈ k ]
-      b4 :  {c d : Obj A } {k : Hom A c a} → A [ A [ γ f g ( A [ α f g o  k ] ) o δ {c} (A [ f o A [ α f g o  k ] ] ) ] ≈ k ]
+      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 ] ] ) ] ≈ k ]
    --  A [ α f g o β f g h ] ≈ h
    β : { d e a b : Obj A}  → (f : Hom A a b) → (g : Hom A a b ) →  (h : Hom A d a ) → Hom A d e
    β {d} f g h =  A [ γ f g h o δ {d} (A [ f o h ]) ] 
 
-lemma-equ1 :  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a b : Obj A} (f g : Hom A a b)  → Equalizer A f g → EqEqualizer A f g
-lemma-equ1  A {a} {b} f g eqa = record {
-      α = {!!} ;
-      γ = {!!} ;
-      δ = {!!} ;
+open Equalizer
+open EqEqualizer
+
+lemma-equ1 :  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a b c : Obj A} (f g : Hom A a b)  → Equalizer A {c} f g → EqEqualizer A {c} f g
+lemma-equ1  A {a} {b} {c} f g eqa = record {
+      α = λ {e'} {a} f g →  ? ; -- e' -> c  c -> a,  Hom A e' a
+      γ = λ {d} {e} {a} {b} f g h → {!!} ;  -- Hom A c e
+      δ =  λ {a} {b} f → {!!} ; -- Hom A a c
       b1 = {!!} ;
       b2 = {!!} ;
       b3 = {!!} ;