Mercurial > hg > Members > kono > Proof > category

view limit-to.agda @ 410:508c88223aab

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add reasoning
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 23 Mar 2016 11:16:16 +0900
parents cb03612d8162
children f04b2fb91432
line wrap: on
line source

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

module limit-to where

open import cat-utility
open import HomReasoning
open import Relation.Binary.Core
open import Data.Maybe
open Functor




-- If we have limit then we have equalizer                                                                                                                                                                  
---  two objects category
---
---          f
---       ------>
---     0         1
---       ------>
---          g



data  TwoObject {c₁ : Level}  : Set c₁ where
   t0 : TwoObject 
   t1 : TwoObject 


-- arrow composition


_×_ :  ∀ { c₁  c₂ }  -> {A B C : TwoObject { c₁} } →  Maybe ( TwoObject   { c₂ }) →  Maybe ( TwoObject    { c₂ })  →  Maybe ( TwoObject  { c₂ })  
_×_   nothing _  = nothing
_×_   (just _) nothing  = nothing
_×_   { c₁} { c₂} {t1} {t1} {t1} _ f   =  f
_×_   { c₁} { c₂} {t0} {t1} {t1} _ f   =  f
_×_   { c₁} { c₂} {t0} {t0} {t0} _ f   =  f
_×_   { c₁} { c₂} {t0} {t0} {t1} f _   =  f
_×_   { c₁} { c₂} {a} {b} {c} (just f)  (just g)   =  nothing


_==_ :  ∀{ c₂ }  ->  Rel (Maybe (TwoObject  { c₂ })) (c₂) 
_==_   =  Eq   _≡_ 

==refl :  ∀{ c₂ } ->  ∀ {x : Maybe (TwoObject  { c₂ })} → _==_ x x
==refl {_} {just x}  = just refl
==refl {_} {nothing} = nothing

==sym :  ∀{ c₂ } -> ∀ {x y :  Maybe (TwoObject  { c₂ })} → _==_ x  y → _==_ y  x
==sym (just x≈y) = just (≡-sym x≈y)
==sym nothing    = nothing

==trans :  ∀{ c₂ } -> ∀ {x y z :   Maybe (TwoObject  { c₂ }) } → _==_ x  y → _==_ y  z → _==_ x  z
==trans (just x≈y) (just y≈z) = just (≡-trans x≈y y≈z)
==trans nothing    nothing    = nothing

module ==-Reasoning { c₁ c₂ : Level} where

        infixr  2 _∎
        infixr 2 _==⟨_⟩_ _==⟨⟩_
        infix  1 begin_


        data _IsRelatedTo_   (x y : (Maybe (TwoObject  { c₂ }))) :
                             Set  c₂ where
            relTo : (x≈y : x  == y  ) → x IsRelatedTo y

        begin_ :  {x : Maybe (TwoObject  { c₂ }) } {y : Maybe (TwoObject  { c₂ })} →
                   x IsRelatedTo y →  x ==  y 
        begin relTo x≈y = x≈y

        _==⟨_⟩_ :  (x :  Maybe (TwoObject  { c₂ })) {y z :  Maybe (TwoObject  { c₂ }) } →
                    x == y  → y IsRelatedTo z → x IsRelatedTo z
        _ ==⟨ x≈y ⟩ relTo y≈z = relTo (==trans x≈y y≈z)

        _==⟨⟩_ :  (x : Maybe (TwoObject  { c₂ })) {y : Maybe (TwoObject  { c₂ })} 
                    → x IsRelatedTo y → x IsRelatedTo y
        _ ==⟨⟩ x≈y = x≈y

        _∎ :  (x :  Maybe (TwoObject  { c₂ })) → x IsRelatedTo x
        _∎ _ = relTo ==refl



--          f    g    h
--       d <- c <- b <- a

assoc-× :   { c₁  c₂ : Level } {a b c d : TwoObject  { c₁} } {f g h : Maybe (TwoObject  { c₂ })} → 
      (  _×_ { c₁} { c₂} {a} {b} {d} f ( _×_ { c₁} { c₂} {a} {b} {c} g h )  ) ==
                (  _×_ { c₁} { c₂} {a} {c} {d}  ( _×_ { c₁} { c₂} {b} {c} {d} f g )   h )
--    ( f × (g × h)) == ((f × g) × h )
assoc-× {_} {_} {_} {_} {_} {_} {nothing} {_} {_} = nothing
assoc-× {_} {_} {_} {_} {_} {_} {just _} {nothing} {_} = nothing
assoc-× {_} {_} {t0} {t0} {t0} {t0} {just _} {just _} {nothing} = nothing
assoc-× {_} {_} {t0} {t0} {t0} {t1} {just _} {just _} {nothing} = nothing
assoc-× {_} {_} {t0} {t0} {t1} {t0} {just _} {just _} {nothing} = nothing
assoc-× {_} {_} {t0} {t0} {t1} {t1} {just _} {just _} {nothing} = nothing
assoc-× {_} {_} {t0} {t1} {t0} {t0} {just _} {just _} {nothing} = nothing
assoc-× {_} {_} {t0} {t1} {t0} {t1} {just _} {just _} {nothing} = nothing
assoc-× {_} {_} {t0} {t1} {t1} {t0} {just _} {just _} {nothing} = nothing
assoc-× {_} {_} {t0} {t1} {t1} {t1} {just _} {just _} {nothing} = nothing
assoc-× {_} {_} {t1} {t0} {t0} {t0} {just _} {just _} {nothing} = nothing
assoc-× {_} {_} {t1} {t0} {t0} {t1} {just _} {just _} {nothing} = nothing
assoc-× {_} {_} {t1} {t0} {t1} {t0} {just _} {just _} {nothing} = nothing
assoc-× {_} {_} {t1} {t0} {t1} {t1} {just _} {just _} {nothing} = nothing
assoc-× {_} {_} {t1} {t1} {t0} {t0} {just _} {just _} {nothing} = nothing
assoc-× {_} {_} {t1} {t1} {t0} {t1} {just _} {just _} {nothing} = nothing
assoc-× {_} {_} {t1} {t1} {t1} {t0} {just _} {just _} {nothing} = nothing
assoc-× {_} {_} {t1} {t1} {t1} {t1} {just _} {just _} {nothing} = nothing
assoc-× {_} {_} {t0} {t0} {t0} {t0} {just _} {just _} {just _} = just refl
assoc-× {_} {_} {t0} {t0} {t0} {t1} {just _} {just _} {just _} = just refl
assoc-× {_} {_} {t0} {t1} {t1} {t1} {just _} {just _} {just _} = just refl
assoc-× {_} {_} {t1} {t1} {t1} {t1} {just _} {just _} {just _} = just refl
assoc-× {_} {_} {t0} {t0} {t1} {t0} {just _} {just _} {just _} =  {!!}
assoc-× {_} {_} {t0} {t0} {t1} {t1} {just t0} {just t0} {just t0} = just refl
assoc-× {_} {_} {t0} {t0} {t1} {t1} {just t0} {just t1} {just t0} = just refl
assoc-× {_} {_} {t0} {t0} {t1} {t1} {just t1} {just t0} {just t1} = just refl
assoc-× {_} {_} {t0} {t0} {t1} {t1} {just t1} {just t1} {just t1} = just refl
assoc-× {_} {_} {t0} {t0} {t1} {t1} {just t1} {just t1} {just t0} = {!!}
assoc-× {_} {_} {t0} {t0} {t1} {t1} {just t1} {just t0} {just t0} = {!!}
assoc-× {_} {_} {t0} {t0} {t1} {t1} {just t0} {just t1} {just t1} = {!!}
assoc-× {_} {_} {t0} {t0} {t1} {t1} {just t0} {just t0} {just t1} = {!!}
assoc-× {_} {_} {t0} {t1} {t0} {t0} {just _} {just _} {just _} = nothing
assoc-× {_} {_} {t0} {t1} {t0} {t1} {just _} {just _} {just _} = nothing
assoc-× {_} {_} {t0} {t1} {t1} {t0} {just _} {just _} {just _} = nothing
assoc-× {_} {_} {t1} {t0} {t0} {t0} {just _} {just _} {just _} = nothing
assoc-× {_} {_} {t1} {t0} {t0} {t1} {just _} {just _} {just _} = nothing
assoc-× {_} {_} {t1} {t0} {t1} {t0} {just _} {just _} {just _} = nothing
assoc-× {_} {_} {t1} {t0} {t1} {t1} {just _} {just _} {just _} = {!!}
assoc-× {_} {_} {t1} {t1} {t0} {t0} {just _} {just _} {just _} = nothing
assoc-× {_} {_} {t1} {t1} {t0} {t1} {just _} {just _} {just _} = nothing
assoc-× {_} {_} {t1} {t1} {t1} {t0} {just _} {just _} {just _} = nothing




TwoId :  { c₁  c₂ : Level } {a : TwoObject  { c₁} } ->  Maybe (TwoObject  { c₂ })
TwoId {_} {_} {_} = just t0


open import maybeCat  


open import Relation.Binary 
TwoCat : { c₁ c₂ ℓ : Level  } ->  Category   c₁  c₂  c₂
TwoCat   {c₁}  {c₂} {ℓ} = record {
    Obj  = TwoObject  {c₁} ;
    Hom = λ a b →    Maybe ( TwoObject  { c₂ } ) ;
    _o_ =  \{a} {b} {c} x y -> _×_ { c₁ } {  c₂} {a} {b} {c} x y ;
    _≈_ =    Eq  _≡_   ;
    Id  =  \{a} -> TwoId { c₁ } {  c₂} {a} ;
    isCategory  = record {
            isEquivalence =  record {refl = ==refl ; trans = ==trans ; sym = ==sym } ;
            identityL  = {!!} ;
            identityR  = {!!} ;
            o-resp-≈  =  {!!} ;
            associative  = assoc-×
       } 
   } 

indexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj (MaybeCat A )) ( f g : Hom A a b ) ->  Functor (TwoCat {c₁} {c₂} {c₂} ) (MaybeCat 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
          I = TwoCat  {c₁} {c₂} {ℓ}
          MA = MaybeCat A
          open ≈-Reasoning (MA)
          fobj :  Obj I -> Obj A
          fobj t0 = a
          fobj t1 = b
          fmap :  {x y : Obj I } ->  Maybe (TwoObject  {c₂} ) -> Hom MA (fobj x) (fobj y)
          fmap {t0} {t1} (just t0) = record { hom = just f }
          fmap {t0} {t1} (just t1) = record { hom = just g }
          fmap {t0} {t0} (just t0)  = record { hom = just ( id1 A a )}
          fmap {t1} {t1} (just t0)  = record { hom = just ( id1 A b )}
          fmap {_} {_}   _ = record { hom = nothing }
          open ≈-Reasoning (A) 
          identity :  {x : Obj I} → {!!}
          identity {t0}  =  {!!}
          identity {t1}  =  {!!}
          distr1 : {a₁ : Obj I} {b₁ : Obj I} {c : Obj I} {f₁ : Hom I a₁ b₁} {g₁ : Hom I b₁ c} → {!!}
          distr1 {a1} {b1} {c} {f1} {g1}   = {!!}
          ≈-cong :   {a : Obj I} {b : Obj I} {f g : Hom I a b}  → _[_≈_] I f g → {!!}
          ≈-cong   {_} {_} {f1} {g1} f≈g = {!!}


---  Equalizer
---                     f
---          e       ------>
---     c ------>  a         b
---     ^      /     ------>
---     |k   h          g
---     |   / 
---     |  / 
---     | /  
---     |/  
---     d  

open Limit

lim-to-equ :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  ->
      (lim : (I : Category c₁ c₂ ℓ) ( Γ : Functor I A ) → { a0 : Obj A } { u : NTrans I A ( K A I a0 ) Γ } → Limit A I Γ a0 u ) -- completeness
        →  {a b c : Obj A}      (f g : Hom A  a b ) 
        → (e : Hom A c a ) → (fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] ) → Equalizer A e f g
lim-to-equ  {c₁} {c₂} {ℓ } A  lim {a} {b} {c}  f g e 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₂} {ℓ }
         Γ = {!!}
         nmap :  (x : Obj I) ( d : Obj A ) (h : Hom A d a ) -> Hom A (FObj (K A I d) x) (FObj Γ x)
         nmap x d h = {!!}
         commute1 : {x y : Obj I}  {f' : Hom I x y} (d : Obj A) (h : Hom A d a ) ->  A [ A [ f  o  h ] ≈ A [ g  o h ] ] 
                 → A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K A I d) f' ] ]
         commute1  {x} {y} {f'} d h fh=gh = {!!}
         nat : (d : Obj A) → (h : Hom A d a ) →  A [ A [ f  o  h ] ≈ A [ g  o h ] ]   → NTrans I A (K A I d) Γ
         nat d h fh=gh = record {
            TMap = λ x → nmap x d h ; 
            isNTrans = record {
                commute = λ {x} {y} {f'} -> commute1 {x} {y} {f'} d h fh=gh 
            }
          }
         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  = {!!} -- limit (lim I Γ  {c} {nat c e fe=ge }) d (nat 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 = {!!}
         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 = {!!}