Mercurial > hg > Members > kono > Proof > category

changeset 426:1290d6876129

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Functor MA → A
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 26 Mar 2016 10:16:05 +0900
parents 98811e927d4a
children 531b739a1d7c
files limit-to.agda maybeCat.agda
diffstat 2 files changed, 64 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Thu Mar 24 14:49:49 2016 +0900
+++ b/limit-to.agda	Sat Mar 26 10:16:05 2016 +0900
@@ -370,6 +370,44 @@
           distr1 {t1} {t0} {t1} {_} {_} | (just arrow-f) |  (just _) = nothing
           distr1 {t1} {t0} {t1} {_} {_} | (just arrow-g) |  (just _) = nothing
 
+record  Nil {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  :  Set   ( c₁ ⊔ c₂ ⊔ ℓ ) where
+     field 
+         nil : {a b : Obj A } -> Hom A a b
+         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
+
+justFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ->  Nil A -> Functor  (MaybeCat A ) A
+justFunctor{c₁} {c₂} {ℓ} A none =  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}   -> distr2 {a} {b} {c} {f} {g}
+             ; ≈-cong = \ {a} {b} {c} {f}   -> ≈-cong  {a} {b} {c} {f}
+       }
+      } where
+          MA = MaybeCat A
+          fobj :  Obj MA -> Obj A
+          fobj = \x -> x
+          fmap :  {x y : Obj MA } ->  Hom MA x y -> Hom A x y 
+          fmap {x} {y} f with MaybeHom.hom f
+          fmap {x} {y} _ | nothing =  nil none
+          fmap {x} {y} _ | (just f)  = f
+          identity  : {x : Obj MA} -> A [ fmap (id1 MA  x) ≈ id1 A (fobj x) ]
+          identity  =  let open ≈-Reasoning (A) in  refl-hom
+          distr2 :  {a : Obj MA} {b : Obj MA} {c : Obj MA} {f : Hom MA a b} {g : Hom MA b c} → A [ fmap (MA [ g o f ]) ≈ A [ fmap g o fmap f ] ]
+          distr2 {a} {b} {c} {f} {g} with MaybeHom.hom f  | MaybeHom.hom g
+          distr2 | nothing | nothing = let open ≈-Reasoning (A) in  sym ( nil-idR none  )
+          distr2 | nothing | just ga = let open ≈-Reasoning (A) in  sym ( nil-idR none  )
+          distr2 | just fa | nothing = let open ≈-Reasoning (A) in  sym ( nil-idL none  )
+          distr2 | just f | just g   = let open ≈-Reasoning (A) in  refl-hom
+          ≈-cong : {a : Obj MA} {b : Obj MA} {f g : Hom MA a b}  →   MA [ f ≈ g ] → A [ fmap f ≈ fmap g ]
+          ≈-cong {a} {b} {f} {g} eq with MaybeHom.hom f  | MaybeHom.hom g
+          ≈-cong {a} {b} {f} {g} nothing | nothing  | nothing = let open ≈-Reasoning (A) in  refl-hom
+          ≈-cong {a} {b} {f} {g} (just eq) | just _ | just _ = eq
+
 
 
 ---  Equalizer
@@ -379,10 +417,18 @@
 ---     ^      /     ------>
 ---     |k   h          g
 ---     |   /
----     |  /
----     | /
----     |/
----     d
+---     |  /            ^
+---     | /             |
+---     |/              | Γ
+---     d _             |
+---      |\             |
+---        \ K          af
+---         \        ------>
+---          \     t0        t1
+---                  ------>
+---                     ag
+---      
+---      
 
 open Limit
 
@@ -410,7 +456,10 @@
          mg = record { hom = just g }
          Γ = indexFunctor  {c₁} {c₂} {ℓ} A  a b f g
          nmap :  (x : Obj I ) ( d : Obj (MA)  ) (h : Hom MA d a ) -> Hom MA (FObj (K MA I d) x) (FObj Γ x)
-         nmap x d h = {!!}
+         nmap x d h with x | MaybeHom.hom h
+         ... | _  | nothing = record { hom = nothing  }
+         ... | t0 | just jh = record { hom = just jh }
+         ... | t1 | just jh = record { hom = just ( A [ f o  jh ] ) }
          commute1 : {x y : Obj I}  {f' : Hom I x y} (d : Obj MA) (h : Hom MA d a ) ->  MA [ MA [ mf  o  h ] ≈ MA [ mg  o h ] ]
                  → MA [ MA [ FMap Γ f' o nmap x d h ] ≈ MA [ nmap y d h o FMap (K MA I d) f' ] ]
          commute1  {x} {y} {f'} d h fh=gh = {!!}
@@ -422,7 +471,9 @@
             }
           }
          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 )
+         k {d} h fh=gh  with MaybeHom.hom ( limit (lim Γ  {c} {nat c (record { hom = just e}) (just fe=ge) }) d (nat d (record { hom = just h }) (just fh=gh) ) )
+         k {d} h fh=gh  | nothing = {!!}
+         k {d} h fh=gh  | just f =   f
          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 ] ] )  ->
--- a/maybeCat.agda	Thu Mar 24 14:49:49 2016 +0900
+++ b/maybeCat.agda	Sat Mar 26 10:16:05 2016 +0900
@@ -74,6 +74,8 @@
         _∎ _ = relTo ≡≡-refl
 
 
+
+
 MaybeCat : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) -> Category   c₁ (ℓ ⊔ c₂)  (ℓ ⊔ c₂)
 MaybeCat { c₁} {c₂} {ℓ} ( A ) =   record {
     Obj  = Obj A  ;
@@ -117,3 +119,8 @@
         associative  {_} {_} {_} {_} {f} {g} {h}  | just _ | just _ | nothing = nothing
         associative  {a} {b} {c} {d} {_} {_} {_}  | just f | just g | just h = 
              just ( IsCategory.associative ( Category.isCategory A )  {a} {b} {c} {d} {f} {g} {h}  )
+
+≈-to-== : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ->  { a b :  Obj A }
+    { f g : Hom A a b } ->
+    A [ f ≈ g ] -> (MaybeCat A) [  record { hom = just f } ≈  record { hom = just g } ]
+≈-to-==  A {a} {b} {f} {g} f≈g =  just f≈g