# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1457689798 -32400
# Node ID 2dfa2d59268c9ca94b44c966f9866ba5e7dffcf4
# Parent  f48940ff08141407e660c0c30e4c734b9e6056dd
associative in twocat dead end?

diff -r f48940ff0814 -r 2dfa2d59268c limit-to.agda
--- a/limit-to.agda	Thu Mar 10 19:56:12 2016 +0900
+++ b/limit-to.agda	Fri Mar 11 18:49:58 2016 +0900
@@ -29,10 +29,127 @@
 ---     d  
 
 
-data TwoObject   : Set where
+data  TwoObject   : Set  where
    t0 : TwoObject 
    t1 : TwoObject 
 
+data Arrow   : Set  where
+   id-t0 : Arrow  
+   id-t1 :  Arrow
+   arrow-f :  Arrow
+   arrow-g :  Arrow
+   arrow-f' :  Arrow
+
+arrowSel : (a : TwoObject   ) (b : TwoObject   ) (sel : TwoObject ) -> Arrow
+arrowSel t0 t0 _ =   id-t0 
+arrowSel t0 t1 t0 =  arrow-f 
+arrowSel t0 t1 t1 =  arrow-g 
+arrowSel t1 t0 _ =   arrow-f' 
+arrowSel t1 t1 _ =   id-t1 
+
+record Two-Hom   (a : TwoObject   ) (b : TwoObject   ) : Set  where
+   field
+       Map    : Arrow 
+       Sel    : TwoObject
+       selection :  ( arrowSel a b Sel  ) ≡ Map
+
+
+Two-id :  (a : TwoObject ) ->  Two-Hom a a
+Two-id t0  = record { Map = id-t0 ; Sel = t0 ; selection = refl }
+Two-id t1  = record { Map = id-t1 ; Sel = t0 ; selection = refl }
+
+-- arrow composition
+
+open Two-Hom
+
+_×_ :  {A B C : TwoObject } → Two-Hom B C → Two-Hom A B → Two-Hom A C
+_×_   {t0} {t0} {t0} a b  = record { Map = id-t0 ; Sel = t0 ; selection = refl }
+_×_   {t0} {t0} {t1} a b  = record { Map = Map a ; Sel = Sel a ; selection = selection a }
+_×_   {t0} {t1} {t0} a b  = record { Map = id-t0 ; Sel = t0 ; selection = refl }
+_×_   {t0} {t1} {t1} a b  = record { Map = Map b ; Sel = Sel b ; selection = selection b }
+_×_   {t1} {t0} {t0} a b  = record { Map = arrow-f' ; Sel = t0 ; selection = refl }
+_×_   {t1} {t0} {t1} a b  = record { Map = id-t1 ; Sel = t0 ; selection = refl }
+_×_   {t1} {t1} {t0} a b  = record { Map = arrow-f' ; Sel = t0 ; selection = refl }
+_×_   {t1} {t1} {t1} a b  = record { Map = id-t1 ; Sel = t0 ; selection = refl }
+
+
+
+
+twocat : {ℓ c₁ c₂ : Level  } ->  Category _ _ _ 
+twocat  = record {
+    Obj  = TwoObject  ;
+    Hom = λ a b →  Two-Hom a b   ; 
+    _o_ =  _×_ ;
+    _≈_ = λ a b →   Map a ≡ Map b  ;
+    Id  =  \{a} -> Two-id 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 } -> associative  {a} {b} {c} {d} {f} {g} {h}
+       } 
+   } where
+        open  import  Relation.Binary.PropositionalEquality
+        ≡-cong = Relation.Binary.PropositionalEquality.cong 
+        identityL : {A B : TwoObject} {f : Two-Hom A B} → Map ( Two-id B × f ) ≡ Map f
+        identityL {t0} {t0} {f} =  let open ≡-Reasoning in
+              begin
+                Map ( Two-id t0 × f )
+              ≡⟨⟩
+                Map ( record { Map = id-t0 ; Sel = t0 ; selection = refl } )
+              ≡⟨ refl ⟩
+                 arrowSel t0 t0 (Sel f )
+              ≡⟨ selection f  ⟩
+                Map f
+              ∎
+        identityL {t0} {t1} {f} = refl
+        identityL {t1} {t0} {f} = selection f
+        identityL {t1} {t1} {f} = selection f
+        identityR : {A B : TwoObject} {f : Two-Hom A B} → Map ( f × Two-id A ) ≡ Map f
+        identityR {t0} {t0} {f} = selection f
+        identityR {t0} {t1} {f} = refl
+        identityR {t1} {t0} {f} = selection f
+        identityR {t1} {t1} {f} = selection f
+        o-resp-≈  : {A B C : TwoObject} {f g : Two-Hom A B} {h i : Two-Hom B C} →
+           Map f ≡ Map g → Map h ≡ Map i → Map ( h × f ) ≡ Map ( i × g )
+        o-resp-≈  {t0} {t0} {t0} {f} {g} {h} {i} f≡g h≡i = refl
+        o-resp-≈  {t0} {t0} {t1} {f} {g} {h} {i} f≡g h≡i = h≡i
+        o-resp-≈  {t0} {t1} {t0} {f} {g} {h} {i} f≡g h≡i = refl
+        o-resp-≈  {t0} {t1} {t1} {f} {g} {h} {i} f≡g h≡i = f≡g
+        o-resp-≈  {t1} {t0} {t0} {f} {g} {h} {i} f≡g h≡i = refl
+        o-resp-≈  {t1} {t0} {t1} {f} {g} {h} {i} f≡g h≡i = refl
+        o-resp-≈  {t1} {t1} {t0} {f} {g} {h} {i} f≡g h≡i = refl
+        o-resp-≈  {t1} {t1} {t1} {f} {g} {h} {i} f≡g h≡i = refl
+        associative : {A B C D : TwoObject} {f : Two-Hom C D} {g : Two-Hom B C} {h : Two-Hom A B} → Map ( f × (g × h) ) ≡ Map ( (f × g) × h )
+        associative {t0} {t0} {t0} {t0} {f} {g} {h} = refl
+        associative {t0} {t0} {t0} {t1} {f} {g} {h} = refl
+        associative {t0} {t0} {t1} {t0} {f} {g} {h} = refl
+        associative {t0} {t0} {t1} {t1} {f} {g} {h} = refl
+        associative {t0} {t1} {t0} {t0} {f} {g} {h} = refl
+        associative {t0} {t1} {t0} {t1} {f} {g} {h} =  let open ≡-Reasoning in
+              begin
+                Map ( f × (g × h) )
+              ≡⟨⟩
+                Map f 
+              ≡⟨ {!!} ⟩
+                Map h
+              ≡⟨⟩
+                Map ( (f × g) × h )
+              ∎
+        associative {t0} {t1} {t1} {t0} {f} {g} {h} = refl
+        associative {t0} {t1} {t1} {t1} {f} {g} {h} = refl
+        associative {t1} {t0} {t0} {t0} {f} {g} {h} = refl
+        associative {t1} {t0} {t0} {t1} {f} {g} {h} = refl
+        associative {t1} {t0} {t1} {t0} {f} {g} {h} = refl
+        associative {t1} {t0} {t1} {t1} {f} {g} {h} = refl
+        associative {t1} {t1} {t0} {t0} {f} {g} {h} = refl
+        associative {t1} {t1} {t0} {t1} {f} {g} {h} = refl
+        associative {t1} {t1} {t1} {t0} {f} {g} {h} = refl
+        associative {t1} {t1} {t1} {t1} {f} {g} {h} = refl
+
+
+
 record TwoCat  {ℓ c₁ c₂ : Level  } (I : Category  c₁ c₂ ℓ) (A : Category  c₁ c₂ ℓ)  ( a b : Obj A ) ( f g : Hom A a b ): Set  (c₂ ⊔ c₁ ⊔ ℓ)  where
     field
          obj→ : Obj I  -> TwoObject