Code

connectivity of wedge inclusion#2211

Code

Merged

Alizter merged 11 commits intoHoTT:masterHoTT/Coq-HoTT:masterfrom Alizter:ps/rr/connectivity_of_wedge_inclusionAlizter/HoTT:ps/rr/connectivity_of_wedge_inclusionCopy head branch name to clipboardMar 15, 2025

Commits

Commits on Mar 13, 2025

• connectivity of wedge inclusion

  Show description for f87c8a1
  Alizter

  committed
  f87c8a1

  Copy full SHA for f87c8a1

• factor wedge connectivity into two parts

  Show description for fb71b5f
  Alizter

  committed
  fb71b5f

  Copy full SHA for fb71b5f

Commits on Mar 14, 2025

• Connectedness: fix heading

  jdchristensen

  committed
  69cf2ff

  Copy full SHA for 69cf2ff

• Wedge: use wglue in wedge_inr to make it unfold better

  jdchristensen

  committed
  4d9375c

  Copy full SHA for 4d9375c

• Wedge: factor out wedge_rec_beta_inl/r from hasbinarycoproducts

  jdchristensen

  committed
  a438e29

  Copy full SHA for a438e29

• Wedge: minor cleanups to some proofs

  jdchristensen

  committed
  18fe59a

  Copy full SHA for 18fe59a

• Wedge: simplify extension_wedge_incl and conn_map_wedge_incl

  jdchristensen

  committed
  7fa7e86

  Copy full SHA for 7fa7e86

Commits on Mar 15, 2025

• remove minimization ToSet, annotate some defs and simplify proofs

  Show description for 0a275cb
  Alizter

  committed
  0a275cb

  Copy full SHA for 0a275cb

• Wedge: get rid of WildCat notations to improve universe variables

  jdchristensen

  committed
  9b11fd3

  Copy full SHA for 9b11fd3

• Wedge: minor changes

  jdchristensen

  committed
  60201bf

  Copy full SHA for 60201bf

• Wedge: remove universe annotation from hasallcoproducts_ptype

  jdchristensen

  committed
  fee411c

  Copy full SHA for fee411c