TEMPLATE.lagda.md

# File title

```agda
{-# OPTIONS --safe #-}

module foundation.template where

open import foundation-core.template public
```

<details><summary>Imports</summary>

```agda
open import ...
```

</details>

## Idea

A **concept** `C` is a _insert abstract idea of concept_, and is defined as
_insert definition using words_.

## Definition

```agda
concept : ...
concept = ...
```

## Properties

### Concepts satisfy a property

```agda
satisfies-property-concept : ...
satisfies-property-concept = ...
```

## Examples

### The following subconcept is a concept

```agda
concept-subconcept : ...
concept-subconcept = ...
```

## See also

- An instructive example of a file with the expected structure is
  [`order-theory.galois-connections`](https://raw.githubusercontent.com/UniMath/agda-unimath/master/src/order-theory/galois-connections.lagda.md).

## References

1. Univalent Foundations Project, _Homotopy Type Theory – Univalent Foundations
   of Mathematics_ (2013) ([website](https://homotopytypetheory.org/book/),
   [arXiv:1308.0729](https://arxiv.org/abs/1308.0729),
   [DOI:10.48550](https://doi.org/10.48550/arXiv.1308.0729))