I've been studying homotopy theory on myself for quite some time now, and it is to my understanding that there's still no generally accepted definition for $\infty$-groupoids. The closest to this is perhaps that of Kan complexes, but I find it very hard to work with. Therefore I've been trying to modify the definition of Kan complexes to find something easier to reason about, and recently I think I might have found something that just might work. Here's a brief summary of the definition I found:

Definition

For each $n\in\mathbb N$, let $[n]:=\{k\in\mathbb N\mid k<n\}$. Let $\mathbf{Fin}$ be the full subcategory of $\mathbf{Set}$ generated by all such $[n]$. Let $\mathbf{Fin_+}$ be the full subcategory of $\mathbf{Fin}$ generated by the non-empty sets, i.e. excluding $[0]$.

Let $\Delta^n:=\mathbf{Fin}(-,[n])$, which defines a presheaf over $\mathbf{Fin}$. Let $\Xi^n:\mathbf{Fin}^\mathrm{op}\to\mathbf{Set}$ be the presheaf that on objects, maps each $[m]$ to the set $\{h:[m]\to[n]\mid\mathrm{im}(h)\subsetneqq[n]\}$, where $\mathrm{im}(h)$ denotes the image of $h$, and on morphisms maps each $g$ to the function $h\mapsto h\circ g$. One can easily verify that this indeed defines a functor. Obviously each $\Xi^n$ is a subpresheaf of $\Delta^n$, and let this inclusion be denoted with $\iota_n:\Xi^n\hookrightarrow\Delta^n$.

We say that a presheaf $P$ over $\mathbf{Fin}$ has the filling property if for every $n\geq2$, $\mathbf{Set}^{\mathbf{Fin}^\mathrm{op}}(i_n,P):\mathbf{Set}^{\mathbf{Fin}^\mathrm{op}}(\Delta^n,P)\to\mathbf{Set}^{\mathbf{Fin}^\mathrm{op}}(\Xi^n,P)$ is surjective, i.e. for every $\phi:\Xi^n\to P$, there is a $\psi:\Delta^n\to P$ such that $\phi=\psi\circ\iota_n$. Finally, we say a presheaf $G$ over $\mathbf{Fin_+}$ is an $\infty$-groupoid if $G([1]\uplus-):\mathbf{Fin}^\mathrm{op}\to\mathbf{Set}$ has the filling property, where $\uplus$ denotes the binary coproduct in $\mathbf{Fin}$.

My Observations

So far, I have been able to prove that one can assign to every topological space $S$ an $\infty$-groupoid $G$ according to this definition such that each $G([n+1])$ is the set of $n$-simplices in $S$, and that this assignment is in fact a functor that preserves both binary products and coproducts.

Furthermore, I have found that given two presheaves $P$ and $Q$ over $\mathbf{Fin}$, it is pretty straightforward to construct a new presheaf $[P;Q]$ that corresponds to the space of natural transformations from $P$ to $Q$ (Altough whether this presheaf also has the filling property is something I'm still working on).

I've also formalized part of what I have so far herehere in Agda. In fact, this was my original goal: to construct models of HoTT within some version of MLTT.

My Questions

• Is there already some work similar to mine being done in homotopy theory? If so, where can I read about them?
• How does the definition I came up with relate to that of Kan complexes? Can one construct one from the other, or are they even equivalent?