Mercurial > hg > Members > kono > Proof > category

changeset 449:156e64d1bce0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on goinhg ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 02 Jan 2017 11:26:21 +0900
parents c2616de4d208
children e9ece23ab94e
files discrete.agda
diffstat 1 files changed, 101 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/discrete.agda	Mon Jan 02 11:01:53 2017 +0900
+++ b/discrete.agda	Mon Jan 02 11:26:21 2017 +0900
@@ -121,7 +121,107 @@
        {g : (TwoHom {c₁}  {c₂ } b c )} →
        {h : (TwoHom {c₁}  {c₂ } a b )} →
        hom ( f × (g × h)) == hom ((f × g) × h )
-assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} = {!!} -- with  hom f | hom g | hom h
+assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} with  hom f | hom g | hom h
+assoc-× {c₁} {c₂} {_} {_} {_} {_} {f} {g} {h} | nothing | _ | _ = nothing
+assoc-× {c₁} {c₂} {_} {_} {_} {_} {f} {g} {h} | just _ | nothing | _ = nothing
+assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} {f} {g} {h} | just id-t0   | just id-t0   | just id-t0  = ==refl
+assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-f | just id-t0   | just id-t0  = ==refl
+assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-g | just id-t0   | just id-t0  = ==refl
+assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1   | just arrow-f | just id-t0  = ==refl
+assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1   | just arrow-g | just id-t0  = ==refl
+assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just id-t1   | just id-t1   | just arrow-f = ==refl
+assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just id-t1   | just id-t1   | just arrow-g = ==refl
+assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} {f} {g} {h} | just id-t1   | just id-t1   | just id-t1  = ==refl
+--  remaining all failure case 
+assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} {f} {g} {h} | just id-t0 | just id-t0 | nothing = nothing
+assoc-× {c₁} {c₂} {t1} {t0} {t0} {t0} {f} {g} {h} | just id-t0 | just id-t0 | nothing = nothing
+assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | nothing = nothing
+assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | nothing = nothing
+assoc-× {c₁} {c₂} {t1} {t0} {t0} {t1} {f} {g} {h} | just arrow-f | just id-t0 | nothing = nothing
+assoc-× {c₁} {c₂} {t1} {t0} {t0} {t1} {f} {g} {h} | just arrow-g | just id-t0 | nothing = nothing
+assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-f | just id-t0 | nothing = nothing
+assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-g | just id-t0 | nothing = nothing
+assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-f | nothing = nothing
+assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-g | nothing = nothing
+assoc-× {c₁} {c₂} {t1} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-f | nothing = nothing
+assoc-× {c₁} {c₂} {t1} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-g | nothing = nothing
+assoc-× {_} {_} {t0} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just _) | nothing = nothing
+assoc-× {_} {_} {t0} {t1} {t0} {t1} {_} {_} {_} | (just _) | (just _) | nothing = nothing
+assoc-× {_} {_} {t1} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just _) | nothing = nothing
+assoc-× {_} {_} {t1} {t1} {t0} {t1} {_} {_} {_} | (just _) | (just _) | nothing = nothing
+assoc-× {_} {_} {t0} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just arrow-f) | (just id-t0) = nothing
+assoc-× {_} {_} {t0} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just arrow-g) | (just id-t0) = nothing
+assoc-× {_} {_} {t0} {t1} {t0} {t1} {_} {_} {_} | (just _) | (just _) | (just _) = nothing
+assoc-× {_} {_} {t1} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just _) | (just _) = nothing
+assoc-× {_} {_} {t1} {t0} {t1} {t1} {_} {_} {_} | (just id-t1) | (just arrow-f) | (just _) = nothing
+assoc-× {_} {_} {t1} {t0} {t1} {t1} {_} {_} {_} | (just id-t1) | (just arrow-g) | (just _) = nothing
+assoc-× {_} {_} {t0} {t1} {t0} {t0} {_} {_} {_} | (just _) | (just _) | (just _) = nothing
+assoc-× {_} {_} {t0} {t1} {t0} {t0} {_} {_} {_} | (just _) | (just _) | nothing = nothing
+assoc-× {_} {_} {t1} {t0} {t0} {t0} {_} {_} {_} | (just id-t0) | (just id-t0) | (just _) = nothing
+assoc-× {_} {_} {t1} {t0} {t0} {t1} {_} {_} {_} | (just arrow-f) | (just id-t0) | (just _) = nothing
+assoc-× {_} {_} {t1} {t0} {t0} {t1} {_} {_} {_} | (just arrow-g) | (just id-t0) | (just _) = nothing
+assoc-× {_} {_} {t1} {t1} {t0} {_} {_} {_} {_} | (just _) | (just _) | (just _) = nothing
+assoc-× {_} {_} {t1} {t1} {t0} {t0} {_} {_} {_} | (just _) | (just _) |  nothing = nothing
+
+TwoId :  {c₁  c₂ : Level } (a : TwoObject  {c₁} ) →  (TwoHom {c₁}  {c₂ } a a )
+TwoId {_} {_} t0 = record { hom =  just id-t0 }
+TwoId {_} {_} t1 = record { hom =  just id-t1 }
+
+
+open import Relation.Binary
+TwoCat : {c₁ c₂ ℓ : Level  } →  Category   c₁  c₂  c₂
+TwoCat   {c₁}  {c₂} {ℓ} = record {
+    Obj  = TwoObject  {c₁} ;
+    Hom = λ a b →    ( TwoHom {c₁}  {c₂ } a b ) ;
+    _o_ =  λ{a} {b} {c} x y → _×_ {c₁ } { c₂} {a} {b} {c} x y ;
+    _≈_ =  λ x y → hom x == hom y ;
+    Id  =  λ{a} → TwoId {c₁ } { c₂} a ;
+    isCategory  = record {
+            isEquivalence =  record {refl = ==refl ; trans = ==trans ; sym = ==sym } ;
+            identityL  = λ{a b f} → identityL {c₁}  {c₂ } {a} {b} {f} ;
+            identityR  = λ{a b f} → identityR {c₁}  {c₂ } {a} {b} {f} ;
+            o-resp-≈  = λ{a b c f g h i} →  o-resp-≈  {c₁}  {c₂ } {a} {b} {c} {f} {g} {h} {i} ;
+            associative  = λ{a b c d f g h } → assoc-×   {c₁}  {c₂} {a} {b} {c} {d} {f} {g} {h}
+       }
+   }  where
+        identityL :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁}  {c₂ } A B) } →  hom ((TwoId B)  × f)  == hom f
+        identityL  {c₁}  {c₂}  {_} {_} {f}  with hom f
+        identityL  {c₁}  {c₂}  {t0} {t0} {_} | nothing  = nothing
+        identityL  {c₁}  {c₂}  {t0} {t1} {_} | nothing  = nothing
+        identityL  {c₁}  {c₂}  {t1} {t0} {_} | nothing  = nothing
+        identityL  {c₁}  {c₂}  {t1} {t1} {_} | nothing  = nothing
+        identityL  {c₁}  {c₂}  {t1} {t1} {_} | just id-t1  = ==refl
+        identityL  {c₁}  {c₂}  {t0} {t0} {_} | just id-t0 = ==refl
+        identityL  {c₁}  {c₂}  {t0} {t1} {_} | just arrow-f = ==refl
+        identityL  {c₁}  {c₂}  {t0} {t1} {_} | just arrow-g = ==refl
+        identityL  {c₁}  {c₂}  {t1} {t0} {_} | just _  = ?
+        identityR :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁}  {c₂ } A B) } →   hom ( f × TwoId A )  == hom f
+        identityR  {c₁}  {c₂}  {_} {_} {f}  with hom f
+        identityR  {c₁}  {c₂}  {t0} {t0} {_} | nothing  = nothing
+        identityR  {c₁}  {c₂}  {t0} {t1} {_} | nothing  = nothing
+        identityR  {c₁}  {c₂}  {t1} {t0} {_} | nothing  = nothing
+        identityR  {c₁}  {c₂}  {t1} {t1} {_} | nothing  = nothing
+        identityR  {c₁}  {c₂}  {t1} {t1} {_} | just id-t1  = ==refl
+        identityR  {c₁}  {c₂}  {t0} {t0} {_} | just id-t0 = ==refl
+        identityR  {c₁}  {c₂}  {t0} {t1} {_} | just arrow-f = ==refl
+        identityR  {c₁}  {c₂}  {t0} {t1} {_} | just arrow-g = ==refl
+        identityR  {c₁}  {c₂}  {t1} {t0} {_} | just _  = ?
+        o-resp-≈ :  {c₁  c₂ : Level } {A B C : TwoObject  {c₁} } {f g :  ( TwoHom {c₁}  {c₂ } A B)} {h i : ( TwoHom B C)} →
+            hom f == hom g → hom h == hom i → hom ( h × f ) == hom ( i × g )
+        o-resp-≈  {c₁}  {c₂} {a} {b} {c} {f} {g} {h} {i}  f==g h==i  = 
+          let open  ==-Reasoning {c₁} {c₂ } in begin
+                    hom ( h × f )
+                ==⟨⟩
+                    comp (hom h) (hom f)
+                ==⟨ ==cong (λ x  → comp ( hom h ) x )  f==g ⟩
+                    comp (hom h) (hom g)
+                ==⟨ ==cong (λ x  → comp x ( hom g ) )  h==i ⟩
+                    comp (hom i) (hom g)
+                ==⟨⟩
+                    hom ( i × g )
+                ∎
+
+
 
 
 record  Nil {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  :  Set   ( c₁ ⊔ c₂ ⊔ ℓ ) where