Mercurial > hg > Members > kono > Proof > category

annotate category-ex.agda @ 790:1e7319868d77

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Sets is CCC
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 19 Apr 2019 23:42:19 +0900
parents 3249aaddc405
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
153
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module category-ex where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 postulate c₁ c₂ ℓ : Level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 postulate A : Category c₁ c₂ ℓ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 postulate a b c : Obj A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 postulate g : Hom A a b
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 postulate f : Hom A b c
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 open Category.Category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 h = _o_ A f g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 i = A [ f o g ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18