Formalize 'Combinatorics of higher-categorical diagrams' by Amar Hadzihasanovic

[anshwad10]

I think this is perfect for formalizing in cubical for a few reasons:

• From the introduction:

Another point of departure with most earlier approaches[4] is that molecules are defined inductively, as produced by a number of “constructors”.

• Also from the introduction:

For anything that concerns regular directed complexes, or any of the surrounding combinatorial structures, I attempted to be detailed and careful in excess of the expected standard for research-level mathematics.

• This is why univalence and inductive types will be helpful here:

Comment 3.3.3 — We will prove many properties of molecules by induction on their construction. Since we only consider properties that are invariant under isomorphism, in these proofs we will not explicitly consider closure under isomorphisms.
(When defining the predicate 'isMolecule' we don't need to give cases for closure under isomorphisms due to univalence making it automatic)

I am going to formalize it over a few PRs, starting with oriented graded posets.