Mercurial > hg > Members > kono > Proof > category

changeset 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
files freyd.agda
diffstat 1 files changed, 8 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/freyd.agda	Sun Jan 05 08:46:31 2014 +0900
+++ b/freyd.agda	Sun Jan 05 09:52:13 2014 +0900
@@ -8,7 +8,14 @@
 
 open import Relation.Binary.Core
 
+-- C is locally small
 postulate ≈→≡ : {a b : Obj C } { x y : Hom C a b } →  (x≈y : C [ x ≈ y  ]) → x ≡ y
 
+infix 4 _⊆_ _⊇_ 
 
--- record SmallCategory 
+_⊆_ : ∀ {ℓ₁ ℓ₂} → Set ℓ₁ → Set ℓ₂ → Set _
+P ⊆ Q = ∀ {x : P} →  {y : Q } → x ≡ y
+
+_⊇_ : ∀ {ℓ₁ ℓ₂} → Set ℓ₁ → Set ℓ₂ → Set _
+Q ⊇ P = ∀ {x : P} →  {y : Q } → x ≡ y
+