V8.19

Release Highlights

• Yoneda lemma using 0-groupoids by @jdchristensen in #1745
• HITs: fix inconsistencies from several HITs by @jdchristensen in #1758
• Wildcat improvements by @jdchristensen in #1766
• Associativity of Join, and lots more by @jdchristensen in #1768
• Susp is a 1-functor; Join Bool A <~> Susp A; etc. by @jdchristensen in #1771
• Naturality of join_assoc and trijoin_twist by @jdchristensen in #1783
• wildcat: show Universe is a 2-cat by @Alizter in #1778
• Join: prove unitors, triangle law, and hexagon law by @jdchristensen in #1784
• trijoin_id_sym is natural; export more from HSpace/Core by @jdchristensen in #1786
• 2-cat of pointed types by @Alizter in #1795
• Updates to EMSpace, Join/Core, HSpaces/* and other things by @jdchristensen in #1796
• pHomotopy, pmap_postwhisker by @jdchristensen in #1797
• 1-category of successor structures by @Alizter in #1799
• πₙ(Sⁿ) = Z, and other cleanups by @jdchristensen in #1800
• CayleyDickson: some cleanups, remove funext by @Alizter in #1801
• Add pmap_from_psphere_iterated_loops, and needed lemmas by @jdchristensen in #1803
• wildcat: binary products by @Alizter in #1804
• Make IsTrunc an inductive type by @jdchristensen in #1806
• symmetry and associativity of products by @Alizter in #1813
• A strengthening of Freudenthal's theorem for H-spaces by @jarlg in #1814
• add prod_0gpd_corec by @Alizter in #1815
• Hartogs: improve speed, reorganize by @jdchristensen in #1816
• Truncatedness of pointed maps and pForall by @jdchristensen in #1819
• New proof and generalization of Licata-Finster theorem by @jdchristensen in #1821
• coproduct symmetry and associativity by @Alizter in #1828
• Wedge of a family of pType by @Alizter in #1829
• Displayed Wild Categories by @gio256 in #1832
• flattening for pushouts + total space of Hopf construction by @Alizter in #1840
• Colimits and Hopf: clean up and speed up by @jdchristensen in #1843
• wedge projections by @Alizter in #1844
• pinch map of suspension by @Alizter in #1845
• functoriality of binary coproducts by @Alizter in #1847
• characterize fiber of loop-susp counit by @Alizter in #1850
• transport011: transport over 2 1-paths and lemmas about them by @Alizter in #1853
• Flattening lemma for GraphQuotient by @Alizter in #1851
• functoriality of GraphQuotient by @Alizter in #1856
• flattening lemma for Coeq, Pushout and improvements to Hopf by @Alizter in #1857
• Equivalences for displayed wild categories by @gio256 in #1859
• add universe constraints in GraphQuotient by @Alizter in #1812
• Improvements to make_equiv by @jdchristensen in #1869
• Clean-ups to Spaces/Int/ and Spaces/Pos/ by @jdchristensen in #1870
• Add instances isconnected_em' and is_minus_one_connected_pointed by @jdchristensen in #1871
• Pointed/Core and Classes/theory/groups by @jdchristensen in #1872
• HIT/quotient: fix universe variables, and uses in Classes by @jdchristensen in #1873
• Generalize quotient_kernel_factor, and use it in Ordinals.v by @jdchristensen in #1874
• Groups for a pointed wildcat, and other things about pointedness by @jdchristensen in #1876
• redefine DPath as transport and cleanup proofs by @Alizter in #1880
• Indexed products and coproducts by @gio256 in #1878
• add missing coherence for TwoOneCat by @Alizter in #1897
• Update bifunctors by @gio256 in #1886
• [Chapter 1 Exercise] Solved by @MintChocoManju in #1901
• functoriality of smash by @Alizter in #1892
• Zero-groupoid universal property for coequalizers by @gio256 in #1900

New Contributors

• @Columbus240 made their first contribution in #1776
• @khalid586 made their first contribution in #1792
• @gio256 made their first contribution in #1832
• @MintChocoManju made their first contribution in #1901

Full Changelog: V8.18...V8.19