Mercurial > hg > Members > kono > Proof > category

annotate freyd.agda @ 305:211f6bec9b4a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
subset
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 05 Jan 2014 09:52:13 +0900
parents bd7b3f3d1d4c
children 92475fe5f59e
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 (C : Category zero zero zero )
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 where
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Relation.Binary.Core
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
305
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 304
diff changeset
11 -- C is locally small
304
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 postulate ≈→≡ : {a b : Obj C } { x y : Hom C a b } → (x≈y : C [ x ≈ y ]) → x ≡ y
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
305
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 304
diff changeset
14 infix 4 _⊆_ _⊇_
304
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
305
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 304
diff changeset
16 _⊆_ : ∀ {ℓ₁ ℓ₂} → Set ℓ₁ → Set ℓ₂ → Set _
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 304
diff changeset
17 P ⊆ Q = ∀ {x : P} → {y : Q } → x ≡ y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 304
diff changeset
18
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 304
diff changeset
19 _⊇_ : ∀ {ℓ₁ ℓ₂} → Set ℓ₁ → Set ℓ₂ → Set _
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 304
diff changeset
20 Q ⊇ P = ∀ {x : P} → {y : Q } → x ≡ y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 304
diff changeset
21