--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/discrete.agda	Mon Jan 02 11:01:53 2017 +0900
@@ -0,0 +1,285 @@
+open import Category -- https://github.com/konn/category-agda
+open import Level
+
+module discrete where
+
+open import cat-utility
+open import HomReasoning
+open import Relation.Binary.Core
+open import Relation.Nullary
+open import Data.Empty
+open import Data.Maybe
+
+open Functor
+
+data  TwoObject {c₁ : Level}  : Set c₁ where
+   t0 : TwoObject
+   t1 : TwoObject
+
+-- If we have limit then we have equalizer
+---  two objects category
+---
+---          f
+---       -----→
+---     0         1
+---       -----→
+---          g
+
+data Arrow {c₁ c₂ : Level } : TwoObject {c₁}  → TwoObject {c₁} → Set c₂ where
+   id-t0 : Arrow t0 t0
+   id-t1 : Arrow t1 t1
+   arrow-f :  Arrow t0 t1
+   arrow-g :  Arrow t0 t1
+
+record TwoHom {c₁ c₂ : Level} (a b : TwoObject {c₁}  ) : Set ( c₂)  where
+   field
+       hom   :  Maybe ( Arrow {c₁} {c₂} a b )
+   constraint1 :  {c₁ c₂ : Level } → TwoObject {c₁}  → TwoObject {c₁} → Maybe ( Set zero )
+   constraint1 t0 t0  = nothing
+   constraint1 {_} {c₂} t0 t1  = just  ⊥ 
+   constraint1 t1 t0  = nothing
+   constraint1 t1 t1  = nothing
+
+comp :  ∀ {c₁  c₂}  → {a b c : TwoObject {c₁}} →  Maybe ( Arrow {c₁} {c₂} b c ) →  Maybe ( Arrow {c₁} {c₂} a b )  →  Maybe ( Arrow {c₁} {c₂} a c )
+comp {_}  {_}  {_} {_} {_}  nothing     _                =   nothing 
+comp {_}  {_}  {_} {_} {_}  (just _     ) nothing          =   nothing 
+comp {_}  {_}  {t0} {t1} {t1}  (just id-t1 ) ( just arrow-f )  =   just arrow-f 
+comp {_}  {_}  {t0} {t1} {t1}  (just id-t1 ) ( just arrow-g ) =   just arrow-g 
+comp {_}  {_}  {t1} {t1} {t1}  (just id-t1 ) ( just id-t1   ) =   just id-t1 
+comp {_}  {_}  {t0} {t0} {t1}  (just arrow-f ) ( just id-t0 )   =   just arrow-f 
+comp {_}  {_}  {t0} {t0} {t1}  (just arrow-g ) ( just id-t0 )   =   just arrow-g 
+comp {_}  {_}  {t0} {t0} {t0}  (just id-t0 ) ( just id-t0  )  =   just id-t0 
+comp {_}  {_}  {_} {_} {_}  (just _ ) ( just _ )  =   nothing 
+
+open TwoHom
+
+_×_ :  ∀ {c₁  c₂}  → {a b c : TwoObject {c₁}} →  ( TwoHom {c₁}  {c₂} b c ) →  ( TwoHom {c₁} {c₂} a b )  →  ( TwoHom {c₁}  {c₂} a c )
+_×_  {c₁}  {c₂}  {a} {b} {c} f g  = record { hom = comp  {c₁}  {c₂}  {a} {b} {c} (hom f) (hom g ) }
+
+_==_ :  ∀{ c₁ c₂ a b }   →  Rel (Maybe (Arrow {c₁} {c₂} a b )) (c₂)
+_==_   =  Eq   _≡_
+
+==refl :  ∀{  c₁ c₂ a b }  →  ∀ {x : Maybe (Arrow  {c₁} {c₂} a b )} → x == x
+==refl {_} {_} {_} {_} {just x}  = just refl
+==refl {_} {_} {_} {_} {nothing} = nothing
+
+==sym :  ∀{  c₁ c₂ a b }   → ∀ {x y :  Maybe (Arrow  {c₁}  {c₂}  a b )} →  x == y →  y == x
+==sym (just x≈y) = just (≡-sym x≈y)
+==sym nothing    = nothing
+
+==trans :  ∀{  c₁ c₂ a b }   → ∀ {x y z :   Maybe (Arrow  {c₁}  {c₂}  a b )  } →
+         x == y → y == z  → x == z
+==trans (just x≈y) (just y≈z) = just (≡-trans x≈y y≈z)
+==trans nothing    nothing    = nothing
+
+==cong :  ∀{  c₁ c₂ a b c d }   → ∀ {x y :  Maybe (Arrow  {c₁}  {c₂}  a b )} →  
+        (f : Maybe (Arrow  {c₁}  {c₂}  a b ) → Maybe (Arrow  {c₁}  {c₂}  c d ) ) → x  ==  y →  f x == f y
+==cong   {  c₁} {c₂} {a} {b } {c} {d} {nothing} {nothing} f nothing = ==refl
+==cong   {  c₁} {c₂} {a} {b } {c} {d} {just x} {just .x} f (just refl)  = ==refl
+
+
+module ==-Reasoning {c₁ c₂ : Level} where
+
+        infixr  2 _∎
+        infixr 2 _==⟨_⟩_ _==⟨⟩_
+        infix  1 begin_
+
+
+        data _IsRelatedTo_   {c₁ c₂ : Level}  {a b : TwoObject {c₁}  }  (x y : (Maybe (Arrow  {c₁}  {c₂}  a b ))) :
+                             Set  c₂ where
+            relTo : (x≈y : x  == y  ) → x IsRelatedTo y
+
+        begin_ :  { a b : TwoObject  {c₁} } {x : Maybe (Arrow  {c₁}  {c₂}  a b ) } {y : Maybe (Arrow  {c₁}  {c₂}  a b )} →
+                   x IsRelatedTo y →  x ==  y
+        begin relTo x≈y = x≈y
+
+        _==⟨_⟩_ :  { a b : TwoObject  {c₁} } (x :  Maybe (Arrow  {c₁}  {c₂}  a b )) {y z :  Maybe (Arrow  {c₁}  {c₂}  a b ) } →
+                    x == y  → y IsRelatedTo z → x IsRelatedTo z
+        _ ==⟨ x≈y ⟩ relTo y≈z = relTo (==trans x≈y y≈z)
+
+        
+        _==⟨⟩_ :   { a b : TwoObject  {c₁} }(x : Maybe (Arrow  {c₁}  {c₂}  a b )) {y : Maybe (Arrow  {c₁}  {c₂}  a b  )}
+                    → x IsRelatedTo y → x IsRelatedTo y
+        _ ==⟨⟩ x≈y = x≈y
+
+        _∎ :   { a b : TwoObject  {c₁} }(x :  Maybe (Arrow  {c₁}  {c₂}  a b )) → x IsRelatedTo x
+        _∎ _ = relTo ==refl
+
+
+-- TwoHom1Eq :  {c₁  c₂ : Level } {a b : TwoObject  {c₁} } {f g :  ( TwoHom1 {c₁}  {c₂ } a b)}  →
+--             hom (Map f) == hom (Map g) → f == g
+-- TwoHom1Eq  = ?
+
+
+--          f    g    h
+--       d <- c <- b <- a
+--
+--   It can be proved without Arrow constraints
+
+assoc-× :   {c₁  c₂ : Level } {a b c d : TwoObject  {c₁} }
+       {f : (TwoHom {c₁}  {c₂ } c d )} →
+       {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
+
+
+record  Nil {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  :  Set   ( c₁ ⊔ c₂ ⊔ ℓ ) where 
+     field 
+         nil : {a b : Obj A } → Hom A a b
+         nil-id : {a  : Obj A } →  A [ nil {a} {a} ≈ id1 A a ]    -- too strong but we need this
+         nil-idL : {a b c : Obj A } → { f : Hom A a b } → A [ A [ nil {b} {c} o f ]   ≈ nil {a} {c} ]
+         nil-idR : {a b c : Obj A } → { f : Hom A b c } → A [ A [ f o nil {a} {b} ]   ≈ nil {a} {c} ]
+
+open Nil
+
+indexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (none : Nil A) ( a b : Obj A) ( f g : Hom A a b ) →  
+    (obj : Obj A -> TwoObject {c₁}) (hom→ : {a b : Obj A} -> Hom A a b -> TwoObject {c₁})  → Functor A A
+indexFunctor  {c₁} {c₂} {ℓ} A none a b f g obj→ hom→ = record {
+         FObj = λ a → fobj a
+       ; FMap = λ {a} {b} f → fmap {a} {b} f
+       ; isFunctor = record {
+             identity = λ{x} → identity {x}
+             ; distr = λ {a} {b} {c} {f} {g}   → distr1 {a} {b} {c} {f} {g}
+             ; ≈-cong = λ {a} {b} {c} {f}   → ≈-cong  {a} {b} {c} {f}
+       }
+      } where
+          fobj :  Obj A → Obj A
+          fobj x with obj→ x 
+          fobj x | t0 = a
+          fobj x | t1 = b
+          fmap :  {x y : Obj A } →  (Hom A x y  ) → Hom A (fobj x) (fobj y)
+          fmap  {x} {y} h with obj→ x | obj→ y | hom→ h
+          fmap  h | t0 | t0 | _ = id1 A a
+          fmap  h | t1 | t1 | _ = id1 A b
+          fmap  h | t0 | t1 | t0 = f
+          fmap  h | t0 | t1 | t1 = g
+          fmap  h | _  | _  | _   = nil none
+          open  ≈-Reasoning A
+          ≈-cong :   {a : Obj A} {b : Obj A} {f g : Hom A a b}  → A [ f ≈ g ]  → A [ fmap f ≈ fmap g ]
+          ≈-cong  = {!!}
+          identity :  {x : Obj A} → A [ fmap ( id1 A x ) ≈  id1 A (fobj x) ]
+          identity {x} with obj→ x
+          identity | t0  =  refl-hom
+          identity | t1  =  refl-hom
+          distr1 : {a₁ : Obj A} {b₁ : Obj A} {c : Obj A} {f₁ : Hom A a₁ b₁} {g₁ : Hom A b₁ c} →
+               A [ fmap (A [ g₁ o f₁ ])  ≈  A [ fmap g₁ o fmap f₁ ] ]
+          distr1 {a1} {b1} {c1} {f1} {g1} with obj→ a1 | obj→ b1 | obj→ c1 | hom→ f1 | hom→ g1 
+          distr1 {a1} {b1} {c1} {f1} {g1} | t0 | t0 | t0 | _ | _ = begin
+                    id1 A a
+                ≈↑⟨ idL ⟩
+                    id1 A a o id1 A a
+                ∎
+          distr1 {a1} {b1} {c1} {f1} {g1} | t1 | t1 | t1 | _ | _ = begin
+                    id1 A b
+                ≈↑⟨ idL ⟩
+                    id1 A b o id1 A b
+                ∎
+          distr1 {a1} {b1} {c1} {f1} {g1} | t1 | t0 | t0 | _ | _ = begin
+                    nil none
+                ≈↑⟨ nil-idR none ⟩
+                    id1 A a o nil none
+                ∎
+          distr1 {a1} {b1} {c1} {f1} {g1} | t1 | t1 | t0 | _ | _ = begin
+                    nil none
+                ≈↑⟨ nil-idL none ⟩
+                    nil none o id1 A b
+                ∎
+          distr1 {a1} {b1} {c1} {f1} {g1} | t0 | t1 | t0 | _ | _ = begin
+                    id1 A a
+                ≈↑⟨ nil-id none ⟩
+                    nil none
+                ≈↑⟨ nil-idL none ⟩
+                    nil none o _
+                ∎
+          distr1 {a1} {b1} {c1} {f1} {g1} | t1 | t0 | t1 | _ | _ = begin
+                    id1 A b
+                ≈↑⟨ nil-id none ⟩
+                    nil none
+                ≈↑⟨ nil-idR none ⟩
+                    _ o nil none
+                ∎
+          distr1 {a1} {b1} {c1} {f1} {g1} | t0 | t0 | t1 | _ | _ =  begin
+                    {!!}
+                ≈⟨ {!!} ⟩
+                    {!!} o id1 A a
+                ∎
+          distr1 {a1} {b1} {c1} {f1} {g1} | t0 | t1 | t1 | _ | _ = {!!}
+
+
+
+
+
+
+---  Equalizer
+---                     f
+---          e       -----→
+---     c -----→  a         b
+---     ^      /     -----→
+---     |k   h          g
+---     |   /
+---     |  /            ^
+---     | /             |
+---     |/              | Γ
+---     d _             |
+---      |\             |
+---        \ K          af
+---         \       -----→
+---          \    t0        t1
+---                  -----→
+---                     ag
+---      
+---      
+
+open Complete
+open Limit
+open NTrans
+
+equlimit : {c₁ c₂ ℓ : Level} (A I : Category c₁ c₂ ℓ) {a b : Obj A} -> (f g : Hom A a b)  (comp : Complete A I) -> 
+         Hom A ( limit-c comp ({!!} )) a
+equlimit A I f g comp = {!!}
+
+lim-to-equ :  {c₁ c₂ ℓ : Level} (A I : Category c₁ c₂ ℓ) 
+      (comp : Complete A I)
+        →  {a b : Obj A}      (f g : Hom A  a b )
+        → IsEqualizer A (equlimit A I f g comp ) f g
+lim-to-equ {c₁} {c₂} {ℓ} A I comp {a} {b} f g =  record {
+        fe=ge =  {!!}
+        ; k = λ {d} h fh=gh → k {d} h fh=gh
+        ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh
+        ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k'
+     } where
+         open  ≈-Reasoning A
+         Γ : Functor I A
+         Γ = {!!} 
+         eqlim = isLimit comp Γ
+         c = {!!}
+         e = {!!}
+         k : {d : Obj A}  (h : Hom A d a) → A [ A [ f  o  h ] ≈ A [ g  o h ] ] → Hom A d c
+         k {d} h fh=gh  = {!!}
+         ek=h :  (d : Obj A ) (h : Hom A d a ) →  ( fh=gh : A [ A [ f  o  h ] ≈ A [ g  o h ] ] )  → A [ A [ e o k h fh=gh ] ≈ h ]
+         ek=h d h fh=gh =   begin
+                    e o k h fh=gh
+                ≈⟨ {!!}  ⟩
+                    h
+                ∎
+         uniq-nat :  {i : Obj I} →  (d : Obj A )  (h : Hom A d a ) ( k' : Hom A d c ) → A [ A [ e o k' ] ≈ h ] → A [ A [ {!!} o k' ] ≈ {!!} ]
+         uniq-nat  d h k' ek'=h =  begin
+                    {!!} o k'
+                ≈⟨⟩
+                    e o k'
+                ≈⟨ ek'=h ⟩
+                    h
+                ≈⟨⟩
+                    {!!}
+                ∎
+         uniquness :  (d : Obj A ) (h : Hom A d a ) →  ( fh=gh : A [ A [ f  o  h ] ≈ A [ g  o h ] ] )  →
+                 ( k' : Hom A d c )
+                → A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ]
+         uniquness d h fh=gh k' ek'=h =   begin
+                    k h fh=gh
+                ≈⟨  {!!}  ⟩
+                    k'
+                ∎
+
+