On the Eckmann-Hilton argument in homotopy type theory:
higher inductive type
initial algebra over an endofunctor
W-type
Last revised on July 28, 2021 at 16:03:14. See the history of this page for a list of all contributions to it.