Code

Update bifunctors#1886

Code

Merged

jdchristensen merged 25 commits intoHoTT:masterHoTT/Coq-HoTT:masterfrom gio256:bifunctorsgio256/Coq-HoTT:bifunctorsCopy head branch name to clipboardMar 14, 2024

+446-206

Commits

Commits on Mar 8, 2024

• Move bifunctor coherence to Is1Bifunctor

  gio256

  committed
  63e3847

• WildCat/Bifunctor.v: Remove bifunctor_hom lemmas

  gio256

  committed
  783f5b9

• AbSES/BaerSum.v: fix proof of is1bifunctor_abses

  gio256

  committed
  a95509d

• WildCat/Bifunctor.v: simplify uncurried proofs

  gio256

  committed
  1046b48

• AbGroups/AbHom.v: prove is1bifunctor_ab_hom

  gio256

  committed
  62b8d2b

• AbSES/Ext.v: rough proofs of Is1Bifunctor

  gio256

  committed
  720075a

Commits on Mar 9, 2024

• AbSES/Ext.v: simplify bifunctor proofs for ab_ext

  gio256

  committed
  56d82e7

• AbSES/Ext.v: remove universe annotations

  gio256

  committed
  2c9fce6

• Simplify building of bifunctors

  gio256

  committed
  d78a876

• WildCat/Yoneda.v: Add bifunctor instances for hom

  gio256

  committed
  e19d81e

• WildCat/Prod.v: add product inclusions

  gio256

  committed
  f5e4d86

• WildCat/Bifunctor.v: remove comment

  gio256

  committed
  192a786

• AbSES/Ext.v: remove universe annotations

  gio256

  committed
  beed14d

• WildCat/Yoneda.v: add comment

  gio256

  committed
  f930232

• WildCat/Monoidal: tensor product is a 1-bifunctor

  gio256

  committed
  da5cb5a

Commits on Mar 10, 2024

• WildCat equivs: add compose_catie'

  gio256

  committed
  c41d397

• Move bifunctor lemmas from Prod.v to Bifunctor.v

  gio256

  committed
  2ae47ce

Commits on Mar 11, 2024

• WildCat/Bifunctor.v: clean up two proofs

  gio256

  committed
  1426fd9

• WildCat equivs: re-define compose_catie'

  gio256

  committed
  b662a72

Commits on Mar 12, 2024

• WildCat equivs fix: cate_homotopic to catie_homotopic

  gio256

  committed
  f902579

Commits on Mar 13, 2024

• WildCat/Yoneda.v: opyon_0gpd bifunctor instances

  gio256

  committed
  c2616da

• contrib/SetoidRewrite.v: formatting

  gio256

  committed
  07b6ff4

• WildCat/Yoneda.v: clean up is0functor_hom_0gpd

  gio256

  committed
  2ed1065

Commits on Mar 14, 2024

• WildCat/Bifunctor.v: formatting

  gio256

  committed
  6c975c1

• WildCat/Yoneda.v: add comment

  gio256

  committed
  31562d0