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

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

1. 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).