Mercurial > hg > Members > kono > Proof > category

annotate freyd.agda @ 307:9872bddec072

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
small full subcategory done.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 05 Jan 2014 18:51:44 +0900
parents 92475fe5f59e
children 7f00cd09274c
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