Code

[refactor] instance declaration#376

Code

Open

gares wants to merge 147 commits intomastermath-comp/hierarchy-builder:masterfrom refactor-instancemath-comp/hierarchy-builder:refactor-instanceCopy head branch name to clipboard

+9,563-270

Commits

Commits on Jan 22, 2024

• [refactor] separate add-mixin and make-mixin-canonical

  gares

  committed
  567cee2

  Copy full SHA for 567cee2

• [instance] declare-instance -> declare-mixins-from-factory + declare-structure-instance-from-mixins

  Show description for 64525c7
  gares

  committed
  64525c7

  Copy full SHA for 64525c7

• document exported-op

  gares

  committed
  e0f7895

  Copy full SHA for e0f7895

• [instance] test for structure op as subject

  gares

  committed
  8c4071c

  Copy full SHA for 8c4071c

• comment

  gares

  committed
  6128f44

  Copy full SHA for 6128f44

• add comment

  gares

  committed
  1f8ca63

  Copy full SHA for 1f8ca63

• wip-wrapping

  gares

  committed
  2ce532b

  Copy full SHA for 2ce532b

• minor changes

  

  ptorrx

  authored and

  gares

  committed
  f12d772

  Copy full SHA for f12d772

• minor changes in instance.elpi

  

  ptorrx

  authored and

  gares

  committed
  d3273a4

  Copy full SHA for d3273a4

• introduced derived instance check in instance.elpi (as a hack); still not working

  

  ptorrx

  authored and

  gares

  committed
  894aff0

  Copy full SHA for 894aff0

• fixed bugs in instance.elpi, compiles

  

  ptorrx

  authored and

  gares

  committed
  1ecb634

  Copy full SHA for 1ecb634

• minor changes

  

  ptorrx

  authored and

  gares

  committed
  cb3d53a

  Copy full SHA for cb3d53a

• added and updated cmon_enriched_cat.v - this file contains three examples; there's an unsolved compilation glitch (it will compile the 2nd and 3rd examples separately but not together, depending on…

  Show description for 2fc6662
  

  ptorrx

  authored and

  gares

  committed
  2fc6662

  Copy full SHA for 2fc6662

• fixed bug in cmonoid_enriched_cat.v

  

  ptorrx

  authored and

  gares

  committed
  c002312

  Copy full SHA for c002312

• revised tests/cmonoid_enriched_cat.v

  

  ptorrx

  authored and

  gares

  committed
  46d5932

  Copy full SHA for 46d5932

• cleanup

  gares

  committed
  ed74a82

  Copy full SHA for ed74a82

• eta expand wrapped mixing in context

  gares

  committed
  3e040b4

  Copy full SHA for 3e040b4

• minimal test for parameters

  gares

  committed
  19fd228

  Copy full SHA for 19fd228

• plan for auto wrapping

  gares

  committed
  2d94c60

  Copy full SHA for 2d94c60

• added enriched_cat_case1.v - problematic

  

  ptorrx

  authored and

  gares

  committed
  df1d865

  Copy full SHA for df1d865

• added enriched_cat_case2.v - which works, but wraps without depencies; and enriched_cat_case3.v which fails, as expected (sadly)

  

  ptorrx

  authored and

  gares

  committed
  ffce0b9

  Copy full SHA for ffce0b9

• added enriched_cat_case4.v

  

  ptorrx

  authored and

  gares

  committed
  f6e4458

  Copy full SHA for f6e4458

• updated examples

  

  ptorrx

  authored and

  gares

  committed
  9aebc2b

  Copy full SHA for 9aebc2b

• updated enriched_cat_case1.v, there are still problems

  

  ptorrx

  authored and

  gares

  committed
  3ef5a1f

  Copy full SHA for 3ef5a1f

• updated enriched_cat_case4.v, not finished but less problematic

  

  ptorrx

  authored and

  gares

  committed
  96a6113

  Copy full SHA for 96a6113

• fix generation of wrapper-mixin when the mixin has deps

  gares

  committed
  1292d1e

  Copy full SHA for 1292d1e

• add more tests

  gares

  committed
  457817c

  Copy full SHA for 457817c

• cleanup

  gares

  committed
  66eb897

  Copy full SHA for 66eb897

• added enriched_cat_case5.v with more cases

  

  ptorrx

  authored and

  gares

  committed
  41da96e

  Copy full SHA for 41da96e

• completed enriched_cat_case4.v

  

  ptorrx

  authored and

  gares

  committed
  30debed

  Copy full SHA for 30debed

• note

  gares

  committed
  7d113d0

  Copy full SHA for 7d113d0

• validate structure declaration and wrap is the wrapper already exists

  gares

  committed
  d3dce62

  Copy full SHA for d3dce62

• a bit unsure about this, it looks too smart in some cases

  Show description for cad4f20
  gares

  committed
  cad4f20

  Copy full SHA for cad4f20

• added enriched_cat_case6.v

  

  ptorrx

  authored and

  gares

  committed
  4e80aff

  Copy full SHA for 4e80aff

• wip

  gares

  committed
  353b3fd

  Copy full SHA for 353b3fd

• fix rebase

  gares

  committed
  d343316

  Copy full SHA for d343316

• fix failsafe structure inference

  gares

  committed
  063ffc3

  Copy full SHA for 063ffc3

• fix test for wrapping

  gares

  committed
  1d18979

  Copy full SHA for 1d18979

• cleanup

  gares

  committed
  8f2d47d

  Copy full SHA for 8f2d47d

• cleanup

  gares

  committed
  7e41346

  Copy full SHA for 7e41346

• option wrapper=off to instance

  gares

  committed
  fb93fbe

  Copy full SHA for fb93fbe

• demo should not break abstractions

  gares

  committed
  4c2742c

  Copy full SHA for 4c2742c

• test

  gares

  committed
  bd83789

  Copy full SHA for bd83789

• moving category theory to theories

  

  CohenCyril

  authored and

  gares

  committed
  d1c8070

  Copy full SHA for d1c8070

• defining pullbacks

  

  CohenCyril

  authored and

  gares

  committed
  b73828c

  Copy full SHA for b73828c

• fix Makefile

  gares

  committed
  2e25e5c

  Copy full SHA for 2e25e5c

• colors are proofs

  gares

  committed
  cb9cfb0

  Copy full SHA for cb9cfb0

• HB.tag

  gares

  committed
  feb9249

  Copy full SHA for feb9249

• remove ELIM hack

  gares

  committed
  a180918

  Copy full SHA for a180918

• cleanup

  gares

  committed
  450cf7e

  Copy full SHA for 450cf7e

• fix test

  gares

  committed
  79aba6c

  Copy full SHA for 79aba6c

• note

  gares

  committed
  8ac8c9d

  Copy full SHA for 8ac8c9d

• fix HB.tag

  gares

  committed
  2a39460

  Copy full SHA for 2a39460

• FIX: toposort will always be buggy ;-)

  gares

  committed
  a2bf6d4

  Copy full SHA for a2bf6d4

• better eta expansion for failsafe structure elab

  gares

  committed
  922d6b9

  Copy full SHA for 922d6b9

• CAT: use HB.tag for pb_terminal (the wrapper is not autogen, but could be)

  gares

  committed
  7005440

  Copy full SHA for 7005440

• use subject-lifter instead of structure-op

  gares

  committed
  e24e3a1

  Copy full SHA for e24e3a1

• document toposort bug

  gares

  committed
  81fe41f

  Copy full SHA for 81fe41f

• Enter HB.from (from factories)

  gares

  committed
  da52021

  Copy full SHA for da52021

• fix rebase

  gares

  committed
  8d40177

  Copy full SHA for 8d40177

• added theories/encat.v (formalization of enriched categories, in progress)

  

  ptorrx

  authored and

  gares

  committed
  d7007d3

  Copy full SHA for d7007d3

• updated theories/encat.v

  

  ptorrx

  authored and

  gares

  committed
  09618b3

  Copy full SHA for 09618b3

• updated theories/encat.v; definitions of enriched category and (tentatively) double category based on ncatlab

  

  ptorrx

  authored and

  gares

  committed
  edb0313

  Copy full SHA for edb0313

• updated theories/encat.v

  

  ptorrx

  authored and

  gares

  committed
  02b0fc5

  Copy full SHA for 02b0fc5

• encat.v: fixed the definition of enriched category (reversed dependency order between base category and monoidal category

  

  ptorrx

  authored and

  gares

  committed
  75d8bfe

  Copy full SHA for 75d8bfe

• encat.v: basic update of double categories

  

  ptorrx

  authored and

  gares

  committed
  b415e67

  Copy full SHA for b415e67

• encat.v: minor changes in comment

  

  ptorrx

  authored and

  gares

  committed
  de22884

  Copy full SHA for de22884

• encat.v: added Cyril's definition of double categories

  

  ptorrx

  authored and

  gares

  committed
  5531d11

  Copy full SHA for 5531d11

• encat.v: revised parametrisation in enriched categories; revised definition of double categories, which includes the (also needed) identity functor - there are still some problems with it though

  

  ptorrx

  authored and

  gares

  committed
  b3dd85d

  Copy full SHA for b3dd85d

• encat.v: minor changes

  

  ptorrx

  authored and

  gares

  committed
  00c66a9

  Copy full SHA for 00c66a9

• encat.v: updates to dcat transposition

  

  ptorrx

  authored and

  gares

  committed
  31843f2

  Copy full SHA for 31843f2

• encat.v: minor changes

  

  ptorrx

  authored and

  gares

  committed
  73a9732

  Copy full SHA for 73a9732

• encat.v: fixed unit functor problem (by changing the definition of unit_map)

  

  ptorrx

  authored and

  gares

  committed
  995fef1

  Copy full SHA for 995fef1

• encat.v: adding composition - however, it seems more problematic than it should

  

  ptorrx

  authored and

  gares

  committed
  b1f88ea

  Copy full SHA for b1f88ea

• encat.v: adding horizontal cell composition (tough)

  

  ptorrx

  authored and

  gares

  committed
  d0014ce

  Copy full SHA for d0014ce

• updated encav.v

  

  ptorrx

  authored and

  gares

  committed
  5c9bac2

  Copy full SHA for 5c9bac2

• updated encav.v; flat version with 4 functors (source, target, horizontal unit and horizontal composition); unital and assoc properties still missing; actual hierarchy to be revised

  

  ptorrx

  authored and

  gares

  committed
  3fb6dde

  Copy full SHA for 3fb6dde

• updated encav.v; still missing: associator; product category to be fixed

  

  ptorrx

  authored and

  gares

  committed
  e2536bc

  Copy full SHA for e2536bc

• updated encav.v; nlab-style definition of double categories; still missing - proof that product category is a category (does not need to be assumed)

  

  ptorrx

  authored and

  gares

  committed
  9c092de

  Copy full SHA for 9c092de

• updated encav.v

  

  ptorrx

  authored and

  gares

  committed
  d158ffc

  Copy full SHA for d158ffc

• updated encav.v; improved some definitions

  

  ptorrx

  authored and

  gares

  committed
  5220df5

  Copy full SHA for 5220df5

• updated encav.v; version with transpose

  

  ptorrx

  authored and

  gares

  committed
  f7a0d99

  Copy full SHA for f7a0d99

• updated encav.v; improved a definition

  

  ptorrx

  authored and

  gares

  committed
  6074c78

  Copy full SHA for 6074c78

• updated encav.v; minor changes

  

  ptorrx

  authored and

  gares

  committed
  0d19f51

  Copy full SHA for 0d19f51

• updated encav.v; added (alternative definitions of) horizontal 2-cell properties

  

  ptorrx

  authored and

  gares

  committed
  64d354c

  Copy full SHA for 64d354c

• added encatA.v, older version for experiments on instantiation. minor changes in encav.v

  

  ptorrx

  authored and

  gares

  committed
  1da3981

  Copy full SHA for 1da3981

• updated encav.v; in progress

  

  ptorrx

  authored and

  gares

  committed
  6a942fb

  Copy full SHA for 6a942fb

• updated encav.v; discharged product precategory assumptions (still to be proved: product is a category)

  

  ptorrx

  authored and

  gares

  committed
  429865c

  Copy full SHA for 429865c

• added encatB.v: complete formalization of double categories, without internal categories

  

  ptorrx

  authored and

  gares

  committed
  7f79278

  Copy full SHA for 7f79278

• encatB.v: cleaned up the definition of strict double category; the definition is complete, it does not use internal categories but defines an ad-hoc product category on D1. TODO: improve the style …

  Show description for c26463b
  

  ptorrx

  authored and

  gares

  committed
  c26463b

  Copy full SHA for c26463b

• encatB.v: improving the proofs

  

  ptorrx

  authored and

  gares

  committed
  5faa745

  Copy full SHA for 5faa745

• encatB.v: improving the notation

  

  ptorrx

  authored and

  gares

  committed
  a5e0e21

  Copy full SHA for a5e0e21

• encatB.v: renamed definition to be consistent with slide presentation

  

  ptorrx

  authored and

  gares

  committed
  d2e0580

  Copy full SHA for d2e0580

• added encatD.v (starting with internal categories)

  

  ptorrx

  authored and

  gares

  committed
  6fdcfb5

  Copy full SHA for 6fdcfb5

• updated encatD.v

  

  ptorrx

  authored and

  gares

  committed
  5cb88f9

  Copy full SHA for 5cb88f9

• updated encatD.v, added definition of internal category based on operators

  

  ptorrx

  authored and

  gares

  committed
  7a60a01

  Copy full SHA for 7a60a01

• updated encatD.v, complete definition of internal category based on NLab

  

  ptorrx

  authored and

  gares

  committed
  45565f9

  Copy full SHA for 45565f9

• updated encatD.v, minor changes

  

  ptorrx

  authored and

  gares

  committed
  0fcd38c

  Copy full SHA for 0fcd38c

• mono/epi code works now

  

  CohenCyril

  authored and

  gares

  committed
  a2757c4

  Copy full SHA for a2757c4

• walking span

  

  CohenCyril

  authored and

  gares

  committed
  d42cc3e

  Copy full SHA for d42cc3e

• rephrasing adjunctions (needs wrapping)

  

  CohenCyril

  authored and

  gares

  committed
  dc4548e

  Copy full SHA for dc4548e

• internal categories parametrized with the ambiant one

  

  CohenCyril

  authored and

  gares

  committed
  b00a244

  Copy full SHA for b00a244

• updated encatD.v

  

  ptorrx

  authored and

  gares

  committed
  4151369

  Copy full SHA for 4151369

• updated encatD.v

  

  ptorrx

  authored and

  gares

  committed
  fc63ca4

  Copy full SHA for fc63ca4

• updated encatD.v, added encatD1.v; open problems in both

  

  ptorrx

  authored and

  gares

  committed
  f661ea2

  Copy full SHA for f661ea2

• updated encatD.v

  

  ptorrx

  authored and

  gares

  committed
  6284697

  Copy full SHA for 6284697

• updated encatD.v

  

  ptorrx

  authored and

  gares

  committed
  9560c9f

  Copy full SHA for 9560c9f

• added encatI.v, which merges new version of cat.v with internal category development from encatD.v

  

  Paolo Torrini

  authored and

  gares

  committed
  b0444ce

  Copy full SHA for b0444ce

• updated encatI.v

  

  Paolo Torrini

  authored and

  gares

  committed
  f1325d7

  Copy full SHA for f1325d7

• updated encatI.v

  

  Paolo Torrini

  authored and

  gares

  committed
  527dd0f

  Copy full SHA for 527dd0f

• updated encatI.v

  

  Paolo Torrini

  authored and

  gares

  committed
  c820234

  Copy full SHA for c820234

• updated encatI.v

  

  Paolo Torrini

  authored and

  gares

  committed
  1e0aa1b

  Copy full SHA for 1e0aa1b

• updated encatI.v

  

  Paolo Torrini

  authored and

  gares

  committed
  eb7d3eb

  Copy full SHA for eb7d3eb

• updated encatI.v

  

  Paolo Torrini

  authored and

  gares

  committed
  9974744

  Copy full SHA for 9974744

• updated encatI.v; added encatI0.v as experiment

  

  Paolo Torrini

  authored and

  gares

  committed
  f81757d

  Copy full SHA for f81757d

• updated encatI.v

  

  ptorrx

  authored and

  gares

  committed
  ab63881

  Copy full SHA for ab63881

• updated encatI.v

  

  Paolo Torrini

  authored and

  gares

  committed
  3459991

  Copy full SHA for 3459991

• updated encatI.v

  

  Paolo Torrini

  authored and

  gares

  committed
  ca8bffd

  Copy full SHA for ca8bffd

• updated encatI.v

  

  Paolo Torrini

  authored and

  gares

  committed
  82e72d6

  Copy full SHA for 82e72d6

• updated encatI.v; complete definition of double cat based on internal cat

  

  Paolo Torrini

  authored and

  gares

  committed
  f1ab058

  Copy full SHA for f1ab058

• updated encatI.v; cleaning up

  

  Paolo Torrini

  authored and

  gares

  committed
  9ff3448

  Copy full SHA for 9ff3448

• updated encatI.v; merged in the strict double category direct definition from encatD.v

  

  Paolo Torrini

  authored and

  gares

  committed
  d9c6869

  Copy full SHA for d9c6869

• updated comment in encatI.v

  

  Paolo Torrini

  authored and

  gares

  committed
  41ad7c1

  Copy full SHA for 41ad7c1

• updated comment in encatI.v

  

  Paolo Torrini

  authored and

  gares

  committed
  40f762b

  Copy full SHA for 40f762b

• changes in encatI0.v

  

  Paolo Torrini

  authored and

  gares

  committed
  c4724d7

  Copy full SHA for c4724d7

• encatI.v and encatI0.v now depend on cat.v

  

  Paolo Torrini

  authored and

  gares

  committed
  6570167

  Copy full SHA for 6570167

• updated encatI.v

  

  Paolo Torrini

  authored and

  gares

  committed
  deb0352

  Copy full SHA for deb0352

• updated encatI.v

  

  Paolo Torrini

  authored and

  gares

  committed
  11e40e2

  Copy full SHA for 11e40e2

• updated encatI.v

  

  Paolo Torrini

  authored and

  gares

  committed
  4292494

  Copy full SHA for 4292494

• updated encatI.v

  

  Paolo Torrini

  authored and

  gares

  committed
  b21e282

  Copy full SHA for b21e282

• restructuring

  

  ptorrx

  authored and

  gares

  committed
  2167b3d

  Copy full SHA for 2167b3d

• restructuring

  

  ptorrx

  authored and

  gares

  committed
  a2cc722

  Copy full SHA for a2cc722

• updated encatI.v

  

  Paolo Torrini

  authored and

  gares

  committed
  e84c91f

  Copy full SHA for e84c91f

• updated dependencies

  

  Paolo Torrini

  authored and

  gares

  committed
  3564fd6

  Copy full SHA for 3564fd6

• updated dependencies

  

  Paolo Torrini

  authored and

  gares

  committed
  1ce5b11

  Copy full SHA for 1ce5b11

• updated encatI.v

  

  Paolo Torrini

  authored and

  gares

  committed
  d94c19f

  Copy full SHA for d94c19f

Commits on Jan 29, 2024

• wip

  gares

  committed
  d88dd20

  Copy full SHA for d88dd20

• wip

  gares

  committed
  b9cb11f

  Copy full SHA for b9cb11f

Commits on Jan 31, 2024

• unsafe(univ) option

  gares

  committed
  f2590ab

  Copy full SHA for f2590ab

• wip

  gares

  committed
  e8a680c

  Copy full SHA for e8a680c

Commits on Feb 2, 2024

• wip

  gares

  committed
  18ca7ba

  Copy full SHA for 18ca7ba

• wip

  gares

  committed
  59af016

  Copy full SHA for 59af016

Commits on Mar 4, 2024

• wip

  gares

  committed
  e19ed85

  Copy full SHA for e19ed85

• wip

  gares

  committed
  10b3fb0

  Copy full SHA for 10b3fb0

• wip

  gares

  committed
  af2989f

  Copy full SHA for af2989f

• wip

  gares

  committed
  0cf1c4c

  Copy full SHA for 0cf1c4c

• wip

  gares

  committed
  e85441c

  Copy full SHA for e85441c