Mercurial > hg > Members > kono > Proof > category

changeset 251:40947f08bab6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
comment
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 09 Sep 2013 16:03:14 +0900
parents a1e2228c2a6b
children e0835b8dd51b
files equalizer.agda
diffstat 1 files changed, 13 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/equalizer.agda	Mon Sep 09 15:56:34 2013 +0900
+++ b/equalizer.agda	Mon Sep 09 16:03:14 2013 +0900
@@ -31,7 +31,7 @@
    equalizer = e
 
 --
--- Flat Equational Definition of Equalizer
+-- Burroni's Flat Equational Definition of Equalizer
 --
 record Burroni { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {c a b : Obj A} (f g : Hom A a b) (e : Hom A c a) : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
    field
@@ -79,6 +79,7 @@
                   g o ( e  o h )
              ∎
 
+--------------------------------
 --
 --
 --   An isomorphic arrow c' to c makes another equalizer
@@ -143,6 +144,7 @@
                    j
              ∎
 
+--------------------------------
 --
 -- If we have two equalizers on c and c', there are isomorphic pair h, h'
 --
@@ -173,10 +175,10 @@
      --                                           h =   j e f   -> j = j'
      --
 
-c-iso→' : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' :  Equalizer A e' f g )
+e←e' : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' :  Equalizer A e' f g )
       →  ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ])  (A [ g o e' ]) )
       →  A [ A [ e' o c-iso-l eqa eqa' keqa ]  ≈ e ]
-c-iso→' {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa = let open ≈-Reasoning (A) in begin
+e←e' {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa = let open ≈-Reasoning (A) in begin
                  e' o c-iso-l eqa eqa' keqa 
               ≈⟨⟩
                  e'  o k eqa' e (fe=ge eqa)
@@ -186,10 +188,10 @@
                  e
               ∎
 
-c-iso←' : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' :  Equalizer A e' f g )
+e'←e : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' :  Equalizer A e' f g )
       →  ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ])  (A [ g o e' ]) )
       →  A [ A [ e o c-iso-r eqa eqa' keqa ]  ≈ e' ]
-c-iso←' {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa = let open ≈-Reasoning (A) in begin
+e'←e {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa = let open ≈-Reasoning (A) in begin
                  e o c-iso-r eqa eqa' keqa 
               ≈⟨⟩
                  e  o  k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') )
@@ -232,7 +234,7 @@
                      k eqa' e (fe=ge eqa )
                    ≈⟨ uniqueness eqa' ( begin
                        e' o k keqa' (id1 A c) (f1=g1 (fe=ge eqa) (id1 A c))
-                   ≈↑⟨ car (c-iso←' eqa eqa' keqa ) ⟩
+                   ≈↑⟨ car (e'←e eqa eqa' keqa ) ⟩
                         ( e  o equalizer keqa' ) o k keqa' (id1 A c) (f1=g1 (fe=ge eqa) (id1 A c))
                    ≈↑⟨ assoc ⟩
                          e  o ( equalizer keqa'  o k keqa' (id1 A c) (f1=g1 (fe=ge eqa) (id1 A c)))
@@ -249,6 +251,7 @@
 
 
 
+--------------------------------
 ----
 --
 -- An equalizer satisfies Burroni equations
@@ -373,6 +376,10 @@
                     j
              ∎ 
 
+--------------------------------
+--
+-- Bourroni equations gives an Equalizer
+--
 
 lemma-equ2 : {a b c : Obj A} (f g : Hom A a b)  (e : Hom A c a )
          → ( bur : Burroni A {c} {a} {b} f g e ) → Equalizer A {c} {a} {b} (α bur f g e) f g