# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1588355844 -32400
# Node ID 4105fabbadd63355e7e93edf85b23f0e5858b9a2
# Parent  549933e6797848ee8ab452d9819630b155e697aa
giving up non small graph

diff -r 549933e67978 -r 4105fabbadd6 CCCGraph.agda
--- 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