Code

quotient by a trivial group#2188

Code

Merged

Alizter merged 5 commits intoHoTT:masterHoTT/Coq-HoTT:masterfrom Alizter:ps/rr/quotient_by_a_trivial_groupAlizter/HoTT:ps/rr/quotient_by_a_trivial_groupCopy head branch name to clipboardJan 8, 2025

+64-39

Commits

Commits on Jan 4, 2025

• quotient by a trivial group

  Show description for dcc21b2
  Alizter

  committed
  dcc21b2

  Copy full SHA for dcc21b2

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

  Alizter

  authored
  df7551c

  Copy full SHA for df7551c

Commits on Jan 6, 2025

• trivial kernel iff isembedding

  Show description for fa9e7ee
  Alizter

  committed
  fa9e7ee

  Copy full SHA for fa9e7ee

Commits on Jan 7, 2025

• update according to review comments

  Show description for 6bc6f73
  Alizter

  committed
  6bc6f73

  Copy full SHA for 6bc6f73

• explode isembedding_grouphomomorphism into both directions

  Show description for 21dc47a
  Alizter

  committed
  21dc47a

  Copy full SHA for 21dc47a