view discrete.agda @ 455:55a9b6177ed4

on going ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 02 Mar 2017 14:58:40 +0900
parents 2f07f4dd9a6d
children 4d97955ea419
line wrap: on
line source

open import Category -- https://github.com/konn/category-agda
open import Level

module discrete where

open import Relation.Binary.Core
open import Relation.Nullary
open import Data.Empty
open import Data.Unit
open import Data.Maybe
open import cat-utility
open import HomReasoning

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 TwoHom {c₁ c₂ : Level } : TwoObject {c₁}  → TwoObject {c₁} → Set c₂ where
   id-t0 : TwoHom t0 t0
   id-t1 : TwoHom t1 t1
   arrow-f :  TwoHom t0 t1
   arrow-g :  TwoHom t0 t1


comp :  ∀ {c₁  c₂}  → {a b c : TwoObject {c₁}} →  TwoHom {c₁} {c₂} b c  →  TwoHom {c₁} {c₂} a b   →  TwoHom {c₁} {c₂} a c 
comp {_}  {_}  {t0} {t1} {t1}  id-t1   arrow-f   =   arrow-f 
comp {_}  {_}  {t0} {t1} {t1}  id-t1   arrow-g  =   arrow-g 
comp {_}  {_}  {t1} {t1} {t1}  id-t1   id-t1    =   id-t1 
comp {_}  {_}  {t0} {t0} {t1}  arrow-f   id-t0    =   arrow-f 
comp {_}  {_}  {t0} {t0} {t1}  arrow-g   id-t0    =   arrow-g 
comp {_}  {_}  {t0} {t0} {t0}  id-t0   id-t0    =   id-t0 

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  =  comp  {c₁}  {c₂}  {a} {b} {c} f g


--          f    g    h
--       d <- c <- b <- a
--
--   It can be proved without TwoHom 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 )} →
       ( f × (g × h)) ≡ ((f × g) × h )
assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} with  f | g | h
assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} | id-t0   | id-t0   | id-t0  = refl
assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} | arrow-f | id-t0   | id-t0  = refl
assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} | arrow-g | id-t0   | id-t0  = refl
assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} | id-t1   | arrow-f | id-t0  = refl
assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} | id-t1   | arrow-g | id-t0  = refl
assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} | id-t1   | id-t1   | arrow-f = refl
assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} | id-t1   | id-t1   | arrow-g = refl
assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} | id-t1   | id-t1   | id-t1  = refl

TwoId :  {c₁  c₂ : Level } (a : TwoObject  {c₁} ) →  (TwoHom {c₁}  {c₂ } a a )
TwoId {_} {_} t0 = id-t0 
TwoId {_} {_} t1 = id-t1 

open import Relation.Binary
open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong )

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 → x  ≡ 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) } →  ((TwoId B)  × f)  ≡ f
        identityL  {c₁}  {c₂}  {a} {b} {f} with f
        identityL  {c₁}  {c₂}  {t1} {t1} | id-t1 = refl
        identityL  {c₁}  {c₂}  {t0} {t0} | id-t0 = refl
        identityL  {c₁}  {c₂}  {t0} {t1} | arrow-f = refl
        identityL  {c₁}  {c₂}  {t0} {t1} | arrow-g = refl
        identityR :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁}  {c₂ } A B) } →   ( f × TwoId A )  ≡ f
        identityR  {c₁}  {c₂}  {_} {_} {f}  with f
        identityR  {c₁}  {c₂}  {t1} {t1} | id-t1  = refl
        identityR  {c₁}  {c₂}  {t0} {t0} | id-t0 = refl
        identityR  {c₁}  {c₂}  {t0} {t1} | arrow-f = refl
        identityR  {c₁}  {c₂}  {t0} {t1} | arrow-g = refl
        o-resp-≈ :  {c₁  c₂ : Level } {A B C : TwoObject  {c₁} } {f g :  ( TwoHom {c₁}  {c₂ } A B)} {h i : ( TwoHom B C)} →
            f  ≡ g → h  ≡ i → ( h × f )  ≡ ( i × g )
        o-resp-≈  {c₁}  {c₂} {a} {b} {c} {f} {g} {h} {i}  f==g h==i  = 
          let open  ≡-Reasoning in begin
                    ( h × f )
                ≡⟨ refl ⟩
                    comp (h) (f)
                ≡⟨ cong (λ x  → comp ( h ) x )  f==g ⟩
                    comp (h) (g)
                ≡⟨ cong (λ x  → comp x ( g ) )  h==i ⟩
                    comp (i) (g)
                ≡⟨ refl ⟩
                    ( i × g )


indexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) →  Functor (TwoCat {c₁} {c₂})  A
indexFunctor  {c₁} {c₂} {ℓ} A a b f g = 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
          T = TwoCat {c₁} {c₂} 
          fobj :  Obj T → Obj A
          fobj t0 = a
          fobj t1 = b
          fmap :  {x y : Obj T } →  (Hom T x y  ) → Hom A (fobj x) (fobj y)
          fmap  {t0} {t0} id-t0 = id1 A a
          fmap  {t1} {t1} id-t1 = id1 A b
          fmap  {t0} {t1} arrow-f = f
          fmap  {t0} {t1} arrow-g = g
          ≈-cong :  {a : Obj T} {b : Obj T} {f g : Hom T a b}  → T [ f ≈ g ]  → A [ fmap f ≈ fmap g ]
          ≈-cong  {a} {b} {f} {.f} refl = let open  ≈-Reasoning A in refl-hom
          identity : (x : Obj T ) ->  A [ fmap (id1 T x) ≈  id1 A (fobj x) ]
          identity t0  = let open  ≈-Reasoning A in refl-hom
          identity t1  = let open  ≈-Reasoning A in refl-hom
          distr1 : {a : Obj T} {b : Obj T} {c : Obj T} {f : Hom T a b} {g : Hom T b c} →
               A [ fmap (T [ g o f ])  ≈  A [ fmap g o fmap f ] ]
          distr1  {a} {b} {c} {f} {g}  with f | g
          distr1  {t0} {t0} {t0} {f} {g}  | id-t0 | id-t0 = let open  ≈-Reasoning A in sym-hom idL
          distr1  {t1} {t1} {t1} {f} {g}  | id-t1 | id-t1 = let open  ≈-Reasoning A in begin 
                   id1 A b 
                ≈↑⟨ idL ⟩
                   id1 A b o id1 A b

          distr1  {t0} {t0} {t1} {f} {g}  | id-t0 | arrow-f = let open  ≈-Reasoning A in begin
                  fmap (comp arrow-f id-t0)
                ≈⟨⟩
                  fmap arrow-f 
                ≈↑⟨ idR ⟩
                   fmap arrow-f o id1 A a

          distr1  {t0} {t0} {t1} {f} {g}  | id-t0 | arrow-g = let open  ≈-Reasoning A in begin
                  fmap (comp arrow-g id-t0)
                ≈⟨⟩
                  fmap arrow-g 
                ≈↑⟨ idR ⟩
                   fmap arrow-g o id1 A a

          distr1  {t0} {t1} {t1} {f} {g}  | arrow-f | id-t1 = let open  ≈-Reasoning A in begin
                  fmap (comp id-t1 arrow-f)
                ≈⟨⟩
                  fmap arrow-f 
                ≈↑⟨ idL ⟩
                   id1 A b o  fmap arrow-f 

          distr1  {t0} {t1} {t1} {f} {g}  | arrow-g | id-t1 = let open  ≈-Reasoning A in begin
                  fmap (comp id-t1 arrow-g)
                ≈⟨⟩
                  fmap arrow-g 
                ≈↑⟨ idL ⟩
                   id1 A b o  fmap arrow-g 


---  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 : Category c₁ c₂  ℓ) {a b : Obj A} -> (f g : Hom A a b)  (comp : Complete A (TwoCat {c₁} {c₂} )) -> 
         Hom A ( limit-c comp (indexFunctor {c₁} {c₂} {ℓ} A a b f g)) a
equlimit A f g comp = {!!}

lim-to-equ :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
      (comp : Complete A (TwoCat {c₁} {c₂} ) )
        →  {a b : Obj A}      (f g : Hom A  a b )
        → (fe=ge : A [ A [ f o (equlimit A  f g comp ) ] ≈ A [ g o (equlimit A  f g comp ) ] ] ) 
        → IsEqualizer A (equlimit A  f g comp ) f g
lim-to-equ {c₁} {c₂} {ℓ} A comp {a} {b} f g fe=ge =  record {
        fe=ge =  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
         I = TwoCat {c₁} {c₂}
         Γ : Functor I A
         Γ = indexFunctor {c₁} {c₂} {ℓ} A a b f g
         eqlim = isLimit comp Γ
         c = limit-c comp Γ
         e = equlimit A f g comp
         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 = {!!} 
         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  = {!!}
         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 {!!} ≈ k' ]
         uniquness = {!!}