Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Thanks! I have added cross-links to internal presheaf.
Thanks Ingo, this sort of stuff is great to have! I changed the action to be (by default) a term in context rather than a single term of dependent product type, since the latter only makes sense when the ambient category is lccc, but the former makes sense for only finitely complete.
1 to 3 of 3