Commit Graph

2 Commits

Author SHA1 Message Date
Dan Frumin 5e4091409d The underlying type need not be an hset for the splitting lemma 2017-08-24 16:36:59 +02:00
Dan Frumin ae60ac0146 LEM <~> all K-finite hsets are projective
and LEMoo -> all K-finite objects (not just hsets) are projective
2017-08-16 17:37:12 +02:00