The code includes two equivalent deductive systems for skew monoidal closed categories:
- a cut-free sequent calculus (SeqCalc.agda)
- a focused subsystem of sequent calculus derivations (Focusing.agda)
The main file containing the whole development is Main.agda.
The formalization uses Agda 2.6.2.