From 57b70508fa197a804a64edf3acb5df1bc9bcdde8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Manuel=20B=C3=A4renz?= Date: Tue, 14 Aug 2018 11:23:10 +0200 Subject: [PATCH 1/4] Typo --- opetopic-play/app/views/docs/eqvs.scala.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/opetopic-play/app/views/docs/eqvs.scala.html b/opetopic-play/app/views/docs/eqvs.scala.html index 85fd3713..024cd770 100644 --- a/opetopic-play/app/views/docs/eqvs.scala.html +++ b/opetopic-play/app/views/docs/eqvs.scala.html @@ -113,7 +113,7 @@

Proof: ⇒

@svg("eqvs/eta-tu.svg")

- Futhermore, since η is a unary, target universal cell, we conclude + Furthermore, since η is a unary, target universal cell, we conclude that it is an equivalence by the coinductive hypothesis.

From 40f87105990d64c217c331986212f1b7c3fcd634 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Manuel=20B=C3=A4renz?= Date: Tue, 14 Aug 2018 11:29:06 +0200 Subject: [PATCH 2/4] Punctuation --- opetopic-play/app/views/docs/complexes.scala.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/opetopic-play/app/views/docs/complexes.scala.html b/opetopic-play/app/views/docs/complexes.scala.html index 0e30fea5..de0ccf20 100644 --- a/opetopic-play/app/views/docs/complexes.scala.html +++ b/opetopic-play/app/views/docs/complexes.scala.html @@ -123,7 +123,7 @@

Atomic Diagrams

edge tree.
- The box and edge trees are each rooted + The box and edge trees are each rooted.
From 7263705809b2656926f9cbdbec46ea894f39b77b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Manuel=20B=C3=A4renz?= Date: Tue, 14 Aug 2018 11:30:06 +0200 Subject: [PATCH 3/4] Typo --- opetopic-play/app/views/docs/opetopes.scala.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/opetopic-play/app/views/docs/opetopes.scala.html b/opetopic-play/app/views/docs/opetopes.scala.html index aad88c33..8651fa89 100644 --- a/opetopic-play/app/views/docs/opetopes.scala.html +++ b/opetopic-play/app/views/docs/opetopes.scala.html @@ -111,7 +111,7 @@

Face

First of all, as you pass your mouse cursor over one of the cells, you will notice that a number of lower dimensional cells are highlighted. - These are exactly the faces of the face you are pointing at. Futhermore + These are exactly the faces of the face you are pointing at. Furthermore if you click on one of the faces, its opetopic structure will be "extracted" into the bottom region, where you can verify that it also is an opetope in the sense defined above. From 0c1232e94de7248c748b607dfb9f68a96f3aef62 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Manuel=20B=C3=A4renz?= Date: Tue, 14 Aug 2018 11:31:21 +0200 Subject: [PATCH 4/4] Typo --- opetopic-play/app/views/docs/geometry.scala.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/opetopic-play/app/views/docs/geometry.scala.html b/opetopic-play/app/views/docs/geometry.scala.html index 2c569ec4..f4082122 100644 --- a/opetopic-play/app/views/docs/geometry.scala.html +++ b/opetopic-play/app/views/docs/geometry.scala.html @@ -50,7 +50,7 @@

Dimension 1

Dimension 2

- Dimension 2 becomes more intersting: we already have infinitely + Dimension 2 becomes more interesting: we already have infinitely many opetopes of dimension two, one for each natural number which counts the number of source arrows.