File title
Content created by Fredrik Bakke.
Created on 2025-10-08.
Last modified on 2025-10-08.
{-# 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
.
Recent changes
- 2025-10-08. Fredrik Bakke. Organize repository files (#1500).