You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
\textbf{Indentifiers}. Identifiers support UTF-8. Indentifiers couldn't
130
158
start with $\texttt{:}$, $\texttt{-}$, $\rightarrow$. Sample identifiers:
@@ -653,7 +681,7 @@ \subsection{de Rham Stack}
653
681
\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) \\
654
682
\end{tabular}
655
683
\end{table}
656
-
\newpage
684
+
657
685
\subsection{Flat Modality}
658
686
659
687
The Flat modality $\flat$ (also known as the discrete modality) is a core primitive of Anders,
@@ -669,7 +697,7 @@ \subsection{Flat Modality}
669
697
\textbf{def} FlatCounit (A : U) (x : $\flat$ A) := $\flat$-counit x \\
670
698
\\
671
699
\textbf{def} isDiscrete (A : U) : U := isEquiv A ($\flat$ A) (FlatUnit A) \\
672
-
\textbf{def} ♭-$\eta$ (A : U) (x : $\flat$ A) : Path ($\flat$ A) x ($\flat$-unit ($\flat$-counit x)) := <p> x \\
700
+
\textbf{def} $\flat$-$\eta$ (A : U) (x : $\flat$ A) : Path ($\flat$ A) x ($\flat$-unit ($\flat$-counit x)) := <p> x \\
673
701
\textbf{def} FlatInd (A : U) (B : $\flat$ A $\rightarrow$ U) := ind-$\flat$ A B \\
674
702
\end{tabular}
675
703
\end{table}
@@ -692,58 +720,162 @@ \subsection{Flat Modality}
692
720
that aren't captured by the discrete topology.
693
721
\end{definition}
694
722
695
-
\newpage
696
723
\subsection{Inductive Types}
697
724
698
-
Anders currently don’t support Lean-compatible generic inductive schemes
699
-
definition. So instead of generic inductive schemes Anders supports well-founded trees (W-types).
700
-
Basic data types like List, Nat, Fin, Vec are implemented as W-types in base library.
725
+
The foundational inductive types in \anders\ are based on Martin-L\"{o}f's intuitionistic type theory \cite{ML84}. Instead of a generic inductive definition scheme, \anders\ provides well-founded trees (W-types) as a primitive construction from which other data types can be derived. Basic data types like List, Fin, and Vec are implemented as W-types in the core library.
701
726
702
-
\begin{itemize}
703
-
\item W, 0, 1, 2 basis of MLTT-80 (Martin-L\"{o}f)
704
-
\item General Schemes of Inductive Types (Paulin-Mohring)
705
-
\end{itemize}
727
+
\subsubsection*{Empty Type}
706
728
707
-
\subsection{Higher Inductive Types}
729
+
The empty type $\mathbf{0}$ (also written as \texttt{empty}) is the inductive type with no constructors. It represents logical falsehood. Its induction principle is the principle of explosion (\textit{ex falso quodlibet}).
708
730
709
-
As for higher inductive types Anders is inspired by Three-HIT foundation (Coequalizer, Path Coequalizer and Colimit)
710
-
but contains only modal extensions Flat and Infinitesimal, Hub Spoke Disc for direct truncations encoding, and
711
-
Coequalizer for computable $S^1$, $S^n$, $K(G,n)$, Colimits.
731
+
\begin{table}[ht!]
732
+
\tabstyle
733
+
\begin{tabular}{l}
734
+
\textbf{def} Empty : U := \textbf{0} \\
735
+
\textbf{def} Empty-elim (C : Empty $\rightarrow$ U) (z : Empty) : C z := \textbf{ind-empty} C z
736
+
\end{tabular}
737
+
\end{table}
712
738
713
-
Also there are other foundations to consider motivated by typical tasks in homotopy (type) theory:
739
+
\subsubsection*{Unit Type}
714
740
715
-
\begin{itemize}
716
-
\item Coequalizer, Path Coequalizer and Colimit (van der Weide)
\item General Schemes of Higher Inductive Types (Cubical Agda, cubicaltt)
719
-
\end{itemize}
741
+
The unit type $\mathbf{1}$ (also written as \texttt{unit}) is the inductive type with a single constructor ★. It represents logical truth.
742
+
743
+
\begin{table}[ht!]
744
+
\tabstyle
745
+
\begin{tabular}{l}
746
+
\textbf{def} Unit : U := \textbf{1} \\
747
+
\textbf{def} star : Unit := ★ \\
748
+
\\
749
+
\textbf{def} Unit-ind (C : Unit $\rightarrow$ U) (u : C star) (z : Unit) : C z := \textbf{ind-unit} C u z
750
+
\end{tabular}
751
+
\end{table}
720
752
721
-
\subsection{Simplicial Types}
753
+
\subsubsection*{Boolean Type}
722
754
723
-
Modification of Anders with Simplicial types and Hopf Fibrations built intro the core of type checker
724
-
is called \textbf{Dan} with following recursive syntax (having $f$ as Simplecies and $coh$ as Path-coherence functions):
755
+
The boolean type $\mathbf{2}$ (also written as \texttt{bool}) is the inductive type with two constructors $0_2$ and $1_2$ (or \texttt{false} and \texttt{true}). It is used for case analysis and decision procedures.
\textbf{def} Bool-ind (C : Bool $\rightarrow$ U) (f : C false) (t : C true) (z : Bool) \\
765
+
\ \ : C z := \textbf{ind-bool} C f t z
730
766
\end{tabular}
731
767
\end{table}
732
768
733
-
and instantiation example:
769
+
\newpage
770
+
\subsubsection*{Natural Numbers}
771
+
772
+
The type of natural numbers $\mathbb{N}$ is a primitive type in \anders, providing efficient normalization for arithmetic operations. Its elimination rule is provided by the \texttt{ind-Nat} primitive.
Well-founded trees (W-types) are the building blocks for all other inductive types in \anders. A W-type $\mathsf{W}(x : A), B(x)$ is specified by a type $A$ of shapes and a family $B : A \to U$ of positions for each shape.
789
+
790
+
\begin{table}[ht!]
791
+
\tabstyle
792
+
\begin{tabular}{l}
793
+
\textbf{def} W (A : U) (B : A $\rightarrow$ U) : U := \textbf{W} A B \\
794
+
\textbf{def} sup (A : U) (B : A $\rightarrow$ U) (a : A) (f : B a $\rightarrow$ W A B) \\
795
+
\ \ : W A B := \textbf{sup} a f \\
796
+
\\
797
+
\textbf{def} W-ind (A : U) (B : A $\rightarrow$ U) (C : W A B $\rightarrow$ U) \\
798
+
\ \ (g : $\Pi$ (a : A) (f : B a $\rightarrow$ W A B), ($\Pi$ (b : B a), C (f b)) $\rightarrow$ C (sup A B a f)) \\
799
+
\ \ (w : W A B) : C w := \textbf{ind-W} A B C g w
744
800
\end{tabular}
745
801
\end{table}
746
802
803
+
\newpage
804
+
\subsection{Higher Inductive Types}
805
+
806
+
Higher inductive types (HITs) generalize inductive types by allowing constructors that target path types, enabling the representation of cell complexes and other quotient-like structures. \anders\ provides two primitive HIT constructions: coequalizers and hub-and-spoke discs. These primitives, combined with W-types, are sufficient to represent a wide range of HITs, including spheres $S^n$, suspensions, and truncations, following the Three-HIT theorem approach \cite{BauerWeide}.
807
+
808
+
\subsubsection*{Coequalizers}
809
+
810
+
The coequalizer $\mathsf{coequ}(f, g)$ of two parallel maps $f, g : A \to B$ is a higher inductive type that identifies the images of $f$ and $g$ in $B$. That is, for every $a : A$, we have a path $f(a) = g(a)$ in $\mathsf{coequ}(f, g)$. This allows for computable representations of the circle $S^1$, the torus, and general colimits.
811
+
812
+
\begin{table}[ht!]
813
+
\tabstyle
814
+
\begin{tabular}{l}
815
+
\textbf{def} coeq (A B : U) (f g : A $\rightarrow$ B) : U := \textbf{coequ} A B f g \\
816
+
\textbf{def} iota (A B : U) (f g : A $\rightarrow$ B) (x : B) : \textbf{coequ} A B f g := $\iota_2$ A B f g x \\
817
+
\textbf{def} resp (A B : U) (f g : A $\rightarrow$ B) (x : A) \\
818
+
\ \ : Path (\textbf{coequ} A B f g) ($\iota_2$ A B f g (f x)) ($\iota_2$ A B f g (g x)) \\
819
+
\ := <i> \textbf{resp} A B f g x @ i \\
820
+
\\
821
+
\textbf{def} coequ-ind' (A B : U) (f g : A $\rightarrow$ B) (X : \textbf{coequ} A B f g $\rightarrow$ U) \\
822
+
\ \ (i : $\Pi$ (b : B), X (iota A B f g b)) \\
823
+
\ \ ($\rho$ : $\Pi$ (x : A), PathP (<i> X (resp A B f g x @ i)) (i (f x)) (i (g x))) \\
824
+
\ \ (z : \textbf{coequ} A B f g) : X z \\
825
+
\ := coequ-ind A B f g X i $\rho$ z
826
+
827
+
\end{tabular}
828
+
\end{table}
829
+
830
+
\subsubsection*{Hub-and-Spoke Discs}
831
+
832
+
The hub-and-spoke construction $\mathsf{disc}(S, A)$ attaches a "disc" to a type $A$ for every map $f : S \to\mathsf{disc}(S, A)$. This is achieved by adding a "hub" point for each such $f$ and a "spoke" path connecting the hub to $f(s)$ for every $s : S$. This construction is particularly useful for defining $n$-truncations and other cell complexes where a point must be connected to an entire family of points.
833
+
834
+
\begin{table}[ht!]
835
+
\tabstyle
836
+
\begin{tabular}{l}
837
+
\textbf{def} hs (S A : U) : U := \textbf{disc} S A \\
838
+
\textbf{def} center (S A : U) (a : A) : hs S A := \textbf{base} S A a \\
839
+
\textbf{def} hub' (S A : U) (f : S $\rightarrow$ hs S A) : hs S A := \textbf{hub} S A f \\
840
+
\textbf{def} spoke' (S A : U) (f : S $\rightarrow$ hs S A) (s : S) \\
841
+
\ \ : PathP (<i> hs S A) (hub' S A f) (f s) := \textbf{spoke} S A f s \\
842
+
\\
843
+
\textbf{def} hs-ind (S A : U) (X : hs S A $\rightarrow$ U) \\
844
+
\ \ (nCenter : $\Pi$ (a : A), X (center S A a)) \\
845
+
\ \ (nHub : $\Pi$ (f : S $\rightarrow$ hs S A) (nF : $\Pi$ (s : S), X (f s)), X (hub' S A f)) \\
846
+
\ \ (nSpoke : $\Pi$ (f : S $\rightarrow$ hs S A) (nF : $\Pi$ (s : S), X (f s)) (s : S), \\
847
+
\ \ \ \ PathP (<i> X (spoke' S A f s @ i)) (nHub f nF) (nF s)) \\
848
+
\ \ (z : hs S A) : X z := \textbf{disc-ind} S A X nCenter nHub nSpoke z
849
+
\end{tabular}
850
+
\end{table}
851
+
852
+
853
+
% \subsection{Simplicial Types}
854
+
855
+
% Modification of Anders with Simplicial types and Hopf Fibrations built intro the core of type checker
856
+
% is called \textbf{Dan} with following recursive syntax (having $f$ as Simplecies and $coh$ as Path-coherence functions):
hcompⁱ (W (x : A), B) [φ ↦ sup a f] (sup a₀ f₀) \\
957
+
\ = sup (hcompⁱ A [φ ↦ a] a₀) (hcompⁱ (B(v) → W) [φ ↦ f] f₀), v = hFillⁱ A [φ ↦ a] a₀ \\
958
+
hcompⁱ (Coequ A B f g) [φ ↦ ι₂ u] (ι₂ u₀) = ι₂ (hcompⁱ B [φ ↦ u] u₀) \\
959
+
hcompⁱ (Coequ A B f g) [φ ↦ resp a j] (resp a₀ j) = resp (hcompⁱ A [φ ↦ a] a₀) j \\
960
+
hcompⁱ (Disc S A) [φ ↦ base a] (base a₀) = base (hcompⁱ A [φ ↦ a] a₀) \\
961
+
hcompⁱ (Disc S A) [φ ↦ hub f] (hub f₀) = hub (hcompⁱ (S → Disc S A) [φ ↦ f] f₀) \\
962
+
hcompⁱ (Disc S A) [φ ↦ spoke f y j] (spoke f₀ y₀ j) \\
963
+
\ = spoke (hcompⁱ (S → Disc S A) [φ ↦ f] f₀) (hcompⁱ S [φ ↦ y] y₀) j \\
964
+
hcompⁱ (ℑ A) [φ ↦ ℑ-unit u] (ℑ-unit u₀) = ℑ-unit (hcompⁱ A [φ ↦ u] u₀) \\
965
+
hcompⁱ (♭ A) [φ ↦ ♭-unit u] (♭-unit u₀) = ♭-unit (hcompⁱ A [φ ↦ u] u₀) \\
966
+
hFillⁱ A [φ ↦ u] u₀ = hcompʲ A [φ ↦ u(i/i∧j), (i=0) ↦ u₀] u₀ : A \\
967
+
\end{tabular}
968
+
\end{table}
969
+
970
+
\newpage
971
+
\section{Annex B. HoTT Mathematics}
789
972
\label{sec:hott-applications}
790
973
791
974
Mathematics in Homotopy Type Theory has seen substantial formalization efforts across multiple proof assistants (including Anders, Cubical Agda, Lean, Coq, etc.). Below is a (non-exhaustive) list of notable results that have been mechanized.
\contitem\title{Anders: Modal Homotopy Type System for Computable Modal Homotopy Type Theory and Differential Geometry}\author{Maksym Sokhatskyi}\page{:1--:16}
1
+
\contitem\title{Anders: Modal Homotopy Type System for Computable Modal Homotopy Type Theory and Differential Geometry}\author{Maksym Sokhatskyi}\page{:1--:19}
0 commit comments