From 3d536883dd99112ca9b5578d6b9db3c953afa9f6 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 27 May 2023 19:45:19 -0400 Subject: [PATCH] remove empty code blocks --- src/group-theory/isomorphisms-concrete-groups.lagda.md | 4 ---- src/univalent-combinatorics/2-element-types.lagda.md | 8 -------- .../unlabeled-rooted-trees.lagda.md | 4 ---- src/univalent-combinatorics/unlabeled-trees.lagda.md | 4 ---- 4 files changed, 20 deletions(-) diff --git a/src/group-theory/isomorphisms-concrete-groups.lagda.md b/src/group-theory/isomorphisms-concrete-groups.lagda.md index 3b1f66ff50b..aba173d2812 100644 --- a/src/group-theory/isomorphisms-concrete-groups.lagda.md +++ b/src/group-theory/isomorphisms-concrete-groups.lagda.md @@ -33,7 +33,3 @@ iso-Concrete-Group = iso-Large-Precategory Concrete-Group-Large-Precategory ## Properties ### Equivalences of concrete groups are isomorphisms of concrete groups - -```agda - -``` diff --git a/src/univalent-combinatorics/2-element-types.lagda.md b/src/univalent-combinatorics/2-element-types.lagda.md index 554f23ee06a..377ce08aa1a 100644 --- a/src/univalent-combinatorics/2-element-types.lagda.md +++ b/src/univalent-combinatorics/2-element-types.lagda.md @@ -840,18 +840,10 @@ module _ This remains to be shown. -```agda - -``` - ### A map between 2-element types is not an equivalence if and only if its image is a singleton subtype of the codomain This remains to be shown. -```agda - -``` - ### Any map between 2-element types that is not an equivalence is constant This remains to be shown. diff --git a/src/univalent-combinatorics/unlabeled-rooted-trees.lagda.md b/src/univalent-combinatorics/unlabeled-rooted-trees.lagda.md index 612cde8a81b..01d159804fb 100644 --- a/src/univalent-combinatorics/unlabeled-rooted-trees.lagda.md +++ b/src/univalent-combinatorics/unlabeled-rooted-trees.lagda.md @@ -17,7 +17,3 @@ module univalent-combinatorics.unlabeled-rooted-trees where An unlabelled rooted tree is an unlabelled tree equipped with a vertex. ## Definition - -```agda - -``` diff --git a/src/univalent-combinatorics/unlabeled-trees.lagda.md b/src/univalent-combinatorics/unlabeled-trees.lagda.md index 538830aa773..d880bb19101 100644 --- a/src/univalent-combinatorics/unlabeled-trees.lagda.md +++ b/src/univalent-combinatorics/unlabeled-trees.lagda.md @@ -18,7 +18,3 @@ An unlabelled tree is an undirected graph `G` such that any cycle in `G` must have length 1. ## Definition - -```agda - -```