Code

pHomotopy, pmap_postwhisker#1797

Code

Merged

Alizter merged 11 commits intoHoTT:masterHoTT/Coq-HoTT:masterfrom jdchristensen:phomotopyjdchristensen/HoTT:phomotopyCopy head branch name to clipboardJan 1, 2024

+355-395

Commits

Commits on Dec 30, 2023

• Pointed/Core: get rid of stray universe variable in pHomotopy

  jdchristensen

  committed
  8b57d0b

  Copy full SHA for 8b57d0b

• Adjust pmap_(pre/post)whisker in pHomotopy.v

  jdchristensen

  committed
  e995adb

  Copy full SHA for e995adb

• pHomotopy: remove redundant pmap_postwhisker/prewhisker

  jdchristensen

  committed
  838b936

  Copy full SHA for 838b936

• pHomotopy: remove Funext in phomotopy_hcompose

  jdchristensen

  committed
  5c0c527

  Copy full SHA for 5c0c527

• pFiber: minor clean-up to main definition

  jdchristensen

  committed
  395db1e

  Copy full SHA for 395db1e

• Pointed/Core: remove stray univ var from phomotopy_refl/symm/trans

  jdchristensen

  committed
  bd5717d

  Copy full SHA for bd5717d

• ExactSequence: avoid some WildCat notation to improve univ vars

  Show description for 8d5039d
  jdchristensen

  committed
  8d5039d

  Copy full SHA for 8d5039d

Commits on Jan 1, 2024

• pHomotopy: rm unneeded results; make ishprop_phomotopy_hset only use Funext

  jdchristensen

  committed
  ed723f1

  Copy full SHA for ed723f1

• Pointed/Core: rm unneeded equiv_path_pmap_1; update comments

  jdchristensen

  committed
  eb5c4a1

  Copy full SHA for eb5c4a1

• Pointed: merge pHomotopy into Core: lots of reordering of things

  jdchristensen

  committed
  e6a719d

  Copy full SHA for e6a719d

• Remove three Local Instances that are already Global Instances

  jdchristensen

  committed
  ab2543e

  Copy full SHA for ab2543e