From 84887f78cb4d224d1be255434cbd373b99c41ea1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Piotr=20Paradzi=C5=84ski?= Date: Thu, 5 Dec 2024 17:10:54 +0100 Subject: [PATCH] Typos in README.org --- README.org | 28 ++-------------------------- 1 file changed, 2 insertions(+), 26 deletions(-) diff --git a/README.org b/README.org index 778ed8f..a220c10 100644 --- a/README.org +++ b/README.org @@ -16,10 +16,10 @@ Product, Sum and These show how to combine types in sets, where Smash, Wedge and |---------------------+---------|------------------|---------------|-------------------------| | both | Product | A * B | Smash product | 1 + (A * B) | | on of them | Sum | A + B | Wedge sum | 1 + A + B | -| bot of one of them | These | A + B + (A * B) | Can | 1 + A + B + (A * B) | +| both or one of them | These | A + B + (A * B) | Can | 1 + A + B + (A * B) | #+END: -[[https://ncatlab.org/nlab/show/smash+product][Smash product]] is canonical tensor product of pointed sets in a category, vien by taking product of underlying objects and indentifying with new basepoint - basepoints from ingredients. +[[https://ncatlab.org/nlab/show/smash+product][Smash product]] is canonical tensor product of pointed sets in a category, given by taking product of underlying objects and indentifying with new basepoint - basepoints from ingredients. #+BEGIN_SRC agda data Smash (A : Set) (B : Set) : Set where @@ -27,10 +27,6 @@ data Smash (A : Set) (B : Set) : Set where smash : A -> B -> Smash A B #+END_SRC -#+BEGIN_EXAMPLE -nada ----+---- smash A B -#+END_EXAMPLE - [[https://ncatlab.org/nlab/show/wedge+sum][Wedge sum]] of two pointed sets A and B is the quotient set of the disjoint union A + B where both copies of the basepoint are identified. @@ -42,16 +38,6 @@ data Wedge (A : Set)(B : Set) : Set where there : B -> Wedge A B #+END_SRC -#+BEGIN_EXAMPLE - here A - | - | -nowhere ----+ - | - | - there B -#+END_EXAMPLE - Can combines smash product with wedge sum: @@ -63,16 +49,6 @@ data Can (A : Set)(B : Set) : Set where two : A -> B -> Can A B #+END_SRC -#+BEGIN_EXAMPLE - one A - | - | -Non ----+----- two A B - | - | - eno B -#+END_EXAMPLE - ** Building Project can be build using [[https://www.gnu.org/software/make/][make]]: