Exploring fractal mazes in cubical type theory https://f.monade.li/maze.pdf

bibliography.bibtex

@misc{Rijke:2022,
  title={Introduction to Homotopy Type Theory},
  author={Egbert Rijke},
  year={2022},
  eprint={2212.11082},
  archivePrefix={arXiv},
  primaryClass={math.LO}
}

@misc{CCHM,
  title={Cubical Type Theory: a constructive interpretation of the univalence axiom},
  author={Cyril Cohen and Thierry Coquand and Simon Huber and Anders Mörtberg},
  year={2016},
  eprint={1611.02108},
  archivePrefix={arXiv},
  primaryClass={cs.LO}
}

@misc{Symmetry,
  title = {Symmetry},
  author = {Marc Bezem and Ulrik Buchholtz and Pierre Cagne
  and Bjørn Ian Dundas and Daniel R. Grayson},
  date = {2023-08-23},
  howpublished = {\url{https://github.com/UniMath/SymmetryBook}},
  note = {Commit: \texttt{33011eb}}
}

@book{HoTT,
  author    = {The {Univalent Foundations Program}},
  title     = {Homotopy Type Theory: Univalent Foundations of Mathematics},
  publisher = {\url{https://homotopytypetheory.org/book}},
  address   = {Institute for Advanced Study},
  year      = 2013
}

@article{cubicalagda,
author = {Vezzosi, Andrea and M\"{o}rtberg, Anders and Abel, Andreas},
title = {Cubical agda: a dependently typed programming language with univalence and higher inductive types},
year = {2019},
issue_date = {August 2019},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {3},
number = {ICFP},
url = {https://doi.org/10.1145/3341691},
doi = {10.1145/3341691},
abstract = {Proof assistants based on dependent type theory provide expressive languages for both programming and proving within the same system. However, all of the major implementations lack powerful extensionality principles for reasoning about equality, such as function and propositional extensionality. These principles are typically added axiomatically which disrupts the constructive properties of these systems. Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence axiom and higher inductive types. This paper describes an extension of the dependently typed functional programming language Agda with cubical primitives, making it into a full-blown proof assistant with native support for univalence and a general schema of higher inductive types. These new primitives make function and propositional extensionality as well as quotient types directly definable with computational content. Additionally, thanks also to copatterns, bisimilarity is equivalent to equality for coinductive types. This extends Agda with support for a wide range of extensionality principles, without sacrificing type checking and constructivity.},
journal = {Proc. ACM Program. Lang.},
month = {jul},
articleno = {87},
numpages = {29},
keywords = {Cubical Type Theory, Dependent Pattern Matching, Higher Inductive Types, Univalence}
}

@online{1lab,
  author = {The {1Lab Development Team}},
  title = {{The 1Lab}},
  url = {https://1lab.dev},
  year = 2024,
}

@ONLINE {afpc2024,
    author = {The {\texttt{\#ircpuzzles} team}},
    title  = "2024 April Fool's Puzzle Competition",
    month  = "apr",
    year   = "2024",
    url    = "https://ircpuzzles.org"
}

@BOOK{wolf,
  title     = "101 enigmatic puzzles",
  author    = "Wolf, Mark J P",
  publisher = "BookBaby",
  month     =  mar,
  year      =  2020,
  address   = "Pennsauken, NJ"
}

@inproceedings{pi1s1,
author = {Licata, Daniel R. and Shulman, Michael},
title = {Calculating the Fundamental Group of the Circle in Homotopy Type Theory},
year = {2013},
isbn = {9780769550206},
publisher = {IEEE Computer Society},
address = {USA},
url = {https://doi.org/10.1109/LICS.2013.28},
doi = {10.1109/LICS.2013.28},
abstract = {Recent work on homotopy type theory exploits an exciting new correspondence between Martin-Lof's dependent type theory and the mathematical disciplines of category theory and homotopy theory. The mathematics suggests new principles to add to type theory, while the type theory can be used in novel ways to do computer-checked proofs in a proof assistant. In this paper, we formalize a basic result in algebraic topology, that the fundamental group of the circle is the integers. Our proof illustrates the new features of homotopy type theory, such as higher inductive types and Voevodsky's univalence axiom. It also introduces a new method for calculating the path space of a type, which has proved useful in many other examples.},
booktitle = {Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science},
pages = {223–232},
numpages = {10},
series = {LICS '13}
}

Maze.hs

{-# LANGUAGE BlockArguments #-}

import Control.Monad
import Data.Foldable
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Sequence qualified as Seq
import Data.PriorityQueue.FingerTree qualified as PQ

type Node = Char -- 'l', 'z', 'A', 'B', 'C', …
type Locus = Char -- 'a', 'b', 'c'
data Op = Plus1 | Times3 deriving Show
data Warp = In Locus | Out Locus deriving Show
type Path = ([Op], [Warp])

flipWarp (In x) = Out x
flipWarp (Out x) = In x

flipPath (ops, warps) = (reverse ops, flipWarp <$> reverse warps)

paths :: [(Node, Path, Node)]
paths =
  [ ('l', ([Times3, Times3], [In 'c']), 'A')
  , ('B', ([Times3], [Out 'a']), 'z')
  , ('A', ([Plus1], [In 'a']), 'C')
  , ('B', ([], [In 'a']), 'K')
  , ('B', ([Times3], [In 'c']), 'D')
  , ('B', ([Plus1], [In 'b']), 'E')
  , ('C', ([Plus1], [In 'a']), 'C')
  , ('D', ([Plus1, Times3], [In 'a']), 'D')
  , ('E', ([Times3, Plus1], [In 'a']), 'B')
  , ('E', ([Plus1], [In 'c']), 'L')
  , ('F', ([Times3], [In 'a']), 'G')
  , ('G', ([Plus1, Times3], [In 'b']), 'D')
  , ('H', ([Times3, Plus1], [In 'b']), 'B')
  , ('K', ([Times3], [In 'b']), 'G')
  , ('L', ([Times3], [In 'b']), 'A')
  , ('H', ([Plus1], [Out 'a', In 'c']), 'A')
  , ('A', ([Times3, Plus1], [Out 'a', In 'b']), 'D')
  , ('C', ([Plus1, Times3], [Out 'b', In 'c']), 'D')
  , ('A', ([Times3, Times3], [Out 'c', In 'c']), 'E')
  , ('D', ([Times3, Times3], [Out 'a', In 'a']), 'A')
  , ('C', ([Times3, Times3], [Out 'b', In 'c']), 'G')
  , ('C', ([Plus1, Plus1], [Out 'b', In 'c']), 'G')
  ]

adj :: Map Node [(Path, Node)]
adj = Map.fromListWith (++) do
  (a, p, b) <- paths
  [(a, [(p, b)]), (b, [(flipPath p, a)])]

type State = (([Locus], Node), Integer, [([Locus], Node)], [Warp])
link = ("", 'l')
zelda = ("", 'z')
initState n = (n, 3, [], [])
loc (n, _, _, _) = n
rep = loc

tryWarp :: [Locus] -> Warp -> Maybe [Locus]
tryWarp l (In x) = Just (x:l)
tryWarp (l:ls) (Out x) | l == x = Just ls
tryWarp _ _ = Nothing

next :: State -> [(State, Integer)]
next ((l, n), score, hist, warps) =
  [ (((l', n'), score', hist ++ [(l', n')], warps ++ warps'), 1)
  | ((ops', warps'), n') <- adj Map.! n
  , Just l' <- [foldlM tryWarp l warps']
  , length l' <= 9
  , let score' = foldl (flip doOp) score ops'
  ]

doOp Times3 = (* 3)
doOp Plus1 = (+ 1)

main =
  mapM_ print
  -- print $ head
  -- $ map (\(((l, n), score, (ops, warps)), _) -> (score, ops, warps))
  $ filter (\(x, _) -> loc x == zelda)
  $ dijkstraOn rep next [initState link]

dijkstra :: (Num n, Ord n, Ord a) => (a -> [(a, n)]) -> [a] -> [(a, n)]
dijkstra = dijkstraOn id

dijkstraOn :: (Num n, Ord n, Ord b) => (a -> b) -> (a -> [(a, n)]) -> [a] -> [(a, n)]
dijkstraOn rep next = astarOn rep next'
  where next' n = [(n', c, 0) | (n', c) <- next n]

astar :: (Num n, Ord n, Ord a) => (a -> [(a, n, n)]) -> [a] -> [(a, n)]
astar = astarOn id

insertMaybeSet :: Ord a => a -> Set a -> Maybe (Set a)
insertMaybeSet = Set.alterF (\p -> True <$ guard (not p))

astarOn :: (Num n, Ord n, Ord b) => (a -> b) -> (a -> [(a, n, n)]) -> [a] -> [(a, n)]
astarOn rep next start = go Set.empty (PQ.fromList $ map (\s -> (0, (0, s))) start) where
  go seen q
    | Just ((_, (d, n)), q') <- PQ.minViewWithKey q =
      let r = rep n
          insert q (n', c, h) = PQ.insert (d' + h) (d', n') q where d' = d + c
      in case insertMaybeSet r seen of
        Nothing -> go seen q'
        Just seen' -> (n, d):go seen' (foldl' insert q' (next n))
    | otherwise = []

Maze.lagda.tex

% https://f.monade.li/maze.pdf
\documentclass[a4paper,11pt]{article}
\usepackage{amsmath,amssymb,amsthm}
\usepackage[margin=1in]{geometry}
\usepackage[british]{babel}
\usepackage{graphicx}
\usepackage{microtype}
\usepackage{csquotes}

\title{Exploring fractal mazes in cubical type theory}
\author{\href{https://monade.li/}{\texttt{ncf}}}
\makeatletter
\let\thetitle\@title
\makeatother

\usepackage[dvipsnames,svgnames*,x11names*]{xcolor}
\definecolor{linkcolor}{HTML}{b603ff}
\usepackage{hyperref}
\hypersetup{
  pdftitle={\thetitle},
  pdfauthor=Naïm Favier,
  colorlinks=true,
  linkcolor=linkcolor,
  citecolor=linkcolor,
  urlcolor=linkcolor,
  breaklinks=true}
\usepackage[nameinlink]{cleveref}
\usepackage{multicol}
\usepackage[
    style=alphabetic,
    maxalphanames=6,
    maxnames=6,
]{biblatex}
\addbibresource{bibliography.bibtex}
\usepackage{float}
\usepackage{agda}

\usepackage{ifthen}
\DeclareRobustCommand{\AgdaFormat}[2]{%
  \ifthenelse{\equal{#1}{≡}}{$\equiv$}{#2}}

\usepackage{libertine}
\usepackage{fontspec}
\setmonofont[Scale=0.7]{JuliaMono}

\newtheorem{theorem}{Theorem}

\begin{document}

\maketitle

\setlength{\parskip}{0.5em}
\setlength{\parindent}{1em}

\begin{code}[hide]
open import 1Lab.Prelude
open import Homotopy.Connectedness
open import Data.Int renaming (Int to ℤ)
open import Data.Int.Universal

open Integers Int-integers

module wip.Maze where
\end{code}

The following puzzle is taken from the 2024 April Fool's Puzzle Competition \autocite[level~05]{afpc2024},
and originally due to Mark J. P. Wolf~\autocite{wolf}. The goal is to find a path from a given
start point to a given end point in a ``fractal'' maze with three loci of
self-similarity (\cref{maze}).

\begin{figure}[h]
  \centering
    \includegraphics[width=0.75\textwidth]{map}
  \caption{A fractal maze (design by Mark J. P. Wolf, tileset by \href{https://za3k.com/}{\texttt{za3k}}, annotations mine).}
  \label{maze}
\end{figure}

In this note, we approach this problem through the lens of homotopy type theory~\autocite{HoTT}:
concerning ourselves only with the \emph{homotopical} structure of the maze, it is
possible to model it as a higher inductive type generated by

\begin{itemize}
\item a point constructor for each of the labeled nodes, denoted by capital letters, as well
as the start point (\AgdaInductiveConstructor{link}) and end point (\AgdaInductiveConstructor{zelda});
\item three recursive constructors $a$, $b$ and $c$ taking a point of the maze to its image under one of the self-similarities;
\item path constructors representing the possible routes of the maze. For example, there is a path connecting
the $B$ node to the image of the $K$ node inside the $a$ submaze: $B \equiv a\ K$.
\end{itemize}

Terms of this type are then interpreted as points on the maze, while the
identity type $A \equiv B$ between any two points represents the type\footnote{In fact we conjecture each of these types to be a \emph{set}, so that the maze is a groupoid, but we will not attempt to show this here.} of \emph{paths}
in the maze from $A$ to $B$, considered up to homotopy.

We formalise this using the Cubical Agda~\autocite{cubicalagda} proof assistant, an implementation of cubical type theory~\autocite{CCHM} that
gives computational content to the univalence axiom. This file is a Literate Agda file
and can be type-checked against the 1Lab~\autocite{1lab}, a formalised library of univalent mathematics
in Cubical Agda. We refer the reader to the 1Lab's website for the definitions
of the basic tools of cubical type theory used in the following code.

\begin{figure}[h]
\centering
\begin{multicols}{2}
\begin{code}
data Maze : Type where
  link zelda : Maze
  A B C D E F G H K L : Maze
  a b c : Maze → Maze
  link≡cA : link ≡ c A
  aB≡zelda : a B ≡ zelda
  A≡aC : A ≡ a C
  B≡aK : B ≡ a K
  B≡cD : B ≡ c D
  B≡bE : B ≡ b E
  C≡aC : C ≡ a C
  D≡aD : D ≡ a D
\end{code}
\columnbreak
\begin{code}
  E≡aB : E ≡ a B
  E≡cL : E ≡ c L
  F≡aG : F ≡ a G
  G≡bD : G ≡ b D
  H≡bB : H ≡ b B
  K≡bG : K ≡ b G
  L≡bA : L ≡ b A
  aH≡cA : a H ≡ c A
  aA≡bD : a A ≡ b D
  bC≡cD : b C ≡ c D
  cA≡cE : c A ≡ c E
  aD≡aA : a D ≡ a A
  bC≡cG : b C ≡ c G
\end{code}
\end{multicols}
\end{figure}

\begin{code}[hide]
Maze-elim-prop!
  : ∀ {ℓ} {P : Maze → Type ℓ} ⦃ _ : ∀ {x} → H-Level (P x) 1 ⦄
  → P link → P zelda → P A → P B → P C → P D → P E → P F → P G → P H → P K → P L
  → (∀ x → P x → P (a x)) → (∀ x → P x → P (b x)) → (∀ x → P x → P (c x))
  → ∀ x → P x
Maze-elim-prop! {P = P} Plink Pzelda PA PB PC PD PE PF PG PH PK PL Pa Pb Pc = go where
  go : ∀ x → P x
  go link = Plink
  go zelda = Pzelda
  go A = PA
  go B = PB
  go C = PC
  go D = PD
  go E = PE
  go F = PF
  go G = PG
  go H = PH
  go K = PK
  go L = PL
  go (a x) = Pa x (go x)
  go (b x) = Pb x (go x)
  go (c x) = Pc x (go x)
  go (link≡cA i) = is-prop→pathp {B = λ i → P (link≡cA i)} (λ _ → hlevel 1) Plink (Pc A PA) i
  go (aB≡zelda i) = is-prop→pathp {B = λ i → P (aB≡zelda i)} (λ _ → hlevel 1) (Pa B PB) Pzelda i
  go (A≡aC i) = is-prop→pathp {B = λ i → P (A≡aC i)} (λ _ → hlevel 1) PA (Pa C PC) i
  go (B≡aK i) = is-prop→pathp {B = λ i → P (B≡aK i)} (λ _ → hlevel 1) PB (Pa K PK) i
  go (B≡cD i) = is-prop→pathp {B = λ i → P (B≡cD i)} (λ _ → hlevel 1) PB (Pc D PD) i
  go (B≡bE i) = is-prop→pathp {B = λ i → P (B≡bE i)} (λ _ → hlevel 1) PB (Pb E PE) i
  go (C≡aC i) = is-prop→pathp {B = λ i → P (C≡aC i)} (λ _ → hlevel 1) PC (Pa C PC) i
  go (D≡aD i) = is-prop→pathp {B = λ i → P (D≡aD i)} (λ _ → hlevel 1) PD (Pa D PD) i
  go (E≡aB i) = is-prop→pathp {B = λ i → P (E≡aB i)} (λ _ → hlevel 1) PE (Pa B PB) i
  go (E≡cL i) = is-prop→pathp {B = λ i → P (E≡cL i)} (λ _ → hlevel 1) PE (Pc L PL) i
  go (F≡aG i) = is-prop→pathp {B = λ i → P (F≡aG i)} (λ _ → hlevel 1) PF (Pa G PG) i
  go (G≡bD i) = is-prop→pathp {B = λ i → P (G≡bD i)} (λ _ → hlevel 1) PG (Pb D PD) i
  go (H≡bB i) = is-prop→pathp {B = λ i → P (H≡bB i)} (λ _ → hlevel 1) PH (Pb B PB) i
  go (K≡bG i) = is-prop→pathp {B = λ i → P (K≡bG i)} (λ _ → hlevel 1) PK (Pb G PG) i
  go (L≡bA i) = is-prop→pathp {B = λ i → P (L≡bA i)} (λ _ → hlevel 1) PL (Pb A PA) i
  go (aH≡cA i) = is-prop→pathp {B = λ i → P (aH≡cA i)} (λ _ → hlevel 1) (Pa H PH) (Pc A PA) i
  go (aA≡bD i) = is-prop→pathp {B = λ i → P (aA≡bD i)} (λ _ → hlevel 1) (Pa A PA) (Pb D PD) i
  go (bC≡cD i) = is-prop→pathp {B = λ i → P (bC≡cD i)} (λ _ → hlevel 1) (Pb C PC) (Pc D PD) i
  go (cA≡cE i) = is-prop→pathp {B = λ i → P (cA≡cE i)} (λ _ → hlevel 1) (Pc A PA) (Pc E PE) i
  go (aD≡aA i) = is-prop→pathp {B = λ i → P (aD≡aA i)} (λ _ → hlevel 1) (Pa D PD) (Pa A PA) i
  go (bC≡cG i) = is-prop→pathp {B = λ i → P (bC≡cG i)} (λ _ → hlevel 1) (Pb C PC) (Pc G PG) i
\end{code}

As \AgdaDatatype{Maze} is the free $\infty$-groupoid generated by the given data, we automatically
have all concatenations of paths, as well as an inverse to every path.
Furthermore, the functorial action of the recursive constructors implies
that every ``top-level'' path has a counterpart in every recursive submaze
(for example, we have \texttt{ap a C≡aC : a C ≡ a (a C)}),
thus ensuring that this is a faithful representation of the maze in \cref{maze}.

We define a \emph{solution} of the maze to be a path $\AgdaInductiveConstructor{link} \equiv \AgdaInductiveConstructor{zelda}$.
A simple graph exploration reveals at least two solutions\footnote{The solutions are named $67161$ and $187203$
for reasons that are out of the scope of this document, but which the reader may easily guess.} given in \cref{solutions}.
The indentation style makes apparent that the first solution has a
``recursion depth'' of four levels, while the second solution goes six
levels deep.

\begin{figure}[H]
\centering
\begin{multicols}{2}
\begin{code}
solution67161 : link ≡ zelda
solution67161
  = link≡cA
  ∙ ap c ( A≡aC
         ∙ ap a ( C≡aC
                ∙ sym A≡aC)
         ∙ aA≡bD
         ∙ ap b ( D≡aD
                ∙ aD≡aA
                ∙ ap a ( A≡aC
                       ∙ sym C≡aC)
                ∙ sym A≡aC)
         ∙ sym L≡bA)
  ∙ sym E≡cL
  ∙ E≡aB
  ∙ aB≡zelda
\end{code}
\columnbreak
\begin{code}
solution187203 : link ≡ zelda
solution187203
  = link≡cA
  ∙ sym aH≡cA
  ∙ ap a ( H≡bB
         ∙ ap b ( B≡aK
                ∙ ap a ( K≡bG
                       ∙ ap b ( G≡bD
                              ∙ sym aA≡bD
                              ∙ ap a ( A≡aC
                                     ∙ sym C≡aC)
                              ∙ sym C≡aC)
                       ∙ bC≡cD
                       ∙ sym B≡cD)
                ∙ sym E≡aB)
         ∙ sym B≡bE)
  ∙ aB≡zelda
\end{code}
\end{multicols}
\caption{Two possible ways for Link to rescue Zelda.}
\label{solutions}
\end{figure}

It is then natural to ask whether these solutions are homotopic to each other.
It turns out that they are not, and in fact there is an \emph{infinite} number of
distinct solutions. More precisely, we will show the following:

\begin{theorem}
\label{retract}
The space of solutions of the maze (i.e. paths $\AgdaInductiveConstructor{link} \equiv \AgdaInductiveConstructor{zelda}$)
retracts onto $\mathbb{Z}$.
\end{theorem}

\begin{proof}
The idea of the proof closely follows the characterisation of the loop space
of the circle~\autocite{pi1s1}: we start by defining a covering space over the maze with
$\mathbb{Z}$ layers, such that transport is constant everywhere except over
a chosen ``bridge'' \AgdaInductiveConstructor{aH≡cA} crossed by one solution but not the other:
when crossing that bridge (at the top-level only), we apply the $+1 : \mathbb{Z} \simeq \mathbb{Z}$
equivalence using univalence.

\begin{multicols}{3}
\begin{code}
Cover : Maze → Type
Cover link = ℤ
Cover zelda = ℤ
Cover A = ℤ
Cover B = ℤ
Cover C = ℤ
Cover D = ℤ
Cover E = ℤ
Cover F = ℤ
Cover G = ℤ
Cover H = ℤ
Cover K = ℤ
Cover L = ℤ
\end{code}
\columnbreak
\begin{code}
Cover (a m) = ℤ
Cover (b m) = ℤ
Cover (c m) = ℤ
Cover (link≡cA i) = ℤ
Cover (aB≡zelda i) = ℤ
Cover (A≡aC i) = ℤ
Cover (B≡aK i) = ℤ
Cover (B≡cD i) = ℤ
Cover (B≡bE i) = ℤ
Cover (C≡aC i) = ℤ
Cover (D≡aD i) = ℤ
Cover (E≡aB i) = ℤ
Cover (E≡cL i) = ℤ
\end{code}
\columnbreak
\begin{code}
Cover (F≡aG i) = ℤ
Cover (G≡bD i) = ℤ
Cover (H≡bB i) = ℤ
Cover (K≡bG i) = ℤ
Cover (L≡bA i) = ℤ
Cover (aH≡cA i) = ua rotate i
Cover (aA≡bD i) = ℤ
Cover (bC≡cD i) = ℤ
Cover (cA≡cE i) = ℤ
Cover (aD≡aA i) = ℤ
Cover (bC≡cG i) = ℤ
\end{code}
\end{multicols}

Thus, transporting 0 along some path $p$ in this covering space
keeps track of how many times the path crosses \AgdaInductiveConstructor{aH≡cA}; however, unlike
the $+1$ bonus given by the Pac-Man ghost sitting on the bridge
(circled in \cref{maze}), this $+1$ only takes effect when crossing the
bridge \emph{top-down}, from $a$ to $c$; when taking the opposite path from $c$
to $a$, we must instead apply the equivalence in reverse and subtract $1$.
This defines a function \AgdaFunction{winding} from the space of solutions to $\mathbb{Z}$.

\begin{code}
winding : link ≡ zelda → ℤ
winding p = subst Cover p 0
\end{code}

Thanks to the computational power of cubical type theory, we can directly check
that the 67161 solution does not cross the \AgdaInductiveConstructor{aH≡cA} bridge,
while the 187203 solution crosses it once backwards:

\begin{code}
_ : winding solution67161 ≡ 0
_ = refl

_ : winding solution187203 ≡ -1
_ = refl
\end{code}

We now define, for every integer $n$, a solution
that passes over the bridge $n$ times. The idea is simple: we start
by going from \AgdaInductiveConstructor{link} to \AgdaInductiveConstructor{zelda} using the 67161 solution, and then \AgdaFunction{loop}
from \AgdaInductiveConstructor{zelda} to \AgdaInductiveConstructor{zelda} $n$ times by concatenating the two solutions.

\begin{code}
loop : zelda ≡ zelda
loop = sym solution187203 ∙ solution67161

loopⁿ : ℤ → link ≡ zelda
loopⁿ = map-out solution67161 (∙-post-equiv loop)
\end{code}

To conclude the proof of \cref{retract}, we show that $\text{winding}(\text{loop}^n) \equiv n$.
This is once again straightforward by computation: the winding number of
the 67161 solution computes to 0, and appending one \AgdaFunction{loop}
increases the winding number by one, thus by the universal property of the
integers the function $\AgdaFunction{winding} \circ \AgdaFunction{loopⁿ}$ is
equal to $\mathrm{id}_\mathbb{Z}$.

\begin{code}
infinite-solutions : is-left-inverse winding loopⁿ
infinite-solutions n = map-out-unique (winding ∘ loopⁿ) refl
  (λ n → ap winding (map-out-rotate _ _ n)) n
  ∙ ℤ-η n
\end{code}
\end{proof}

We can also show that it is possible to go from any point in the maze to any other point.
In particular, a solution can visit points at arbitrary recursion depths.

\begin{theorem}
\AgdaDatatype{Maze} is a connected type.
\end{theorem}

\begin{proof}
Further graph exploration shows that there are paths from \AgdaInductiveConstructor{link}
to every other top-level node, and there are paths descending from every level to its
\AgdaInductiveConstructor{a}, \AgdaInductiveConstructor{b} and \AgdaInductiveConstructor{c}
sublevel, so this is simply a matter of wrangling paths.

\begin{code}
A≡C : A ≡ C
A≡C = A≡aC ∙ sym C≡aC
aA≡G : a A ≡ G
aA≡G = aA≡bD ∙ sym G≡bD
D≡aA : D ≡ a A
D≡aA = D≡aD ∙ aD≡aA
caA≡B : c (a A) ≡ B
caA≡B = ap c (sym D≡aA) ∙ sym B≡cD
caA≡baC : c (a A) ≡ b (a C)
caA≡baC = ap c aA≡G ∙ sym bC≡cG ∙ ap b C≡aC
B≡abaA : B ≡ a (b (a A))
B≡abaA = B≡aK ∙ ap a (K≡bG ∙ ap b (sym aA≡G))
link≡caA : link ≡ c (a A)
link≡caA = link≡cA ∙ ap c (A≡aC ∙ ap a (sym A≡C))
link≡baC : link ≡ b (a C)
link≡baC = link≡caA ∙ caA≡baC
link≡baA : link ≡ b (a A)
link≡baA = link≡baC ∙ ap b (ap a (sym A≡C))
link≡aC : link ≡ a C
link≡aC = link≡baA ∙ ap b (sym D≡aA) ∙ sym aA≡bD ∙ ap a A≡C
link≡A : link ≡ A
link≡A = link≡aC ∙ sym A≡aC
link≡B : link ≡ B
link≡B = link≡caA ∙ caA≡B
link≡C : link ≡ C
link≡C = link≡aC ∙ sym C≡aC
link≡D : link ≡ D
link≡D = link≡baA ∙ ap b (sym D≡aA) ∙ sym aA≡bD ∙ sym D≡aA
link≡E : link ≡ E
link≡E = link≡caA ∙ ap c (aA≡bD ∙ ap b (D≡aA ∙ ap a A≡C ∙ sym A≡aC) ∙ sym L≡bA) ∙ sym E≡cL
link≡F : link ≡ F
link≡F = link≡B ∙ B≡abaA ∙ ap a (ap b (sym D≡aA) ∙ sym G≡bD) ∙ sym F≡aG
link≡G : link ≡ G
link≡G = link≡baA ∙ ap b (sym D≡aA) ∙ sym G≡bD
link≡H : link ≡ H
link≡H
  = link≡B ∙ B≡bE
  ∙ ap b (E≡aB ∙ ap a (B≡cD ∙ sym bC≡cD ∙ ap b (C≡aC ∙ ap a (sym A≡C))) ∙ sym B≡abaA)
  ∙ sym H≡bB
link≡K : link ≡ K
link≡K = link≡baA ∙ ap b aA≡G ∙ sym K≡bG
link≡L : link ≡ L
link≡L = link≡baC ∙ ap b (sym A≡aC) ∙ sym L≡bA

Maze-is-connected : is-connected Maze
Maze-is-connected = is-connected∙→is-connected link-links where
  link-links : ∀ x → ∥ x ≡ link ∥
  link-links = ∥-∥-map sym ∘ Maze-elim-prop!
    (inc refl) (inc solution67161) (inc link≡A) (inc link≡B)
    (inc link≡C) (inc link≡D) (inc link≡E) (inc link≡F)
    (inc link≡G) (inc link≡H) (inc link≡K) (inc link≡L)
    (λ _ → map λ px → link≡C ∙ C≡aC ∙ ap a (sym link≡C ∙ px))
    (λ _ → map λ px → link≡K ∙ K≡bG ∙ ap b (sym link≡G ∙ px))
    (λ _ → map λ px → link≡cA ∙ ap c (sym link≡A ∙ px))

module _ {ℓ : Level} {A : Type ℓ} where
  fam : ∥ A ∥ → n-Type ℓ 0
  fam = rec! λ x → el! (Singleton x)
\end{code}
\end{proof}

\printbibliography[heading=bibintoc,title={References}]

\end{document}