corrections in part 1 (#96)

* corrections in part 1 * expand explanations in chapter 5 after discussion with @greenbergjosh * wip * wip * fixes * wip * add talk slides * add talk slides * corrections * fixes * wip
winitzki · Apr 16, 2024 · f00d2ee · f00d2ee
1 parent 66cc810
commit f00d2ee
Show file tree

Hide file tree

Showing 19 changed files with 4,910 additions and 393 deletions.
diff --git a/sofp-src/lyx/sofp-appendices.lyx b/sofp-src/lyx/sofp-appendices.lyx
@@ -33676,7 +33676,7 @@ Now we can use the pushout property of
 \begin_inset Formula $z:S^{B,A,P^{A,B}}$
 \end_inset
 
- such that
+ such that:
 \begin_inset Formula 
 \[
 x\triangleright\big(\overline{f^{\uparrow P^{A,\bullet}}}\big)^{\uparrow S^{A,A,\bullet}}=z\triangleright f^{\downarrow S^{\bullet,A,P^{A,B}}}\text{ and }y\triangleright\big(\overline{f^{\downarrow P^{\bullet,B}}}\big)^{\uparrow S^{B,B,\bullet}}=z\triangleright f^{\uparrow S^{B,\bullet,P^{A,B}}}\quad.
@@ -33688,7 +33688,7 @@ We need to produce a value
 \begin_inset Formula $t:S^{B,A,P^{B,A}}$
 \end_inset
 
- such that 
+ such that: 
 \begin_inset Formula 
 \[
 x=t\triangleright f^{\downarrow S^{\bullet,A,P^{B,A}}}\bef\big(\overline{f^{\downarrow P^{\bullet,A}}}\big)^{\uparrow S^{A,A,\bullet}}\text{ and }y=t\triangleright f^{\uparrow S^{B,\bullet,P^{B,A}}}\bef\big(\overline{f^{\uparrow P^{B,\bullet}}}\big)^{\uparrow S^{B,B,\bullet}}\quad.