[no description] http://git.yellowsquid.uk/yellowsquid/idris-obs.git/atom?h=master 2023-01-12T17:57:06Z 2023-01-12T17:57:06Z Greg Brown greg.brown01@ed.ac.uk 2023-01-12T17:57:06Z urn:sha1:72feeec46c34c678640341e76958481f4244d8df This folder spells out the action of equality and cast for the different type constructors. Ideally the two correctness proofs should given by reflexivity.