[refactor] instance declaration#376

Open

gares wants to merge 147 commits intomasterfrom

refactor-instance

Commits on Jan 22, 2024

[refactor] separate add-mixin and make-mixin-canonical
gares
committed
[instance] declare-instance -> declare-mixins-from-factory + declare-structure-instance-from-mixins
gares
committed
document exported-op
gares
committed
[instance] test for structure op as subject
gares
committed
comment
gares
committed
add comment
gares
committed
wip-wrapping
gares
committed
minor changes

ptorrx
authored and
gares
committed
minor changes in instance.elpi

ptorrx
authored and
gares
committed
introduced derived instance check in instance.elpi (as a hack); still not working

ptorrx
authored and
gares
committed
fixed bugs in instance.elpi, compiles

ptorrx
authored and
gares
committed
minor changes

ptorrx
authored and
gares
committed
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…

ptorrx
authored and
gares
committed
fixed bug in cmonoid_enriched_cat.v

ptorrx
authored and
gares
committed
revised tests/cmonoid_enriched_cat.v

ptorrx
authored and
gares
committed
cleanup
gares
committed
eta expand wrapped mixing in context
gares
committed
minimal test for parameters
gares
committed
plan for auto wrapping
gares
committed
added enriched_cat_case1.v - problematic

ptorrx
authored and
gares
committed
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
added enriched_cat_case4.v

ptorrx
authored and
gares
committed
updated examples

ptorrx
authored and
gares
committed
updated enriched_cat_case1.v, there are still problems

ptorrx
authored and
gares
committed
updated enriched_cat_case4.v, not finished but less problematic

ptorrx
authored and
gares
committed
fix generation of wrapper-mixin when the mixin has deps
gares
committed
add more tests
gares
committed
cleanup
gares
committed
added enriched_cat_case5.v with more cases

ptorrx
authored and
gares
committed
completed enriched_cat_case4.v

ptorrx
authored and
gares
committed
note
gares
committed
validate structure declaration and wrap is the wrapper already exists
gares
committed
a bit unsure about this, it looks too smart in some cases
gares
committed
added enriched_cat_case6.v

ptorrx
authored and
gares
committed
wip
gares
committed
fix rebase
gares
committed
fix failsafe structure inference
gares
committed
fix test for wrapping
gares
committed
cleanup
gares
committed
cleanup
gares
committed
option wrapper=off to instance
gares
committed
demo should not break abstractions
gares
committed
test
gares
committed
moving category theory to theories

CohenCyril
authored and
gares
committed
defining pullbacks

CohenCyril
authored and
gares
committed
fix Makefile
gares
committed
colors are proofs
gares
committed
HB.tag
gares
committed
remove ELIM hack
gares
committed
cleanup
gares
committed
fix test
gares
committed
note
gares
committed
fix HB.tag
gares
committed
FIX: toposort will always be buggy ;-)
gares
committed
better eta expansion for failsafe structure elab
gares
committed
CAT: use HB.tag for pb_terminal (the wrapper is not autogen, but could be)
gares
committed
use subject-lifter instead of structure-op
gares
committed
document toposort bug
gares
committed
Enter HB.from (from factories)
gares
committed
fix rebase
gares
committed
added theories/encat.v (formalization of enriched categories, in progress)

ptorrx
authored and
gares
committed
updated theories/encat.v

ptorrx
authored and
gares
committed
updated theories/encat.v; definitions of enriched category and (tentatively) double category based on ncatlab

ptorrx
authored and
gares
committed
updated theories/encat.v

ptorrx
authored and
gares
committed
encat.v: fixed the definition of enriched category (reversed dependency order between base category and monoidal category

ptorrx
authored and
gares
committed
encat.v: basic update of double categories

ptorrx
authored and
gares
committed
encat.v: minor changes in comment

ptorrx
authored and
gares
committed
encat.v: added Cyril's definition of double categories

ptorrx
authored and
gares
committed
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
encat.v: minor changes

ptorrx
authored and
gares
committed
encat.v: updates to dcat transposition

ptorrx
authored and
gares
committed
encat.v: minor changes

ptorrx
authored and
gares
committed
encat.v: fixed unit functor problem (by changing the definition of unit_map)

ptorrx
authored and
gares
committed
encat.v: adding composition - however, it seems more problematic than it should

ptorrx
authored and
gares
committed
encat.v: adding horizontal cell composition (tough)

ptorrx
authored and
gares
committed
updated encav.v

ptorrx
authored and
gares
committed
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
updated encav.v; still missing: associator; product category to be fixed

ptorrx
authored and
gares
committed
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
updated encav.v

ptorrx
authored and
gares
committed
updated encav.v; improved some definitions

ptorrx
authored and
gares
committed
updated encav.v; version with transpose

ptorrx
authored and
gares
committed
updated encav.v; improved a definition

ptorrx
authored and
gares
committed
updated encav.v; minor changes

ptorrx
authored and
gares
committed
updated encav.v; added (alternative definitions of) horizontal 2-cell properties

ptorrx
authored and
gares
committed
added encatA.v, older version for experiments on instantiation. minor changes in encav.v

ptorrx
authored and
gares
committed
updated encav.v; in progress

ptorrx
authored and
gares
committed
updated encav.v; discharged product precategory assumptions (still to be proved: product is a category)

ptorrx
authored and
gares
committed
added encatB.v: complete formalization of double categories, without internal categories

ptorrx
authored and
gares
committed
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 …

ptorrx
authored and
gares
committed
encatB.v: improving the proofs

ptorrx
authored and
gares
committed
encatB.v: improving the notation

ptorrx
authored and
gares
committed
encatB.v: renamed definition to be consistent with slide presentation

ptorrx
authored and
gares
committed
added encatD.v (starting with internal categories)

ptorrx
authored and
gares
committed
updated encatD.v

ptorrx
authored and
gares
committed
updated encatD.v, added definition of internal category based on operators

ptorrx
authored and
gares
committed
updated encatD.v, complete definition of internal category based on NLab

ptorrx
authored and
gares
committed
updated encatD.v, minor changes

ptorrx
authored and
gares
committed
mono/epi code works now

CohenCyril
authored and
gares
committed
walking span

CohenCyril
authored and
gares
committed
rephrasing adjunctions (needs wrapping)

CohenCyril
authored and
gares
committed
internal categories parametrized with the ambiant one

CohenCyril
authored and
gares
committed
updated encatD.v

ptorrx
authored and
gares
committed
updated encatD.v

ptorrx
authored and
gares
committed
updated encatD.v, added encatD1.v; open problems in both

ptorrx
authored and
gares
committed
updated encatD.v

ptorrx
authored and
gares
committed
updated encatD.v

ptorrx
authored and
gares
committed
added encatI.v, which merges new version of cat.v with internal category development from encatD.v

Paolo Torrini
authored and
gares
committed
updated encatI.v

Paolo Torrini
authored and
gares
committed
updated encatI.v

Paolo Torrini
authored and
gares
committed
updated encatI.v

Paolo Torrini
authored and
gares
committed
updated encatI.v

Paolo Torrini
authored and
gares
committed
updated encatI.v

Paolo Torrini
authored and
gares
committed
updated encatI.v

Paolo Torrini
authored and
gares
committed
updated encatI.v; added encatI0.v as experiment

Paolo Torrini
authored and
gares
committed
updated encatI.v

ptorrx
authored and
gares
committed
updated encatI.v

Paolo Torrini
authored and
gares
committed
updated encatI.v

Paolo Torrini
authored and
gares
committed
updated encatI.v

Paolo Torrini
authored and
gares
committed
updated encatI.v; complete definition of double cat based on internal cat

Paolo Torrini
authored and
gares
committed
updated encatI.v; cleaning up

Paolo Torrini
authored and
gares
committed
updated encatI.v; merged in the strict double category direct definition from encatD.v

Paolo Torrini
authored and
gares
committed
updated comment in encatI.v

Paolo Torrini
authored and
gares
committed
updated comment in encatI.v

Paolo Torrini
authored and
gares
committed
changes in encatI0.v

Paolo Torrini
authored and
gares
committed
encatI.v and encatI0.v now depend on cat.v

Paolo Torrini
authored and
gares
committed
updated encatI.v

Paolo Torrini
authored and
gares
committed
updated encatI.v

Paolo Torrini
authored and
gares
committed
updated encatI.v

Paolo Torrini
authored and
gares
committed
updated encatI.v

Paolo Torrini
authored and
gares
committed
restructuring

ptorrx
authored and
gares
committed
restructuring

ptorrx
authored and
gares
committed
updated encatI.v

Paolo Torrini
authored and
gares
committed
updated dependencies

Paolo Torrini
authored and
gares
committed
updated dependencies

Paolo Torrini
authored and
gares
committed
updated encatI.v

Paolo Torrini
authored and
gares
committed

Commits on Jan 29, 2024

wip
gares
committed
wip
gares
committed

Commits on Jan 31, 2024

unsafe(univ) option
gares
committed
wip
gares
committed

Commits on Feb 2, 2024

wip
gares
committed
wip
gares
committed

Commits on Mar 4, 2024