AgdaProofs My agda proofs for my internship at Chalmers with Mr. Coquand Here is a list of the proof done here for now: Proof in Cubical Agda (cubical type theory) that in the 2-loop space of A, the path concatenation commutes.