Mercurial > hg > Members > kono > Proof > category

changeset 777:5160b431f1de

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 26 Sep 2018 10:00:02 +0900
parents 5a3ca9509fbf
children 06388660995b
files epi.agda
diffstat 1 files changed, 89 insertions(+), 77 deletions(-) [+]
line wrap: on
line diff
--- a/epi.agda	Tue Sep 25 18:06:14 2018 +0900
+++ b/epi.agda	Wed Sep 26 10:00:02 2018 +0900
@@ -23,56 +23,68 @@
    arrow-ad :  FourHom ta td
    arrow-cd :  FourHom tc td
 
+--
+--       epi and monic but does not have inverted arrow
+--
+--       +--------------------------+
+--       |                          |
+--       c-----------------+        |
+--       |                 ↓        ↓
+--       + ----→  a ----→  b ----→  d 
+--                |                 ↑
+--                +-----------------+
+--
 
-_×_ :  {a b c : FourObject } →  FourHom b c  →  FourHom a b   →  FourHom a c 
-_×_ {x} {ta} {ta}  id-ta   y  = y
-_×_ {x} {tb} {tb}  id-tb   y  = y
-_×_ {x} {tc} {tc}  id-tc   y  = y
-_×_ {x} {td} {td}  id-td   y  = y
-_×_ {ta} {ta} {x}  y id-ta = y
-_×_ {tb} {tb} {x}  y id-tb = y
-_×_ {tc} {tc} {x}  y id-tc = y
-_×_ {td} {td} {x}  y id-td = y
-_×_ {tc} {ta} {tb} arrow-ab arrow-ca = arrow-cb
-_×_ {ta} {tb} {td} arrow-bd arrow-ab = arrow-ad
-_×_ {tc} {tb} {td} arrow-bd arrow-cb = arrow-cd
-_×_ {tc} {ta} {td} arrow-ad arrow-ca = arrow-cd
-_×_ {tc} {ta} {tc} () arrow-ca
-_×_ {ta} {tb} {ta} () arrow-ab
-_×_ {tc} {tb} {ta} () arrow-cb
-_×_ {ta} {tb} {tc} () arrow-ab
-_×_ {tc} {tb} {tc} () arrow-cb
-_×_ {tb} {td} {ta} () arrow-bd
-_×_ {ta} {td} {ta} () arrow-ad
-_×_ {tc} {td} {ta} () arrow-cd
-_×_ {tb} {td} {tb} () arrow-bd
-_×_ {ta} {td} {tb} () arrow-ad
-_×_ {tc} {td} {tb} () arrow-cd
-_×_ {tb} {td} {tc} () arrow-bd
-_×_ {ta} {td} {tc} () arrow-ad
-_×_ {tc} {td} {tc} () arrow-cd
+
+_・_ :  {a b c : FourObject } →  FourHom b c  →  FourHom a b   →  FourHom a c 
+_・_ {x} {ta} {ta}  id-ta   y  = y
+_・_ {x} {tb} {tb}  id-tb   y  = y
+_・_ {x} {tc} {tc}  id-tc   y  = y
+_・_ {x} {td} {td}  id-td   y  = y
+_・_ {ta} {ta} {x}  y id-ta = y
+_・_ {tb} {tb} {x}  y id-tb = y
+_・_ {tc} {tc} {x}  y id-tc = y
+_・_ {td} {td} {x}  y id-td = y
+_・_ {tc} {ta} {tb} arrow-ab arrow-ca = arrow-cb
+_・_ {ta} {tb} {td} arrow-bd arrow-ab = arrow-ad
+_・_ {tc} {tb} {td} arrow-bd arrow-cb = arrow-cd
+_・_ {tc} {ta} {td} arrow-ad arrow-ca = arrow-cd
+_・_ {tc} {ta} {tc} () arrow-ca
+_・_ {ta} {tb} {ta} () arrow-ab
+_・_ {tc} {tb} {ta} () arrow-cb
+_・_ {ta} {tb} {tc} () arrow-ab
+_・_ {tc} {tb} {tc} () arrow-cb
+_・_ {tb} {td} {ta} () arrow-bd
+_・_ {ta} {td} {ta} () arrow-ad
+_・_ {tc} {td} {ta} () arrow-cd
+_・_ {tb} {td} {tb} () arrow-bd
+_・_ {ta} {td} {tb} () arrow-ad
+_・_ {tc} {td} {tb} () arrow-cd
+_・_ {tb} {td} {tc} () arrow-bd
+_・_ {ta} {td} {tc} () arrow-ad
+_・_ {tc} {td} {tc} () arrow-cd
 
 open FourHom
 
 
-assoc-× :    {a b c d : FourObject   }
-       {f : (FourHom c d )} → {g : (FourHom b c )} → {h : (FourHom a b )} →
-       ( f × (g × h)) ≡ ((f × g) × h )
-assoc-×  {_} {_} {_} {_} {id-ta} {y} {z} = refl
-assoc-×  {_} {_} {_} {_} {id-tb} {y} {z} = refl
-assoc-×  {_} {_} {_} {_} {id-tc} {y} {z} = refl
-assoc-×  {_} {_} {_} {_} {id-td} {y} {z} = refl
-assoc-×  {_} {_} {_} {_} {arrow-ca} {id-tc} {z} = refl
-assoc-×  {_} {_} {_} {_} {arrow-ab} {id-ta} {z} = refl
-assoc-×  {_} {_} {_} {_} {arrow-ab} {arrow-ca} {id-tc} = refl
-assoc-×  {_} {_} {_} {_} {arrow-bd} {id-tb} {z} = refl
-assoc-×  {_} {_} {_} {_} {arrow-bd} {arrow-ab} {id-ta} = refl
-assoc-×  {_} {_} {_} {_} {arrow-bd} {arrow-ab} {arrow-ca} = refl
-assoc-×  {_} {_} {_} {_} {arrow-bd} {arrow-cb} {id-tc} = refl
-assoc-×  {_} {_} {_} {_} {arrow-cb} {id-tc} {z} = refl
-assoc-×  {_} {_} {_} {_} {arrow-ad} {id-ta} {z} = refl
-assoc-×  {_} {_} {_} {_} {arrow-ad} {arrow-ca} {id-tc} = refl
-assoc-×  {_} {_} {_} {_} {arrow-cd} {id-tc} {id-tc} = refl
+assoc-・ :    {a b c d : FourObject   }
+       (f : FourHom c d ) → (g : FourHom b c ) → (h : FourHom a b ) →
+       ( f ・ (g ・ h)) ≡ ((f ・ g) ・ h )
+assoc-・  id-ta y z = refl
+assoc-・  id-tb y z = refl
+assoc-・  id-tc y z = refl
+assoc-・  id-td y z = refl
+assoc-・  arrow-ca id-tc z = refl
+assoc-・  arrow-ab id-ta z = refl
+assoc-・  arrow-ab arrow-ca id-tc = refl
+assoc-・  arrow-bd id-tb z = refl
+assoc-・  arrow-bd arrow-ab id-ta = refl
+assoc-・  arrow-bd arrow-ab arrow-ca = refl
+assoc-・  arrow-bd arrow-cb id-tc = refl
+assoc-・  arrow-cb id-tc z = refl
+assoc-・  arrow-ad id-ta z = refl
+assoc-・  arrow-ad arrow-ca id-tc = refl
+assoc-・  arrow-cd id-tc id-tc = refl
 
 FourId :   (a : FourObject  ) →  (FourHom  a a )
 FourId ta = id-ta 
@@ -86,17 +98,17 @@
 FourCat    = record {
     Obj  = FourObject ;
     Hom = λ a b →   FourHom a b  ;
-    _o_ =  λ{a} {b} {c} x y → _×_ x y ;
+    _o_ =  λ{a} {b} {c} x y → _・_ x y ;
     _≈_ =  λ x y → x  ≡ y ;
     Id  =  λ{a} → FourId a ;
     isCategory  = record {
             isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } ; identityL  = λ{a b f} → identityL {a} {b} {f} ;
             identityR  = λ{a b f} → identityR  {a} {b} {f} ;
             o-resp-≈  = λ{a b c f g h i} →  o-resp-≈   {a} {b} {c} {f} {g} {h} {i} ;
-            associative  = λ{a b c d f g h } → assoc-×    {a} {b} {c} {d} {f} {g} {h}
+            associative  = λ{a b c d f g h } → assoc-・    f g h
        }
    }  where
-        identityL :   {A B : FourObject } {f : ( FourHom A B) } →  ((FourId B)  × f)  ≡ f
+        identityL :   {A B : FourObject } {f : ( FourHom A B) } →  ((FourId B)  ・ f)  ≡ f
         identityL  {ta} {ta} {id-ta} = refl
         identityL  {tb} {tb} {id-tb} = refl
         identityL  {tc} {tc} {id-tc} = refl
@@ -107,7 +119,7 @@
         identityL  {tc} {tb} {arrow-cb} = refl
         identityL  {ta} {td} {arrow-ad} = refl
         identityL  {tc} {td} {arrow-cd} = refl
-        identityR :   {A B : FourObject } {f : ( FourHom A B) } →   ( f × FourId A )  ≡ f
+        identityR :   {A B : FourObject } {f : ( FourHom A B) } →   ( f ・ FourId A )  ≡ f
         identityR  {ta} {ta} {id-ta} = refl
         identityR  {tb} {tb} {id-tb} = refl
         identityR  {tc} {tc} {id-tc} = refl
@@ -119,34 +131,34 @@
         identityR  {ta} {td} {arrow-ad} = refl
         identityR  {tc} {td} {arrow-cd} = refl
         o-resp-≈ :   {A B C : FourObject   } {f g :  ( FourHom A B)} {h i : ( FourHom B C)} →
-            f  ≡ g → h  ≡ i → ( h × f )  ≡ ( i × g )
+            f  ≡ g → h  ≡ i → ( h ・ f )  ≡ ( i ・ g )
         o-resp-≈  {a} {b} {c} {f} {x} {h} {y} refl refl = refl
 
-epi :  {a b c : FourObject } {f₁ f₂ : Hom FourCat  a b } { h : Hom FourCat b c }
-   →   FourCat  [  h o f₁ ]  ≡ FourCat [  h o  f₂ ]   → f₁  ≡  f₂
-epi {ta} {ta} {c} {id-ta} {id-ta} {h} refl = refl
-epi {tb} {tb} {c} {id-tb} {id-tb} {h} refl = refl
-epi {tc} {tc} {c} {id-tc} {id-tc} {h} refl = refl
-epi {td} {td} {c} {id-td} {id-td} {h} refl = refl
-epi {tc} {ta} {c} {arrow-ca} {arrow-ca} {h} refl = refl
-epi {ta} {tb} {c} {arrow-ab} {arrow-ab} {h} refl = refl
-epi {tb} {td} {c} {arrow-bd} {arrow-bd} {h} refl = refl
-epi {tc} {tb} {c} {arrow-cb} {arrow-cb} {h} refl = refl
-epi {ta} {td} {c} {arrow-ad} {arrow-ad} {h} refl = refl
-epi {tc} {td} {c} {arrow-cd} {arrow-cd} {h} refl = refl
+epi :  {a b c : FourObject } (f₁ f₂ : Hom FourCat  a b ) ( h : Hom FourCat b c )
+   →    h ・ f₁   ≡ h ・  f₂   → f₁  ≡  f₂
+epi id-ta id-ta _ refl = refl
+epi id-tb id-tb _ refl = refl
+epi id-tc id-tc _ refl = refl
+epi id-td id-td _ refl = refl
+epi arrow-ca arrow-ca _ refl = refl
+epi arrow-ab arrow-ab _ refl = refl
+epi arrow-bd arrow-bd _ refl = refl
+epi arrow-cb arrow-cb _ refl = refl
+epi arrow-ad arrow-ad _ refl = refl
+epi arrow-cd arrow-cd _ refl = refl
 
-monic :  {a b c : FourObject } {g₁ g₂ : Hom FourCat  b c } { h : Hom FourCat  a b }
-   →   FourCat  [ g₁ o h ]  ≡ FourCat  [ g₂ o h ]   → g₁  ≡  g₂
-monic {a} {ta} {ta} {id-ta} {id-ta} {h} refl = refl
-monic {a} {tb} {tb} {id-tb} {id-tb} {h} refl = refl
-monic {a} {tc} {tc} {id-tc} {id-tc} {h} refl = refl
-monic {a} {td} {td} {id-td} {id-td} {h} refl = refl
-monic {a} {tc} {ta} {arrow-ca} {arrow-ca} {h} refl = refl
-monic {a} {ta} {tb} {arrow-ab} {arrow-ab} {h} refl = refl
-monic {a} {tb} {td} {arrow-bd} {arrow-bd} {h} refl = refl
-monic {a} {tc} {tb} {arrow-cb} {arrow-cb} {h} refl = refl
-monic {a} {ta} {td} {arrow-ad} {arrow-ad} {h} refl = refl
-monic {a} {tc} {td} {arrow-cd} {arrow-cd} {h} refl = refl
+monic :  {a b c : FourObject } (g₁ g₂ : Hom FourCat  b c ) ( h : Hom FourCat  a b )
+   →   g₁ ・ h  ≡ g₂ ・ h   → g₁  ≡  g₂
+monic id-ta id-ta _ refl = refl
+monic id-tb id-tb _ refl = refl
+monic id-tc id-tc _ refl = refl
+monic id-td id-td _ refl = refl
+monic arrow-ca arrow-ca _ refl = refl
+monic arrow-ab arrow-ab _ refl = refl
+monic arrow-bd arrow-bd _ refl = refl
+monic arrow-cb arrow-cb _ refl = refl
+monic arrow-ad arrow-ad _ refl = refl
+monic arrow-cd arrow-cd _ refl = refl
 
 open import cat-utility
 open import Relation.Nullary
@@ -155,11 +167,11 @@
 record Rev  {a b : FourObject } (f : Hom FourCat a b ) : Set where
   field
      rev :   Hom FourCat b a
-     eq  :   FourCat  [ f o rev ]  ≡ id1 FourCat b
+     eq  :   f ・ rev  ≡ id1 FourCat b
 
 not-rev : ¬ ( {a b : FourObject } →  (f : Hom FourCat a b ) →  Rev f )
-not-rev r =   ⊥-elim  ( lemma1 arrow-ab (Rev.rev (r  arrow-ab)) (Rev.eq (r  arrow-ab))  )
+not-rev r =  lemma1 arrow-ab (Rev.rev (r  arrow-ab)) (Rev.eq (r  arrow-ab))  
   where
      lemma1 :  (f : Hom FourCat ta tb )  →  (e₁ : Hom FourCat tb ta )
-          → ( FourCat  [ f o e₁ ]  ≡ id1 FourCat tb )  →  ⊥
+          → ( f ・ e₁  ≡ id1 FourCat tb )  →  ⊥
      lemma1 _ () eq