Mercurial > hg > Members > kono > Proof > category

changeset 662:e1d54c0f73a7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
move InitialObject to cat-utility
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 12 Aug 2017 16:35:58 +0900
parents 04ffb37df2af
children 855e497a9c8f
files cat-utility.agda freyd2.agda limit-to.agda
diffstat 3 files changed, 8 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/cat-utility.agda	Wed Jul 19 22:27:35 2017 +0900
+++ b/cat-utility.agda	Sat Aug 12 16:35:58 2017 +0900
@@ -378,3 +378,11 @@
           limit-u :  ( Γ : Functor I A ) ->  NTrans I A ( K A I (limit-c Γ )) Γ
           limit-u  Γ  = t0 ( climit Γ)
 
+
+-- initial object
+
+        record HasInitialObject {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (i : Obj A) : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
+          field
+             initial :  ∀( a : Obj A ) →  Hom A i a
+             uniqueness  : { a : Obj A } →  ( f : Hom A i a ) → A [ f ≈  initial a ]
+
--- a/freyd2.agda	Wed Jul 19 22:27:35 2017 +0900
+++ b/freyd2.agda	Sat Aug 12 16:35:58 2017 +0900
@@ -80,7 +80,6 @@
          reprId←  :  {x : Obj A} →  Sets [ Sets [ TMap repr← x  o  TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)]
 
 open Representable
-open import freyd
 
 _↓_ :  { c₁ c₂ ℓ : Level}  { c₁' c₂' ℓ' : Level} { A : Category c₁ c₂ ℓ } { B : Category c₁' c₂' ℓ' }
     →  ( F G : Functor A B )
@@ -88,9 +87,7 @@
 _↓_   { c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'}  { A } { B } F G  = CommaCategory
          where open import Comma1 F G
 
-open SmallFullSubcategory
 open Complete
-open PreInitial
 open HasInitialObject
 open import Comma1
 open CommaObj
@@ -241,9 +238,6 @@
 
 -- A is complete and K{*}↓U has preinitial full subcategory and U preserve limit then U is representable
 
-open SmallFullSubcategory
-open PreInitial
-
 -- if U preserve limit,  K{*}↓U has initial object from freyd.agda
 
 ≡-cong = Relation.Binary.PropositionalEquality.cong
@@ -374,8 +368,6 @@
 
 module Adjoint-Functor {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I )
      (U : Functor A B )
-     (SFS : (b : Obj B) → SmallFullSubcategory ((K B A b) ↓ U) )  
-     (PI :  (b : Obj B) → PreInitial (K B A b ↓ U)  (SFSF (SFS b))) 
      ( i :  (b : Obj B) → Obj ( K B A b ↓ U) )
      (In :  (b : Obj B) → HasInitialObject ( K B A b ↓ U) (i b) ) 
      (LP :  LimitPreserve A I B U  ) where
--- a/limit-to.agda	Wed Jul 19 22:27:35 2017 +0900
+++ b/limit-to.agda	Sat Aug 12 16:35:58 2017 +0900
@@ -51,7 +51,6 @@
       } 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