Mercurial > hg > Members > kono > Proof > category

changeset 908:4105fabbadd6 non-small-graph

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
giving up non small graph
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 02 May 2020 02:57:24 +0900
parents 549933e67978
children d6f71c3a69d9
files CCCGraph.agda
diffstat 1 files changed, 1 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Fri May 01 19:26:54 2020 +0900
+++ b/CCCGraph.agda	Sat May 02 02:57:24 2020 +0900
@@ -321,6 +321,7 @@
 record CCCObj { c₁ c₂ ℓ  : Level} : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
    field
      cat : Category c₁ c₂ ℓ
+     csmall : {a b : Obj cat } → { f g : Hom cat a b } → cat [ f ≈ g ] → f ≡ g
      ccc : CCC cat
  
 open CCCObj