You should work in the same directory as for previous lab. In particular, it contains the Prelude
Note: the names have been chosen so that we are compatible with the cubical Agda library but we are not using it yet
The labs will be following each other starting from now => work regularly!
Begin with
{-# OPTIONS --without-K #-}private variable
ℓ ℓ' : Levelrefl, sym, trans, subst, cong
show that addition is associative and admits zero as neutral element