Library Univalence.components
Embeddings
Every type is a "coproduct" of its components.
The image of a map.
The characterization of embeddings as inclusions of a subset of the components.
The characterization of univalent type families.
Expressing the result using
BAut
.
This page has been generated by
coqdoc