Instances in DoubleTT - #1246

Draft

KevinDCarlson wants to merge 53 commits into

mainfrom

Commits on Jul 16, 2026

@over types
KevinDCarlson
committed
54e4d02
Instance without specializations declares
KevinDCarlson
committed
77b56db
Diagrams in discrete theories declaring and validating, generating DiscreteDblModelDiagrams, behaving as dopfs
KevinDCarlson
committed
27c738a
Add the test files
KevinDCarlson
committed
9d1aeb6
missing commit
KevinDCarlson
committed
1b92d0c
clippy
KevinDCarlson
committed
42a9b62
docs fix
KevinDCarlson
committed
8f0a6f9
change a variable
KevinDCarlson
committed
d0cf43b
Switching specializations to equality types in diagrams
KevinDCarlson
committed
f4b812c
getting rid of the silly augment_with_lifts hack ahead of proper instance datatype
KevinDCarlson
committed
ee63b2a
Generate a dbl::instance from an @Instance
KevinDCarlson
committed
7e1e44a
Remove diagram elab pathway
KevinDCarlson
committed
504b4c3
should split: forgot to add DblModelInstances before; secondly, got rid of diagram keyword and started interpret instances as terms of types.
KevinDCarlson
committed
42d7dc1
:= morphism assignment and set literals
KevinDCarlson
committed
77ab7ea
Instance Tms, mapping syntax, improved singleton mapping syntax
KevinDCarlson
committed
72d9489
clippy
KevinDCarlson
committed
c9ceafb
cargo doc
KevinDCarlson
committed
57f5d5c
non-recursive discrete instance terms
KevinDCarlson
committed
b3dfbe9
revert special-casing for _ ident
KevinDCarlson
committed
9a61d40
fix todo
KevinDCarlson
committed
db2e8f1
clippy
KevinDCarlson
committed
f392286
delete spurious diagram toplevel
KevinDCarlson
committed
ffbd293
make instance body type more honest
KevinDCarlson
committed
cbd2175
eliminate stale mentions of @over
KevinDCarlson
committed
69a048f
Get the codomains into context
KevinDCarlson
committed
a8d2bde
documentation for instance_body_inner
KevinDCarlson
committed
950f254
introduce instance keyword to disambiguate instance terms from cons terms
KevinDCarlson
committed
20feba6
cleanup
KevinDCarlson
committed
723a891
Make unit an empty record
KevinDCarlson
committed
4020453
fmt
KevinDCarlson
committed
2056e69
Cleanup spurious support for morphism equations in instance declarations
KevinDCarlson
committed
ab9a7ec
FMT
KevinDCarlson
committed
39cc234
replace DefConst with Instance and keyword type with model
KevinDCarlson
committed
960dd63
tt: hold instance codomain as a real context variable, not a side channel
KevinDCarlson
committed
f988bb2
tt: rename TyS/TyV -> BaseTyS/BaseTyV
KevinDCarlson
committed
426684c
tt: represent instances as fiber types (FiberTy/FiberTm)
KevinDCarlson
committed
f87fc92
tt: rename TmS/TmV -> BaseTmS/BaseTmV
KevinDCarlson
committed
6ecc274
fix bug on importing instances of distinct codomains, introduce FiberTyS::TopVar to match with BaseTyS
KevinDCarlson
committed
e18c270
elaborate instances over modal codomains (multicat, SMC)
KevinDCarlson
committed
5381ad5
support nested codomain-morphism paths in instances (Add.op)
KevinDCarlson
committed
ada1ab0
DblModalModel datastructure
KevinDCarlson
committed
0cc997c
multicategory instances good to go
KevinDCarlson
committed
a61939a
support for ob ops
KevinDCarlson
committed
3a22e08
Handling HomApps
KevinDCarlson
committed
c75fbab
show off some normalization
KevinDCarlson
committed
8ff89a9

Commits on Jul 17, 2026

add klausmeir examples from matteo
KevinDCarlson
committed
070be32
formatting on nb
KevinDCarlson
committed
224553a
document types for instances as opposed to diagrams
KevinDCarlson
committed
064d95e
AI will never be able to forget to git add new files like a genuine human
KevinDCarlson
committed
1964f9c
notebook elaboration
KevinDCarlson
committed
5bdec7d
add backup test for nb examples
KevinDCarlson
committed
c57838a
separate out shared fiber elaboration structure
KevinDCarlson
committed
19838f8
Getting utils that aren't special to tt out of tt
KevinDCarlson
committed
ed76bff