Code

FinSetoids is Cartesian#292

Code

Draft

Taneb wants to merge 5 commits intoagda:masteragda/agda-categories:masterfrom Taneb:finset-cartesianTaneb/agda-categories:finset-cartesianCopy head branch name to clipboard

+171

Commits

Commits on Jul 3, 2021

• Add proof that FinSetoids is cartesian

  Taneb

  committed
  0543fa1

  Copy full SHA for 0543fa1

Commits on Jul 4, 2021

• Simplify FinSetoids Cartesian proofs a bit

  Taneb

  committed
  235e4bf

  Copy full SHA for 235e4bf

• Hide map-cong₂

  Show description for 73e1394
  Taneb

  committed
  73e1394

  Copy full SHA for 73e1394

• Don't use record syntax for products for terminal

  Taneb

  committed
  2b35f2c

  Copy full SHA for 2b35f2c

• FinSetoids is cocartesian too

  Taneb

  committed
  7429fe9

  Copy full SHA for 7429fe9