Code

Set-enriched categories#1467

Code

Open

umedaikiti wants to merge 62 commits intoUniMath:masterUniMath/UniMath:masterfrom umedaikiti:cartesian-monoidalumedaikiti/UniMath:cartesian-monoidalCopy head branch name to clipboard

+1,527-8

Commits

Commits on Nov 22, 2021

• Uniqueness of general products (up to isomorphism)

  

  langston-barrett

  authored and

  umedaikiti

  committed
  d884132

• Associativity of binary products

  

  langston-barrett

  authored and

  umedaikiti

  committed
  0d97d7f

• Fix notation conflict

  

  langston-barrett

  authored and

  umedaikiti

  committed
  b222d1f

• monoidal structure on categories with products

  

  langston-barrett

  authored and

  umedaikiti

  committed
  c13d72e

• Migrate proof of binary product associativity to binproducts.v

  

  langston-barrett

  authored and

  umedaikiti

  committed
  e629c8b

• Add Cartesian.v to CONTENTS.md

  

  langston-barrett

  authored and

  umedaikiti

  committed
  dabdc7b

Commits on Nov 23, 2021

• fix errors

  umedaikiti

  committed
  ca9bf06

Commits on Feb 13, 2022

• Merge branch 'master' into univalence-slices

  nmvdw

  authored
  38574c7

Commits on Feb 14, 2022

• Merge pull request UniMath#1457 from nmvdw/univalence-slices

  Show description for 2d319b9
  benediktahrens

  authored
  2d319b9

• Street (op)fibs in Cat

  nmvdw

  committed
  096421b

• Merge branch 'master' into street-fib-in-cat

  nmvdw

  authored
  70324d3

• Merge pull request UniMath#1458 from nmvdw/street-fib-in-cat

  Show description for d2273bf
  benediktahrens

  authored
  d2273bf

Commits on Feb 17, 2022

• try to get the unicode notation table to look nice in ASCII viewing mode

  DanGrayson

  committed
  d04c63d

• Merge branch 'master' of github.com:UniMath/UniMath

  DanGrayson

  committed
  36b3874

• add some remarks about emacs to USAGE.md

  DanGrayson

  committed
  5ff1ae2

• try to get the unicode notation table to look nice in ASCII viewing mode, part 2

  DanGrayson

  committed
  c725e07

Commits on Feb 18, 2022

• Duality involutions, rework discrete bicats

  nmvdw

  committed
  f3bb66e

• Merge branch 'master' into duality-involution

  nmvdw

  authored
  393e08c

• Whoops....

  nmvdw

  committed
  fc49805

• Remove comments

  nmvdw

  committed
  d239668

• Forgot to add a file

  nmvdw

  committed
  368f71d

• Merge pull request UniMath#1460 from nmvdw/duality-involution

  Show description for 91d2bb0
  benediktahrens

  authored
  91d2bb0

Commits on Feb 19, 2022

• Uniqueness of general products (up to isomorphism)

  

  langston-barrett

  authored and

  umedaikiti

  committed
  6cc9f2e

• Associativity of binary products

  

  langston-barrett

  authored and

  umedaikiti

  committed
  8018188

• Fix notation conflict

  

  langston-barrett

  authored and

  umedaikiti

  committed
  e1dd9d7

• monoidal structure on categories with products

  

  langston-barrett

  authored and

  umedaikiti

  committed
  6c4c07b

• Migrate proof of binary product associativity to binproducts.v

  

  langston-barrett

  authored and

  umedaikiti

  committed
  7e7b846

• Add Cartesian.v to CONTENTS.md

  

  langston-barrett

  authored and

  umedaikiti

  committed
  740c86e

• fix errors

  umedaikiti

  committed
  2eeccd0

Commits on Feb 20, 2022

• remove obsolete file Cats.v with def of precat of cats

  benediktahrens

  committed
  503a80e

• dissolve DispCat/Aux

  benediktahrens

  committed
  b76613d

Commits on Feb 21, 2022

• Merge pull request UniMath#1461 from benediktahrens/issue-1404

  Show description for c08e9d4
  DanGrayson

  authored
  c08e9d4

• Merge branch 'master' into issue-1421-sq

  benediktahrens

  authored
  0da7f1c

• Merge pull request UniMath#1462 from benediktahrens/issue-1421-sq

  Show description for 9abbfb0
  DanGrayson

  authored
  9abbfb0

Commits on Feb 22, 2022

• remove duplicate z_iso_inv_mor

  benediktahrens

  committed
  ac60705

• remove duplicate z_iso_is_z_isomorphism2

  benediktahrens

  committed
  9ff746c

• remove comments

  benediktahrens

  committed
  bb95381

• arguments now implicit

  benediktahrens

  committed
  f0da7e2

• arguments now implicit II

  benediktahrens

  committed
  c5f099d

• arguments now implicit III

  benediktahrens

  committed
  78e12b4

• arguments now implicit IV

  benediktahrens

  committed
  b089c47

Commits on Feb 23, 2022

• Merge pull request UniMath#1463 from benediktahrens/issue-948

  Show description for 5362f3a
  benediktahrens

  authored
  5362f3a

Commits on Mar 2, 2022

• mention tags-search in the INSTALL file

  DanGrayson

  committed
  ff504a7

• move tags-search discussion from USAGE to INSTALL

  DanGrayson

  committed
  e4111db

Commits on Mar 4, 2022

• remove autorewrite

  umedaikiti

  committed
  dbda0c0

• Merge branch 'cartesian-monoidal' of github.com:umedaikiti/UniMath into cartesian-monoidal

  umedaikiti

  committed
  6d7c516

Commits on Mar 5, 2022

• add correspondence between HSET-enriched and ordinary categories

  umedaikiti

  committed
  2ac52f4

• improve proofs

  umedaikiti

  committed
  126a7e9

• Merge branch 'UniMath:master' into cartesian-monoidal

  umedaikiti

  authored
  39ea615

• Merge branch 'UniMath:master' into cartesian-monoidal

  umedaikiti

  authored
  ea2e038

• remove auto and autorewrite

  umedaikiti

  committed
  0a08dae

Commits on Mar 7, 2022

• move some parts to UniMath/Bicategories/EnrichedCategories

  umedaikiti

  committed
  16ae6a5

Commits on Mar 11, 2022

• Merge branch 'master' into cartesian-monoidal

  benediktahrens

  authored
  18f4a6c

Commits on Oct 18, 2022

• Merge branch 'master' into cartesian-monoidal

  benediktahrens

  authored
  7166753

Commits on Nov 7, 2022

• Update UniMath/CategoryTheory/limits/binproducts.v

  Show description for 70c125f
  

  benediktahrens

  and

  m-lindgren

  authored
  70c125f

• Update UniMath/CategoryTheory/limits/binproducts.v

  Show description for 9788301
  

  benediktahrens

  and

  m-lindgren

  authored
  9788301

• Update UniMath/CategoryTheory/limits/binproducts.v

  Show description for 2a7cdc5
  

  benediktahrens

  and

  m-lindgren

  authored
  2a7cdc5

• Update UniMath/CategoryTheory/limits/binproducts.v

  Show description for 5d42579
  

  benediktahrens

  and

  m-lindgren

  authored
  5d42579

• Update UniMath/CategoryTheory/limits/binproducts.v

  Show description for 7c41460
  

  benediktahrens

  and

  m-lindgren

  authored
  7c41460

• Merge branch 'master' into cartesian-monoidal

  benediktahrens

  authored
  98f0cc6

Commits on Nov 18, 2022

• Merge branch 'master' into cartesian-monoidal

  benediktahrens

  authored
  41339c6

• Update UniMath/CategoryTheory/Monoidal/Cartesian.v

  Show description for 9d5e0e4
  

  benediktahrens

  and

  m-lindgren

  authored
  9d5e0e4