File title
module template where
Imports
open import ...
Idea
A concept is a insert abstract idea of concept, and is defined as insert definition using words.
Definition
concept : ...
concept = ...
Properties
Concept satisfies specific property
has-specific-property-concept : ...
has-specific-property-concept = ...
Examples
A subconcept is a concept
concept-subconcept : ...
concept-subconcept = ...
See also
- An instructive example of a file with the expected structure is
foundation.cantor-schroder-bernstein-escardo.
References
- Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013) (https://homotopytypetheory.org/book/, arXiv:1308.0729, DOI:10.48550)