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.
I have hyperlinked induction on identity, but please check if thatâ€™s what you need here.
One should also be able to define the additional dagger categories:
A skeletal dagger category is a dagger precategory for which the canonical function $(A = B) \to \vert A \cong^\dagger B \vert$ is an equivalence.
A strict dagger category is a dagger precategory whose type of objects is 0-truncated. (these are the dagger categories in set-theoretic foundations)
A gaunt dagger category is a strict univalent dagger category, or equivalently a skeletal univalent dagger category.
1 to 5 of 5