# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1435313034 -32400
# Node ID 29e0f0bd4d2c42b3f361af3d5db30c8b82a874da
# Parent  6d803a4708bf5e8a9dc13d7dfab643de38aa4058
arrow

diff -r 6d803a4708bf -r 29e0f0bd4d2c limit-to.agda
--- a/limit-to.agda	Fri Jun 26 17:56:22 2015 +0900
+++ b/limit-to.agda	Fri Jun 26 19:03:54 2015 +0900
@@ -23,7 +23,6 @@
 ---       ------>
 ---          g
 
-postulate φ id-0 id-1 f g : Set  c₂
 
 infixr 40 _::_
 data  List {a} (A : Set a)  : Set a where
@@ -50,34 +49,73 @@
 memberp1 .(succ (x + y)) ( x :: T)  | greater .x y = memberp1 x T
 
 
-
+-- Category object configuration
 
-data Two {c₁}  : Set c₁ where
+data Two   : Set c₁ where
    t0 : Two 
    t1 : Two 
 
-record Two-Hom {c₁} (a : Two  {c₁}) (b : Two  {c₁}) : Set (c₁ ⊔ suc c₂ ⊔ ℓ) where
-   field
-       Map    : Set  c₂
+two-equality : Two -> Two -> Bool
+two-equality  t0 t0 = true
+two-equality  t0 t1 = false
+two-equality  t1 t0 = true
+two-equality  t1 t1 = false
+
+data Arrow  : Set  c₂ where
+    id-0 : Arrow
+    id-1 :  Arrow
+    af :  Arrow
+    ag :  Arrow
 
-hom : Two {c₁} → Two {c₁} → List (Set  c₂)
+arrow-equality : Arrow -> Arrow -> Bool
+arrow-equality id-0 id-0 = true
+arrow-equality id-0 id-1 = false
+arrow-equality id-0 af = false
+arrow-equality id-0 ag = false
+arrow-equality id-1 id-0 = false
+arrow-equality id-1 id-1 = true
+arrow-equality id-1 af = false
+arrow-equality id-1 ag = false
+arrow-equality af id-0 = false
+arrow-equality af id-1 = false
+arrow-equality af af = true
+arrow-equality af ag = false
+arrow-equality ag id-0 = false
+arrow-equality ag id-1 = false
+arrow-equality ag af = false
+arrow-equality ag ag = true
+
+-- Category arrow configuration
+
+hom : Two  → Two  → List (Arrow )
 hom t0 t0 =  id-0 :: []
-hom t0 t1 =  f :: g :: []
+hom t0 t1 =  af :: ag :: []
 hom t1 t0 =  []
 hom t1 t1 =  id-1 :: []
 
-Two-id :  {c₁ : Level} -> (a : Two {c₁}) ->  Two-Hom {c₁} a a
-Two-id {c₁} t0  = record { Map = id-0 }
-Two-id {c₁} t1  = record { Map = id-1 }
+in-hom : Arrow -> List Arrow -> Bool
+in-hom _ [] = false
+in-hom x (y :: T) with arrow-equality  x y
+in-hom _ (y :: T) | true = true
+in-hom x (y :: T) | false = in-hom x T
+
+record Two-Hom (a : Two  ) (b : Two  ) : Set (c₁ ⊔ suc c₂ ⊔ ℓ) where
+   field
+       Map    : Arrow 
+       isMap  : in-hom  Map ( hom a b )  ≡ true
+
+Two-id :  (a : Two ) ->  Two-Hom a a
+Two-id t0  = record { Map = id-0 ; isMap = refl }
+Two-id t1  = record { Map = id-1 ; isMap = refl }
 
 open Two-Hom
 
-twocat : {c₁ ℓ : Level} → Category c₁ _ ℓ
-twocat {c₁} {ℓ} = record {
-    Obj  = Two {c₁} ;
+twocat :  Category c₁ _ (ℓ ⊔ (suc c₂ ⊔ c₁))
+twocat  = record {
+    Obj  = Two ;
     Hom = λ a b →  Two-Hom a b   ; 
     _o_ =  {!!} ;
-    _≈_ = {!!} ;
+    _≈_ = _≡_;
     Id  =  \{a} -> Two-id a ;
     isCategory  = record {
             isEquivalence = {!!} ;
@@ -100,10 +138,10 @@
         ; ek=h = λ {d} {h} {fh=gh} → {!!}
         ; uniqueness = λ {d} {h} {fh=gh} {k'} → {!!}
      } where
-         Γobj :  Two {c₁} → Obj A
+         Γobj :  Two  → Obj A
          Γobj t0 = a
          Γobj t1 = b
-         Γmap :  Two {c₁} → Hom A a b
+         Γmap :  Two  → Hom A a b
          Γmap t0 = f
          Γmap t1 = g
          Γ : Functor I A