Mercurial > hg > Members > kono > Proof > category

changeset 304:bd7b3f3d1d4c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Freyd Adjoint Functor Theorem
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 05 Jan 2014 08:46:31 +0900
parents 7f40d6a51c72
children 211f6bec9b4a
files freyd.agda
diffstat 1 files changed, 14 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/freyd.agda	Sun Jan 05 08:46:31 2014 +0900
@@ -0,0 +1,14 @@
+open import Category -- https://github.com/konn/category-agda                                                                                     
+open import Level
+open import Category.Sets
+
+module freyd {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
+     (C : Category zero zero zero )
+  where
+
+open import Relation.Binary.Core
+
+postulate ≈→≡ : {a b : Obj C } { x y : Hom C a b } →  (x≈y : C [ x ≈ y  ]) → x ≡ y
+
+
+-- record SmallCategory