Mercurial > hg > Members > kono > Proof > category

--- a/limit-to.agda	Fri Jun 26 19:38:57 2015 +0900
+++ b/limit-to.agda	Sat Mar 05 07:20:03 2016 +0900
@@ -13,6 +13,10 @@
 open import Data.Nat hiding ( _⊔_ ) renaming ( suc to succ )
 open import Data.Bool

+open import Data.Fin as Fin
+  using (Fin; Fin′; #_; toℕ) renaming (_ℕ-ℕ_ to _-_ ; zero to Fzero ; suc to Fsuc )
+
+

 -- If we have limit then we have equalizer
 ---  two objects category
@@ -24,127 +28,23 @@
 ---          g


-infixr 40 _::_
-data  List {a} (A : Set a)  : Set a where
-   [] : List A
-   _::_ : A -> List A -> List A
-
-nat-equal : ℕ -> ℕ -> Bool
-nat-equal zero zero = true
-nat-equal (succ _) zero = false
-nat-equal zero (succ _) = false
-nat-equal (succ x) (succ y) = nat-equal x y
-
-memberp :  ℕ  ->  List  ℕ  → Bool
-memberp _ []  = false
-memberp x (y :: T) with nat-equal x y
-... | true = true
-... | false = memberp x T
-
-memberp1 :  ℕ  ->  List  ℕ  → Bool
-memberp1 _ []  = false
-memberp1 x (y :: T) with compare x y
-memberp1 x (.x :: T)  | equal .x = true
-memberp1 x ( .(succ (x + y)) :: T)  | less .x y = memberp1 x T
-memberp1 .(succ (x + y)) ( x :: T)  | greater .x y = memberp1 x T
+data TwoObject {c₁}  : Set c₁ where
+   t0 : TwoObject
+   t1 : TwoObject


--- Category object configuration
-
-data Two   : Set c₁ where
-   t0 : Two
-   t1 : Two
-
-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
-
-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 =  af :: ag :: []
-hom t1 t0 =  []
-hom t1 t1 =  id-1 :: []
+record TwoCat  {ℓ c₁ c₂ : Level  } (Two : Category  c₁ c₂ ℓ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
+    field
+         hom→ : Obj Two  -> TwoObject {ℓ}
+         hom← : TwoObject {ℓ} -> Obj Two
+         hom-iso : {a : Obj Two} -> hom← ( hom→ a) ≡ a
+         hom-rev : {a : TwoObject {ℓ} } -> hom→ ( hom← a) ≡ a

-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 }
-
--- arrow composition
-
-_×_ :  {A B C : Two} → Two-Hom B C → Two-Hom A B → Two-Hom A C
-_×_  {t0} {t0} {t0} a b  = record { Map = id-0; isMap = refl }
-_×_  {t0} {t0} {t1} a b  =  record { Map = {!!} ; isMap = refl }
-_×_  {t0} {t1} {t1} a b  =   record { Map =  {!!} ; isMap = refl }
-_×_  {t1} {t1} {t1} a b  =   record { Map = id-1; isMap = refl }
--- not happening case, but we have possible answer
-_×_  {t0} {t1} {t0} a b  =  record { Map = id-0; isMap = refl }
-_×_  {t1} {t0} {t1} a b  =  record { Map = id-1; isMap = refl }
--- non exiting arrow ( how to handle it? ) we cannot create the answer ...
-_×_  {t1} {t0} {t0} a b  = {!!}
-_×_  {t1} {t1} {t0} a b  = {!!}
-
-
-open Two-Hom
-
-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 = record {refl = refl ; trans = ≡-trans ; sym = ≡-sym};
-            identityL  = {!!} ;
-            identityR  = {!!} ;
-            o-resp-≈  = {!!} ;
-            associative  = {!!}
-       }
-   } where

 open Limit

 lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
-      (two : {!!}  )
+      (two : TwoCat A )
       (lim : ( Γ : 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₁} A I two lim {a} {b} {c} f g e fe=ge = record {
@@ -153,10 +53,10 @@
         ; ek=h = λ {d} {h} {fh=gh} → {!!}
         ; uniqueness = λ {d} {h} {fh=gh} {k'} → {!!}
      } where
-         Γobj :  Two  → Obj A
+         Γobj :  {!!}  → Obj A
          Γobj t0 = a
          Γobj t1 = b
-         Γmap :  Two  → Hom A a b
+         Γmap :  {!!}  → Hom A a b
          Γmap t0 = f
          Γmap t1 = g
          Γ : Functor I A
--- a/pullback.agda	Fri Jun 26 19:38:57 2015 +0900
+++ b/pullback.agda	Sat Mar 05 07:20:03 2016 +0900
@@ -175,7 +175,7 @@

 --------------------------------
 --
--- Contancy Functor
+-- Constancy Functor

 KI : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) →  Functor A ( A ^ I )
 KI { c₁'} {c₂'} {ℓ'} I = record {