phanerozoic/

Agda-Cubical

Structured dataset from agda/cubical — Cubical Agda library for HoTT and univalent mathematics.

Repository: https://github.com/agda/cubical Commit: d4a2af62de40a6ca9a0b51981e41f804d879a1b9 Files: 1192 License: mit

	Schema




	

Column Type Description

statement string Declaration signature/claim with the leading keyword removed (verbatim slice); the full declaration minus its proof

proof string Verbatim proof/body, empty… See the full description on the dataset page: https://huggingface.co/datasets/phanerozoic/Agda-Cubical.