GitHub - amblafont/admissible-initial: Initial Semantics for admissible operations

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 7 Commits
Main.v		Main.v
README		README
additional_diag.json		additional_diag.json
appendixd.json		appendixd.json
compatST.json		compatST.json
d6.json		d6.json
daletha_nat.json		daletha_nat.json
dalethmu_is_sigma_mor.json		dalethmu_is_sigma_mor.json
diag1.json		diag1.json
diag2-.json		diag2-.json
diag2-aux.json		diag2-aux.json
diag2.json		diag2.json
distrib.json		distrib.json
dnat.json		dnat.json
dur.json		dur.json
dur2.json		dur2.json
eq1.json		eq1.json
eq2.json		eq2.json
eta_is_alg.json		eta_is_alg.json
hyp_dalethS_alg_mor.json		hyp_dalethS_alg_mor.json
nice_models.json		nice_models.json
tactic.v		tactic.v

Repository files navigation

This is an ongoing formalisation on some ongoing work
about Initial Semantics for admissible operations.

It is based on the UniMath library.

Some proofs were semi-generated from the diagram editor 
https://amblafont.github.io/graph-editor/index.html, based
on the commutative diagrams saved in the json files.