From 8a5fe0bbbfc27f74a0aa3e5031a17dccc1a7661a Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Tue, 28 Nov 2023 10:28:58 -0500 Subject: [PATCH] Update src/graph-theory/complete-bipartite-graphs.lagda.md MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Vojtěch Štěpančík --- src/graph-theory/complete-bipartite-graphs.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/graph-theory/complete-bipartite-graphs.lagda.md b/src/graph-theory/complete-bipartite-graphs.lagda.md index c51345aeda..1b255ce9ff 100644 --- a/src/graph-theory/complete-bipartite-graphs.lagda.md +++ b/src/graph-theory/complete-bipartite-graphs.lagda.md @@ -34,7 +34,7 @@ consisting of: - The finite set of vertices is the [coproduct type](univalent-combinatorics.coproduct-types.md) `X + Y`. - Given an [unordered pair](foundation.unordered-pairs.md) `f : I → X + Y` of - vertices, an the finite type of edges on the unordered pair `(I , f)` is given + vertices, the finite type of edges on the unordered pair `(I , f)` is given by ```text