File title

Content created by Fredrik Bakke and Jonathan Prieto-Cubides.

Created on 2023-03-23.
Last modified on 2023-11-01.

{-# 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

References

  1. Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013) (website, arXiv:1308.0729)

Recent changes