Showing changes from revision #4 to #5:
Added | Removed | Changed
We can stick to two spaces together by their points.
The wedge sum of two pointed types and can be defined as the higher inductive type with the following constructors:
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
Revision on January 19, 2019 at 15:54:32 by Ali Caglayan. See the history of this page for a list of all contributions to it.