Mercurial > hg > Members > kono > Proof > category

annotate freyd.agda @ 308:7f00cd09274c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
pre-initial
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 05 Jan 2014 19:02:29 +0900
parents 9872bddec072
children e213595b845e
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
304
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Category -- https://github.com/konn/category-agda
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Level
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Category.Sets
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 module freyd {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 where
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
307
9872bddec072 small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 306
diff changeset
8 open import cat-utility
304
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Relation.Binary.Core
307
9872bddec072 small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 306
diff changeset
10 open Functor
304
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
306
92475fe5f59e Small Full Subcategory (underconstruction)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 305
diff changeset
12 -- C is small full subcategory of A
304
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
307
9872bddec072 small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 306
diff changeset
14 record SmallFullSubcategory {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
9872bddec072 small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 306
diff changeset
15 (F : Functor A A ) ( FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b )
9872bddec072 small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 306
diff changeset
16 : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
306
92475fe5f59e Small Full Subcategory (underconstruction)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 305
diff changeset
17 field
307
9872bddec072 small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 306
diff changeset
18 ≈→≡ : {a b : Obj A } → { x y : Hom A (FObj F a) (FObj F b) } →
9872bddec072 small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 306
diff changeset
19 (x≈y : A [ FMap F x ≈ FMap F y ]) → FMap F x ≡ FMap F y -- co-comain of FMap is local small
9872bddec072 small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 306
diff changeset
20 full→ : { a b : Obj A } { x : Hom A (FObj F a) (FObj F b) } → A [ FMap F ( FMap← x ) ≈ x ]
9872bddec072 small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 306
diff changeset
21 full← : { a b : Obj A } { x : Hom A a b } → A [ FMap← ( FMap F x ) ≈ x ]
305
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 304
diff changeset
22
308
7f00cd09274c pre-initial
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 307
diff changeset
23 record PreInitial-SmallFullSubcategory {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
7f00cd09274c pre-initial
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 307
diff changeset
24 (F : Functor A A ) ( FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b )
7f00cd09274c pre-initial
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 307
diff changeset
25 (SFS : SmallFullSubcategory A F FMap← ) : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
7f00cd09274c pre-initial
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 307
diff changeset
26 field
7f00cd09274c pre-initial
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 307
diff changeset
27 pre-initial : ∀{ a : Obj A } → { a' : Obj A } → Hom A ( FObj F a' ) a
7f00cd09274c pre-initial
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 307
diff changeset
28 uniqueness : ∀{ a : Obj A } → { a' : Obj A } → ( f' : Hom A ( FObj F a' ) a ) →
7f00cd09274c pre-initial
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 307
diff changeset
29 A [ f' ≈ pre-initial {a} {a'} ]
7f00cd09274c pre-initial
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 307
diff changeset
30