File title
Content created by Fredrik Bakke and Jonathan Prieto-Cubides.
Created on 2023-03-23.
Last modified on 2023-06-28.
{-# OPTIONS --safe #-}
module foundation.template where
open import foundation-core.template public
Imports
open import ...
Idea
A concept C
is a insert abstract idea of concept, and is defined as
insert definition using words.
Definition
concept : ...
concept = ...
Properties
Concepts satisfy a property
satisfies-property-concept : ...
satisfies-property-concept = ...
Examples
The following subconcept is a concept
concept-subconcept : ...
concept-subconcept = ...
See also
- An instructive example of a file with the expected structure is
order-theory.galois-connections
.
References
- Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013) (website, arXiv:1308.0729, DOI:10.48550)
Recent changes
- 2023-06-28. Fredrik Bakke. Localizations and other things (#655).
- 2023-06-25. Fredrik Bakke. Fix alignment
where
blocks (#670). - 2023-06-07. Fredrik Bakke. Move public imports before "Imports" block (#642).
- 2023-03-23. Fredrik Bakke and Jonathan Prieto-Cubides. Improvements to file conventions and other documentation (#537).