Skip to content

Commit

Permalink
Add blank lines between <details> tags and markdown syntax (#490)
Browse files Browse the repository at this point in the history
Resolves #489.

It remains to add linebreaks between import statements from different
namespaces and such again.
  • Loading branch information
fredrik-bakke committed Mar 7, 2023
1 parent 90c5f3b commit 5a52006
Show file tree
Hide file tree
Showing 909 changed files with 1,819 additions and 0 deletions.
2 changes: 2 additions & 0 deletions src/category-theory/adjunctions-large-precategories.lagda.md
Expand Up @@ -5,6 +5,7 @@ module category-theory.adjunctions-large-precategories where
```

<details><summary>Imports</summary>

```agda
open import Agda.Primitive using (Setω)
open import category-theory.functors-large-precategories
Expand All @@ -15,6 +16,7 @@ open import foundation.equivalences
open import foundation.identity-types
open import foundation.universe-levels
```

</details>

## Idea
Expand Down
2 changes: 2 additions & 0 deletions src/category-theory/anafunctors.lagda.md
Expand Up @@ -5,6 +5,7 @@ module category-theory.anafunctors where
```

<details><summary>Imports</summary>

```agda
open import category-theory.categories
open import category-theory.functors-precategories
Expand All @@ -17,6 +18,7 @@ open import foundation.identity-types
open import foundation.propositional-truncations
open import foundation.universe-levels
```

</details>

## Idea
Expand Down
2 changes: 2 additions & 0 deletions src/category-theory/categories.lagda.md
Expand Up @@ -5,6 +5,7 @@ module category-theory.categories where
```

<details><summary>Imports</summary>

```agda
open import category-theory.isomorphisms-precategories
open import category-theory.precategories
Expand All @@ -21,6 +22,7 @@ open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels
```

</details>

## Idea
Expand Down
2 changes: 2 additions & 0 deletions src/category-theory/coproducts-precategories.lagda.md
Expand Up @@ -5,6 +5,7 @@ module category-theory.coproducts-precategories where
```

<details><summary>Imports</summary>

```agda
open import category-theory.precategories
open import foundation.cartesian-product-types
Expand All @@ -15,6 +16,7 @@ open import foundation.propositions
open import foundation.unique-existence
open import foundation.universe-levels
```

</details>

## Idea
Expand Down
2 changes: 2 additions & 0 deletions src/category-theory/discrete-precategories.lagda.md
Expand Up @@ -5,6 +5,7 @@ module category-theory.discrete-precategories where
```

<details><summary>Imports</summary>

```agda
open import category-theory.functors-precategories
open import category-theory.natural-transformations-precategories
Expand All @@ -16,6 +17,7 @@ open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels
```

</details>

### Discrete precategories
Expand Down
Expand Up @@ -5,6 +5,7 @@ module category-theory.endomorphisms-of-objects-categories where
```

<details><summary>Imports</summary>

```agda
open import category-theory.categories
open import foundation.dependent-pair-types
Expand All @@ -14,6 +15,7 @@ open import foundation.universe-levels
open import group-theory.monoids
open import group-theory.semigroups
```

</details>

## Definition
Expand Down
2 changes: 2 additions & 0 deletions src/category-theory/epimorphisms-large-precategories.lagda.md
Expand Up @@ -5,6 +5,7 @@ module category-theory.epimorphisms-large-precategories where
```

<details><summary>Imports</summary>

```agda
open import category-theory.isomorphisms-large-precategories
open import category-theory.large-precategories
Expand All @@ -14,6 +15,7 @@ open import foundation.identity-types
open import foundation.propositions
open import foundation.universe-levels
```

</details>

## Idea
Expand Down
2 changes: 2 additions & 0 deletions src/category-theory/equivalences-categories.lagda.md
Expand Up @@ -5,12 +5,14 @@ module category-theory.equivalences-categories where
```

<details><summary>Imports</summary>

```agda
open import category-theory.categories
open import category-theory.equivalences-precategories
open import category-theory.functors-categories
open import foundation.universe-levels
```

</details>

## Idea
Expand Down
2 changes: 2 additions & 0 deletions src/category-theory/equivalences-large-precategories.lagda.md
Expand Up @@ -5,13 +5,15 @@ module category-theory.equivalences-large-precategories where
```

<details><summary>Imports</summary>

```agda
open import Agda.Primitive using (Setω)
open import category-theory.functors-large-precategories
open import category-theory.large-precategories
open import category-theory.natural-isomorphisms-large-precategories
open import foundation.universe-levels
```

</details>

## Idea
Expand Down
2 changes: 2 additions & 0 deletions src/category-theory/equivalences-precategories.lagda.md
Expand Up @@ -5,6 +5,7 @@ module category-theory.equivalences-precategories where
```

<details><summary>Imports</summary>

```agda
open import category-theory.functors-precategories
open import category-theory.natural-isomorphisms-precategories
Expand All @@ -13,6 +14,7 @@ open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.universe-levels
```

</details>

## Idea
Expand Down
Expand Up @@ -5,6 +5,7 @@ module category-theory.exponential-objects-precategories where
```

<details><summary>Imports</summary>

```agda
open import category-theory.precategories
open import category-theory.products-precategories
Expand All @@ -13,6 +14,7 @@ open import foundation.dependent-pair-types
open import foundation.unique-existence
open import foundation.universe-levels
```

</details>

## Idea
Expand Down
2 changes: 2 additions & 0 deletions src/category-theory/functors-categories.lagda.md
Expand Up @@ -5,13 +5,15 @@ module category-theory.functors-categories where
```

<details><summary>Imports</summary>

```agda
open import category-theory.categories
open import category-theory.functors-precategories
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels
```

</details>

## Idea
Expand Down
2 changes: 2 additions & 0 deletions src/category-theory/functors-large-precategories.lagda.md
Expand Up @@ -5,13 +5,15 @@ module category-theory.functors-large-precategories where
```

<details><summary>Imports</summary>

```agda
open import Agda.Primitive using (Setω)
open import category-theory.large-precategories
open import foundation.functions
open import foundation.identity-types
open import foundation.universe-levels
```

</details>

## Idea
Expand Down
2 changes: 2 additions & 0 deletions src/category-theory/functors-precategories.lagda.md
Expand Up @@ -5,6 +5,7 @@ module category-theory.functors-precategories where
```

<details><summary>Imports</summary>

```agda
open import category-theory.precategories
open import foundation.cartesian-product-types
Expand All @@ -14,6 +15,7 @@ open import foundation.identity-types
open import foundation.propositions
open import foundation.universe-levels
```

</details>

## Idea
Expand Down
2 changes: 2 additions & 0 deletions src/category-theory/groupoids.lagda.md
Expand Up @@ -5,6 +5,7 @@ module category-theory.groupoids where
```

<details><summary>Imports</summary>

```agda
open import category-theory.categories
open import category-theory.equivalences-categories
Expand All @@ -26,6 +27,7 @@ open import foundation.sets
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels
```

</details>

## Idea
Expand Down
Expand Up @@ -5,6 +5,7 @@ module category-theory.homotopies-natural-transformations-large-precategories wh
```

<details><summary>Imports</summary>

```agda
open import Agda.Primitive using (Setω)
open import category-theory.functors-large-precategories
Expand All @@ -14,6 +15,7 @@ open import foundation.homotopies
open import foundation.identity-types
open import foundation.universe-levels
```

</details>

## Idea
Expand Down
2 changes: 2 additions & 0 deletions src/category-theory/initial-objects-precategories.lagda.md
Expand Up @@ -5,13 +5,15 @@ module category-theory.initial-objects-precategories where
```

<details><summary>Imports</summary>

```agda
open import category-theory.precategories
open import foundation-core.identity-types
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.universe-levels
```

</details>

## Idea
Expand Down
2 changes: 2 additions & 0 deletions src/category-theory/isomorphisms-categories.lagda.md
Expand Up @@ -5,6 +5,7 @@ module category-theory.isomorphisms-categories where
```

<details><summary>Imports</summary>

```agda
open import category-theory.categories
open import category-theory.isomorphisms-precategories
Expand All @@ -19,6 +20,7 @@ open import foundation.sets
open import foundation.subtype-identity-principle
open import foundation.universe-levels
```

</details>

## Idea
Expand Down
2 changes: 2 additions & 0 deletions src/category-theory/isomorphisms-large-precategories.lagda.md
Expand Up @@ -5,6 +5,7 @@ module category-theory.isomorphisms-large-precategories where
```

<details><summary>Imports</summary>

```agda
open import category-theory.large-precategories
open import foundation.cartesian-product-types
Expand All @@ -15,6 +16,7 @@ open import foundation.sets
open import foundation.subtypes
open import foundation.universe-levels
```

</details>

## Idea
Expand Down
2 changes: 2 additions & 0 deletions src/category-theory/isomorphisms-precategories.lagda.md
Expand Up @@ -5,6 +5,7 @@ module category-theory.isomorphisms-precategories where
```

<details><summary>Imports</summary>

```agda
open import category-theory.precategories
open import foundation.cartesian-product-types
Expand All @@ -19,6 +20,7 @@ open import foundation.sets
open import foundation.subtypes
open import foundation.universe-levels
```

</details>

## Idea
Expand Down
2 changes: 2 additions & 0 deletions src/category-theory/large-categories.lagda.md
Expand Up @@ -5,13 +5,15 @@ module category-theory.large-categories where
```

<details><summary>Imports</summary>

```agda
open import Agda.Primitive using (Setω)
open import category-theory.isomorphisms-large-precategories
open import category-theory.large-precategories
open import foundation.equivalences
open import foundation.universe-levels
```

</details>

## Idea
Expand Down
2 changes: 2 additions & 0 deletions src/category-theory/large-precategories.lagda.md
Expand Up @@ -5,13 +5,15 @@ module category-theory.large-precategories where
```

<details><summary>Imports</summary>

```agda
open import Agda.Primitive using (Setω)
open import foundation.functions
open import foundation.identity-types
open import foundation.sets
open import foundation.universe-levels
```

</details>

## Idea
Expand Down
Expand Up @@ -5,6 +5,7 @@ module category-theory.monomorphisms-large-precategories where
```

<details><summary>Imports</summary>

```agda
open import category-theory.isomorphisms-large-precategories
open import category-theory.large-precategories
Expand All @@ -14,6 +15,7 @@ open import foundation.identity-types
open import foundation.propositions
open import foundation.universe-levels
```

</details>

## Idea
Expand Down
2 changes: 2 additions & 0 deletions src/category-theory/natural-isomorphisms-categories.lagda.md
Expand Up @@ -5,13 +5,15 @@ module category-theory.natural-isomorphisms-categories where
```

<details><summary>Imports</summary>

```agda
open import category-theory.categories
open import category-theory.functors-categories
open import category-theory.natural-isomorphisms-precategories
open import category-theory.natural-transformations-categories
open import foundation.universe-levels
```

</details>

## Idea
Expand Down
Expand Up @@ -5,13 +5,15 @@ module category-theory.natural-isomorphisms-large-precategories where
```

<details><summary>Imports</summary>

```agda
open import category-theory.functors-large-precategories
open import category-theory.isomorphisms-large-precategories
open import category-theory.large-precategories
open import category-theory.natural-transformations-large-precategories
open import foundation.universe-levels
```

</details>

## Idea
Expand Down

0 comments on commit 5a52006

Please sign in to comment.