fix flat modality

Author: 5HT

doc/anders.tex

@@ -101,6 +101,7 @@ \section{Syntax}
     kan :=&$\textbf{transp}\ E\ E\ |\ \textbf{hcomp}\ E$ \\
    glue :=&$\textbf{Glue}\ E\ |\ \textbf{glue}\ E\ |\ \textbf{unglue}\ E\ E$ \\
      Im :=&$\textbf{Im}\ \mathrm{E}\ |\ \textbf{Inf}\ \mathrm{E}\ |\ \textbf{Join}\ \mathrm{E}\ |\ \textbf{ind$_{Im}$}\ \mathrm{E}\ \mathrm{E}$ \\
+     Flat :=&$\flat\ \mathrm{E}\ |\ \flat-\textrm{unit}\ \mathrm{E}\ |\ \flat-\textrm{counit}\ \mathrm{E}\ |\ \textbf{ind}_{\flat}\ \mathrm{E}\ \mathrm{E}$ \\
 \end{tabular}
 \end{table}
 
@@ -109,7 +110,7 @@ \section{Syntax}
 \begin{table}[ht!]
 \centering
 \begin{tabular}{rl}
-      E :=&$\textrm{cosmos}\ |\ \textrm{var}\ |\ \textrm{MLTT}\ |\ \textrm{CCHM}\ |\ \textrm{Im}$ \\
+      E :=&$\textrm{cosmos}\ |\ \textrm{var}\ |\ \textrm{MLTT}\ |\ \textrm{CCHM}\ |\ \textrm{Im}\ |\ \textrm{Flat}$ \\
    CCHM :=&$\textrm{path}\ |\ \textrm{I}\ |\ \textrm{part}\ |\ \textrm{sub}\ |\ \textrm{kan}\ |\ \textrm{glue}$ \\
    MLTT :=&$\textrm{pi}\ |\ \textrm{sigma}\ |\ \textrm{id}$ \\
 \end{tabular}
@@ -122,7 +123,8 @@ \section{Syntax}
 \texttt{V}, \texttt{$\bigvee$}, \texttt{$\bigwedge$}, \texttt{-}, \texttt{+}, \texttt{@}, \texttt{PathP},
 \texttt{transp}, \texttt{hcomp}, \texttt{zero}, \texttt{one}, \texttt{Partial}, \texttt{inc},
 \texttt{$\times$}, \texttt{$\rightarrow$}, \texttt{:}, \texttt{:=}, \texttt{$\mapsto$}, \texttt{U},
-\texttt{ouc}, \texttt{interval}, \texttt{inductive}, \texttt{Glue}, \texttt{glue}, \texttt{unglue}.
+\texttt{ouc}, \texttt{interval}, \texttt{inductive}, \texttt{Glue}, \texttt{glue}, \texttt{unglue},
+\texttt{$\flat$}, \texttt{$\flat$-unit}, \texttt{$\flat$-counit}, \texttt{ind-$\flat$}.
 
 \textbf{Indentifiers}. Identifiers support UTF-8. Indentifiers couldn't
 start with $\texttt{:}$, $\texttt{-}$, $\rightarrow$. Sample identifiers:
@@ -651,6 +653,44 @@ \subsection{de Rham Stack}
 \textbf{def} T$^\infty$-map (X Y : U) (f : X → Y) ($\tau$ : T$^\infty$ X) : T$^\infty$ Y := (f $\tau$.1, d X Y f $\tau$.1 $\tau$.2) \\
 \end{tabular}
 \end{table}
+\newpage
+\subsection{Flat Modality}
+
+The Flat modality $\flat$ (also known as the discrete modality) is a core primitive of Anders,
+providing a way to talk about discrete types. In a cohesive type theory, $\flat A$
+is the type $A$ equipped with the discrete topology. The Anders prover implements
+computational semantics for the Flat modality including its interaction with cubical primitives.
+
+\begin{table}[ht!]
+\tabstyle
+\begin{tabular}{l}
+\textbf{def} Flat (A : U) := $\flat$ A \\
+\textbf{def} FlatUnit (A : U) (a : A) := $\flat$-unit a \\
+\textbf{def} FlatCounit (A : U) (x : $\flat$ A) := $\flat$-counit x \\
+\\
+\textbf{def} isDiscrete (A : U) : U := isEquiv A ($\flat$ A) (FlatUnit A) \\
+\textbf{def} ♭-$\eta$ (A : U) (x : $\flat$ A) : Path ($\flat$ A) x ($\flat$-unit ($\flat$-counit x)) := <p> x \\
+\textbf{def} FlatInd (A : U) (B : $\flat$ A $\rightarrow$ U) := ind-$\flat$ A B \\
+\end{tabular}
+\end{table}
+
+The Flat modality satisfies several computational reduction rules for transport and
+homogeneous composition, which ensure that $\flat$ behaves correctly with respect to the
+cubical structure of the type theory.
+
+\begin{table}[ht!]
+\tabstyle
+\begin{tabular}{l}
+transp$^{i}$ ($\flat$ A) $\varphi$ ($\flat$-unit a) = $\flat$-unit (transp$^i$ A $\varphi$ a) \\
+hcomp$^{i}$ ($\flat$ A) [$\phi$ $\mapsto$ $\flat$-unit u] ($\flat$-unit u$_0$) = $\flat$-unit (hcomp$^i$ A [$\phi$ $\mapsto$ u] u$_0$) \\
+\end{tabular}
+\end{table}
+
+\begin{definition}[Discreteness]
+A type $A$ is called discrete if the unit map $\flat$-unit : $A \rightarrow \flat A$ is an equivalence.
+This corresponds to the intuition that a type is discrete if its points have no non-trivial paths between them
+that aren't captured by the discrete topology.
+\end{definition}
 
 \newpage
 \subsection{Inductive Types}

library/foundations/modal/flat.anders

@@ -18,3 +18,19 @@ def ♭-η (A : U) := λ (x : Flat A), <p> x
 
 -- Discrete types: A type is discrete if ♭-unit is an equivalence.
 def isDiscrete (A : U) := isEquiv A (Flat A) (FlatUnit A)
+
+-- Reality Check (Simon Huber Equations)
+
+def trans-♭ (A : I → U) (a : A 0) : ♭ (A 1) := ♭-unit (transp (<i> A i) 0 a)
+def trans-♭′ (A : I → U) (a : A 0) : ♭ (A 1) := transp (<i> ♭ (A i)) 0 (♭-unit a)
+def trans-♭-is-correct (A : I → U) (a : A 0) : Path (♭ (A 1)) (trans-♭ A a) (trans-♭′ A a) := <_> trans-♭ A a
+
+def hcomp-♭ (A : U) (r : I) (u : I → Partial A r) (u₀ : A[r ↦ u 0]) : ♭ A
+ := ♭-unit (hcomp A r u (ouc u₀))
+
+def hcomp-♭′ (A : U) (r : I) (u : I → Partial A r) (u₀ : A[r ↦ u 0]) : ♭ A
+ := hcomp (Flat A) r (λ (i : I), [(r = 1) → ♭-unit (u i 1=1)]) (♭-unit (ouc u₀))
+
+def hcomp-♭-is-correct (A : U) (r : I) (u : I → Partial A r) (u₀ : A[r ↦ u 0])
+  : Path (Flat A) (hcomp-♭ A r u u₀) (hcomp-♭′ A r u u₀)
+ := <_> hcomp-♭ A r u u₀

src/ocaml/kernel/check.ml

@@ -1321,6 +1321,7 @@ and conv_internal v1 v2 =
     | VJoin u, VJoin v -> u == v || conv u v
     | VIndIm (a1, b1), VIndIm (a2, b2) -> (a1 == a2 || conv a1 a2) && (b1 == b2 || conv b1 b2)
     | VFla u, VFla v -> u == v || conv u v
+    | VFlaUnit u, VFlaUnit v -> u == v || conv u v
     | VFlaCounit u, VFlaCounit v -> u == v || conv u v
     | VIndFla (a1, b1), VIndFla (a2, b2) -> (a1 == a2 || conv a1 a2) && (b1 == b2 || conv b1 b2)
     | VCoequ (a1, b1, f1, g1), VCoequ (a2, b2, f2, g2) -> (a1 == a2 || conv a1 a2) && (b1 == b2 || conv b1 b2) && (f1 == f2 || conv f1 f2) && (g1 == g2 || conv g1 g2)