Homotopy Type Theory
wedge sum > history (Rev #6, changes)
Showing changes from revision #5 to #6:
Added | Removed | Changed
Idea
We can stick two spaces together by their points.
Definition
The wedge sum of two pointed types and can be defined as the higher inductive type with the following constructors:
- Points come from the sum type?
- And their base point is glued Clearly this is pointed.
The wedge sum of two types and , can also be defined as the pushout of the span
where the maps pick the base points of and . This pushout is denoted and has basepoint
References
HoTT book
Revision on June 9, 2022 at 05:36:17 by
Anonymous?.
See the history of this page for a list of all contributions to it.