HoTT/HoTT — pull request #227 by JasonGross (2013-10-21 19:31:03+00:00)
Title: Port subcategories

This fixes the things Andrej pointed out yesterday, and also ports subcategories (more generally, it ports sigma types). Sigma types for categories are more properly grothendieck constructions of functors to Cat, but using this light-weight version is sometimes convenient, especially when we only care about subcategories. There's a bit more automation in this set of files, but hopefully nothing too objectionable.

Is there a standard notation for wide/full subcategories?

Next up, the category of sets, full and faithful, and the Yoneda lemma. I'm still having trouble showing that the precategory of hSets is saturated, so I'll probably have to take another look at http://arxiv.org/abs/1303.0584 or ask for help. What I have so far is at https://github.com/JasonGross/HoTT-categories/blob/univalent-set/theories/Categories/SetCategory/Morphisms.v; perhaps someone can suggest a better way to define `equiv_iso_equiv_SetCat {H : Funext} (s d : SetCat) : s ≅ d <~> (s <~> d)` than by chaining a bunch of transitivity, symmetry, issig, and `equiv_functor_sigma_id`, and then finishing with `equiv_iff_hprop`. (What I want, essentially, is that `equiv_adjointify` is an equivalence if you're defining an equivalence between `hSet`s.) Because the way that I do it makes it computationally challenging to show that the identity isomorphism goes to the identity equivalence, and vice versa.