David Corfield sandbox

$$\mathbf{N} \colon \text{If}\;\; P \;\;\text{is a theorem, then so is}\;\; K P$$

$$w: W \vdash A(w): Type$$

$$w: W \vdash x(w): A(w)$$

$$w: W, x(w): A(w) \vdash (x(w) = x(w)): Prop$$

$$\vdash a: W$$

$$w: W \vdash A(w): Type$$

$$\vdash a^{\ast} A(w) \coloneqq A(a): Type$$

$$w: W \vdash A(w): Type$$

$$\vdash \sum_{w: W} A(w): Type$$

$$w: W \vdash \lozenge_W A(w) \coloneqq W^{\ast} (\sum_{w: W} A(w)): Type$$

1diff structure on S3 ? diff structures on S4 1 diff structures on S5 1 diff structures on S6 28 diff structures on S7, 8.7/2 2 diff structures on S8 8 diff structures on S9 6 diff structures on S10 992 diff structures on S11 32.31 1 diff structures on S12 3 diff structures on S13 2 diff structures on S14 16256 diff structures on S15 128.127

24, 120, 504, 960

$16256 = 128 \cdot 127$,

78, 133, 248

4k+3 ?

$\alpha^{rev}_{X,Y,Z} = \alpha^{-1}_{Z,Y,X}$

Ganesalingam in The Language of Mathematics uses Discourse Representation Theory (DRT) where Ranta uses Dependent Type Theory (DTT). My money is still on DTT. Does anyone using DRT in computerised mathematics?

According to Ganesalingam

DRT was developed to handle Geach’s ‘donkey sentences’ (Geach, 1980) and, as we will show in §3.3.1, there are similar sentences in real mathematical texts. We will also be able to adapt DRT to overcome deficiencies noted by Ranta in his own work; see §3.3.2 for details. (p. 15, n6)

DTT claims to do well with donkey sentences too, as I said in the post.

As far as I can see from the preview, one supposed deficiency of DTT is treated in §3.3.6:

Our approach also correctly handles an area which Ranta highlights as a deficiency of his own analysis. He notes that the plural pronoun ‘they’ is sometimes given a distributive reading and sometimes a collective reading; cf.

Nor do we quite understand the use of the plural pronoun They, which is sometimes distributive, paraphrasable by the term conjunction e.g.

If $A$ and $B$ do not lie outside the line $a$, they are incident on it

but sometimes used on the place of the “surface term conjunction”, so that it fuses together the arguments of the predicate, e.g.

If $a$ and $b$ do not converge, they are parallel.

(Ranta, 1994, p. 12)

Our analysis correctly distinguishes distributive and collective readings. ‘they’ is always taken to be a pronoun introducing an underlined plural discourse referent, requiring a plural antecedent. The difference in the readings of the two sentences given above is accounted for by the fact that ‘incident on it’ is distributive (as a single point is incident on a single line) and the adjective ‘parallel’ is collective (a single line cannot be parallel, but a collection of lines can). (p. 64)

How very odd. I wonder why Ranta believed this to be difficult for DTT? Suppose we have $x, y: A \vdash P(x), Q(x, y): Prop$ and suppose we have $a, b: A$ and $P(a), P(b), Q(a, b)$ all true. Then we would say ‘$a$ and $b$ are $A$s. They are $P$. They are $Q$.’ if sugared versions allow this, such as when $Q$ says of two lines that they’re parallel.

Maybe it’s not clear when such a $Q(a, b)$ affords the sugaring, ‘They are $Q$’. We wouldn’t do this for an asymmetric relation, such as less than. Certainly many symmetric relations are fine, ‘They are parallel/equal/isometric/homeomorphic’.

$Mod(-)$ and $Set^{(-)}$

$$\int_G (f_1 + f_2) = \int_G f_1 + \int_G f_2$$

$$\forall f_1, f_2 \in [G, \mathbb{C}]_{\text{Top}}$$

$(\mathbb{R}^3)^{cpt} \wedge (\mathbb{R}^1)_+ \union (\mathbb{R}^3)_+ \wedge (\mathbb{R}^1)^{cpt}$ different from $(\mathbb{R}^1)^{cpt} \wedge (\mathbb{R}^3)_+ \union (\mathbb{R}^1)_+ \wedge (\mathbb{R}^3)^{cpt}$

$$\array{ \hat E &\stackrel{}{\longrightarrow}& \flat_{dR} \hat E \\ \downarrow &{}^{(pb)}& \downarrow \\ \Pi(\hat E) &\stackrel{ch_E}{\longrightarrow}& \Pi \flat_{dR} \hat E }$$

$$\array{ \hat E &\stackrel{}{\longrightarrow}& \subset_{dR} \hat E \\ \downarrow &{}^{(pb)}& \downarrow \\ \lt(\hat E) &\stackrel{}{\longrightarrow}& \lt \subset_{dR} \hat E }$$

/!!/

$/\!\!/$

$$\array{ T^\infty X &\stackrel{p_1}{\longrightarrow}& X \\ \downarrow^{\mathrlap{p_2}} &(pb)& \downarrow^{\mathrlap{i_X}} \\ X &\stackrel{i_X}{\longrightarrow}& \Im X }$$

$A_\ast B$, $A \star B$, $A * B$

If $\Im(C_2\to C_1\to C_0) = C_2 \to C_0\to C_0$, then base change and adjoints.

$(A_2 \to A_1 \to A_0) \to (C_2 \to C_0\to C_0) \mapsto (A_2 \to A_1 \times_{C_0} C_1 \to A_0) \to (C_2\to C_1\to C_0)$

$$\array{ B_1 \leftarrow A_1 \times_{C_0} C_1 & \to & A_1\\ \downarrow & & \downarrow \\ C_1 & \to & C_0 }$$

So right adjoint to base change:

$(B_2 \to B_1 \to B_0) \to (C_2 \to C_1\to C_0) \mapsto (B_2 \to ?? \to B_0) \to (C_2\to C_0\to C_0)$

Is it just to make $Hom_{H/C_1}(A_1 \times_{C_0} C_1, B_1)$ be equivalent to $Hom_{H/C_0}(A_1, ??)$?

$\displaystyle \int$, $\textstyle \int$, $\textsize \int$, $\scriptsize \int$, $\scriptscriptsize \int$

probability, Probability?

Dynkin diagram?/ Dynkin quiver?	Platonic solid?	finite subgroups of SO(3)?	finite subgroups of SU(2)?	simple Lie group?
$A_{n \geq 1}$		cyclic group? $\mathbb{Z}_{n+1}$	cyclic group? $\mathbb{Z}_{n+1}$	special unitary group? $SU(n+1)$
D4?		Klein four-group? $D_4 \simeq \mathbb{Z}_2 \times \mathbb{Z}_2$	quaternion group? $2 D_4 \simeq$ Q8?	SO(8)?
${\bgcolor{red} D_{n \geq 4}}$	dihedron?, hosohedron?	dihedral group? $D_{2(n-2)}$	binary dihedral group? $2 D_{2(n-2)}$	special orthogonal group? $SO(2n)$
$E_6$	tetrahedron?	tetrahedral group? $T$	binary tetrahedral group? $2T$	E6?
$E_7$	cube?, octahedron?	octahedral group? $O$	binary octahedral group? $2O$	E7?
$E_8$	dodecahedron?, icosahedron?	icosahedral group? $I$	binary icosahedral group? {\bgcolor{red}$2I$}	E8?

\begin{table} \begin{tabular}{l | a | b | a | b} \hline \rowcolor{LightCyan} \mc{1}{} & \mc{1}{x} & \mc{1}{y} & \mc{1}{w} & \mc{1}{z} \ \hline variable 1 & a & b & c & d \ variable 2 & a & b & c & d \ \hline \end{tabular} \end{table}

{ b \color{red} c \color d } e

${\bgcolor{red} a b} c {\bgcolor{#0F0}d e}$

${\bgcolor{red} a}$

${\color{green} b}$

${\bgcolor{green} \color{red} c}$