Skip to content

Commit

Permalink
Typos in README.org
Browse files Browse the repository at this point in the history
  • Loading branch information
lemastero authored Dec 5, 2024
1 parent 476154a commit 84887f7
Showing 1 changed file with 2 additions and 26 deletions.
28 changes: 2 additions & 26 deletions README.org
Original file line number Diff line number Diff line change
Expand Up @@ -16,21 +16,17 @@ 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
nada : Smash A B
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.
Expand All @@ -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:


Expand All @@ -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]]:

Expand Down

0 comments on commit 84887f7

Please sign in to comment.