Code

tensor preserves coequalizers#2034

Code

Merged

Alizter merged 8 commits intoHoTT:masterHoTT/Coq-HoTT:masterfrom Alizter:ps/rr/tensor_preserves_coequalizersAlizter/HoTT:ps/rr/tensor_preserves_coequalizersCopy head branch name to clipboardAug 30, 2024

+169-34

Commits

Commits on Jul 23, 2024

• tensor preserves coequalizers

  Show description for b3f62bf
  Alizter

  committed
  b3f62bf

  Copy full SHA for b3f62bf

Commits on Jul 24, 2024

• AbHom: make definition of coeq match definition of in_cosetL

  jdchristensen

  committed
  30f43c0

  Copy full SHA for 30f43c0

• TensorProduct: introduce and use ab_tensor_prod_rec'

  jdchristensen

  committed
  bb8d051

  Copy full SHA for bb8d051

• make Monoidal.braide global

  Show description for 5e11461
  Alizter

  committed
  5e11461

  Copy full SHA for 5e11461

Commits on Jul 25, 2024

• show grp_iso_ab_tensor_prod_coeq_{l,r} commute in obv triangle resp.

  Show description for a0daafa
  Alizter

  committed
  a0daafa

  Copy full SHA for a0daafa

• TensorProduct: update comments and names

  jdchristensen

  committed
  08a6986

  Copy full SHA for 08a6986

Commits on Aug 8, 2024

• Merge branch 'master' into ps/rr/tensor_preserves_coequalizers

  Alizter

  authored
  303fde7

  Copy full SHA for 303fde7

Commits on Aug 30, 2024

• Merge branch 'master' into ps/rr/tensor_preserves_coequalizers

  Alizter

  authored
  bd3282b

  Copy full SHA for bd3282b