blob: 9b4387efbde4052ce270c7fdd540c3504382a818 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
|
\begin{signature}\label{phase5_context_apply}
$\apply{f}{x}$ is a set.
\end{signature}
\begin{signature}\label{phase5_context_pair}
$(a,b)$ is a set.
\end{signature}
\begin{struct}\label{phase5_context_magma}
A phase five context magma $A$ is a onesorted structure equipped with
\begin{enumerate}
\item $\phasefivecombine$
\end{enumerate}
such that
\begin{enumerate}
\item\label{phase5_context_refl} $A = A$.
\end{enumerate}
\end{struct}
\begin{struct}\label{phase5_context_unital_magma}
A phase five context unital magma $A$ is a phase five context magma.
\end{struct}
\begin{abbreviation}\label{phase5_context_dot}
%! infixl 4
$a\phasefivedot b = \phasefivecombine(a,b)$.
\end{abbreviation}
\begin{abbreviation}\label{phase5_context_commutes}
$a$ phase five commutes with $b$ iff
$a\phasefivedot b = b\phasefivedot a$.
\end{abbreviation}
\begin{proposition}\label{phase5_context_dot_explicit}
Let $A$ be a phase five context magma.
Let $a,b$ be sets.
Then $a\phasefivedot b = \phasefivecombine[A](a,b)$.
\end{proposition}
\begin{proposition}\label{phase5_context_inherited}
Let $A$ be a phase five context unital magma.
Let $a,b$ be sets.
Then $a\phasefivedot b = \phasefivecombine[A](a,b)$.
\end{proposition}
\begin{proposition}\label{phase5_context_nested}
Let $A$ be a phase five context magma.
Let $a,b$ be sets.
Then $a$ phase five commutes with $b$ iff
$\phasefivecombine[A](a,b) = \phasefivecombine[A](b,a)$.
\end{proposition}
\begin{proposition}\label{phase5_context_explicit_unique}
Let $A,a,b$ be sets.
Then $\phasefivecombine[A](a,b) = \phasefivecombine[A](a,b)$.
\end{proposition}
|
