Source-linked AI summary
Any colour you like, as long as it's UIP: Semi-simplicial types from weakenings and thinnings
Thorsten Altenkirch
TL;DR
The paper tackles the open problem of defining semi-simplicial types uniformly in HoTT by building their syntax and constructing SST n within it. The syntax can be made a set without K, but the naive interpretation still requires UIP for semantic types, so composition's coherences remain unresolved.
Problem
Book HoTT lacks a known uniform definition of semi-simplicial types, the structure used to present higher categories internally.
Source: §1 · p. 1Method
Results
SST n is constructed uniformly in the syntax, but its naive interpretation needs UIP for the semantic types.
Source: §6 · p. 6, §7 · pp. 6–7Takeaways & Limitations
The coherence of composing non-invertible maps must be supplied either in the syntax or the semantics; this approach does not eliminate that obstruction.
Source: §9 · p. 9, §11 · p. 11The naive interpretation transports along propositional equations, and making those transports agree requires UIP for arbitrary semantic types.
Source: §7 · pp. 6–7
Abstract
from arXiv · showhide
We explain an attempt to define semi-simplicial types (SST) in homotopy type theory by first defining a small type theory whose contexts are exactly the data of semi-simplicial types, constructing $\mathrm{SST}\,n$ uniformly in that syntax, and then interpreting the syntax in the universe. The syntax can be defined without any truncation and without K, and the construction of $\mathrm{SST}\,n$ goes through. The naive interpretation does not: it transports along the semantic images of equations that hold only propositionally, and making these transports agree needs uniqueness of identity proofs (UIP) for the semantic types. Moving the problem into the syntax, by making composition a constructor of a higher inductive-inductive type (HIIT), does not remove it either: it reappears as a coherence problem in the syntax. Fording the HIIT (storing equations instead of computed indices), with conditional rules, makes the syntax provably a set. This is UIP for the syntax, obtained by encode-decode, and it does not by itself restrict the semantics; but the naive interpretation of the conditional rules again needs UIP for the semantic types. A semantics into groupoids that avoids UIP will be discussed in a separate note. The Agda development accompanying this note is in the repository https://github.com/txa/sst-new.
1 Why semi-simplicial types?
Semi-simplicial types would let HoTT represent higher categories internally, but their uniform construction remains open in book HoTT. The paper frames the challenge through triangles, where compatible selections must compose.
1 Why semi-simplicial types?
- A standard presentation of an (∞, 1)-category uses a semi-simplicial object of types satisfying Segal and completeness conditions, so defining SST in HoTT could represent higher categories internally.This includes the (∞, 1)-category of types itself.Source: §1 · p. 1
2 Semi-simplicial types up to triangles
- At level 2, a semi-simplicial type has points, edges, and triangles filling boundaries formed by three points and three edges.Source: §2 · p. 2
- The SST problem is to define data up to a variable level n uniformly; writing each numeral separately is possible, but no uniform construction is known in book HoTT.Source: §2 · p. 2
- Each Xk is a family over a telescope whose entries are earlier families applied to selections of earlier entries.For example, an edge selects its two endpoints from the points.Source: §2 · p. 2
- Selections must compose compatibly: a triangle boundary uses edges, whose own boundaries select points, making level 2 the first non-trivial composition case.Source: §2 · p. 2
3 A type theory with only weakenings and thinnings
The paper encodes semi-simplicial data in a small type theory with contexts, telescopes, variables, and thinnings. Weakening moves syntax between contexts, while thinnings select entries within a telescope and compose compatibly.
3 A type theory with only weakenings and thinnings
- The syntax has five sorts, including contexts, telescopes, variables, and thinnings, to represent sequences of type families and their selections.Source: §3 · p. 2
- Weakening moves from a longer context to a shorter one by one step, while a thinning drops entries from a longer telescope to select a shorter one.Source: §3 · p. 2
- The constructors extend contexts and telescopes, with variables referring to families and thinnings acting as projections.Source: §3 · pp. 2–3
- Weakening is defined recursively on syntax, pushing through types, variables, and thinnings; it renames family references without changing telescope or thinning shape.Source: §3 · p. 3
- In the intended interpretation, a context is a nested Σ-type of families, and extending a telescope pairs an entry with its dependent selection.Source: §3 · p. 3
- The triangle example encodes its points, then edges as thinnings selecting endpoints, and builds the triangle boundary by composing those selections.Keeping the final point requires its stored selection to equal the composite selection.Source: §3 · p. 3
4 The syntax: induction-recursion
The syntax is defined by induction-recursion so it remains untruncated and can be interpreted into the universe. Composition indexed by computed composites creates propositional transport problems; storing equations instead makes the syntax face a UIP coherence problem.
4 The syntax: induction-recursion
- The syntax must remain untruncated because quotient inductive-inductive types eliminate only into sets, whereas the intended interpretation targets the universe.The syntax's set property is intended as a theorem, not an axiom.Source: §4 · p. 4
- Composition and weakening are defined simultaneously with syntax because constructors for thinnings and variables have indices involving their recursively defined functions.Source: §4 · p. 4
- Agda accepts these induction-recursion definitions, but their semantics is not well understood and no known account covers recursive functions or their proofs in constructor indices.The authors use the feature while noting that the obstruction remains.Source: §4 · p. 4
- Indexing t-k by the composite makes composition ill-typed when associativity, identity, or weakening equations hold only propositionally, requiring transports that block computation.Source: §4 · p. 4
- Fording instead stores an equality relating the chosen index to the composite, allowing composition to build that equation as data.Closed examples compute with stored equations all reflexive.Source: §4 · pp. 4–5
- Proving congruence for t-k then requires equal proofs of the same equation, which amounts to UIP for Thin in this construction.Source: §4 · p. 5
5 Removing UIP: codes for equality
The authors use encode-decode codes for equality to prove uniqueness of stored proofs without K. This establishes that the untruncated syntax is a set, including its sorts.
5 Removing UIP: codes for equality
- Encode-decode codes for equality are defined recursively for thinnings, with reflexive codes, proposition-valued codes, and soundness decoding codes into equations.Source: §5 · p. 5
- The codes are propositions by induction, without K, Hedberg, or a Prop axiom.Source: §5 · p. 5
- Splitting the kept variable into related variables avoids repeated indices, so pattern matching works without K.Source: §5 · p. 5
- The equality codes establish that the total space of variables is a set, and the same encode-decode method proves the syntax sorts are sets.Source: §5 · p. 5
6 Semi-simplicial types in the syntax
The construction defines the context, k-skeleton, face maps, and their functoriality together by structural recursion on k. Because each new level uses the previous one weakened once, it yields SST n uniformly without K.
6 Semi-simplicial types in the syntax
- Structural recursion on k simultaneously defines the context ctx k, the k-skeleton SK k n, its face maps, and their functoriality.The face maps are indexed by order-preserving embeddings, with composition matching composition of embeddings.Source: §6 · pp. 5–6
- Level k +1 uses level k weakened once, so the types agree definitionally and the construction yields SST n uniformly without K.The resulting construction is in SSTk.agda.Source: §6 · p. 6
7 The naive interpretation, and the obstruction
The syntax is interpreted by recursion into the universe, where contexts become nested Σ-types and extensions become Σ-types of a family and its variable family. The interpretation does not give a semantic encoding of SST in HoTT: composing transports along propositional equations requires UIP for arbitrary semantic types.
7 The naive interpretation, and the obstruction
- The interpretation maps contexts to nested Σ-types and extends a context by a Σ-type pairing a family element with its variable-family value.The goal is for ⟦SST n⟧C to be the type of semi-simplicial types up to level n.Source: §7 · p. 6
- Interpreting a kept entry transports its value along the semantic image of a stored equation, which is proved propositionally rather than definitionally.The equation relates the interpretation of δ' to that of δ after σ.Source: §7 · p. 6
- Composing keeps produces two transports that must agree, and for arbitrary semantic types this requires UIP.The required paths live in arbitrary semantic types; weakening has the related issue that unwk-nat holds propositionally.Source: §7 · pp. 6–7
- The obstruction is not that semantic equations must hold definitionally: propositional equations suffice if their coherence is established.The Agda interpretation uses K only through pair-irr, proved with K; the K-based interpretation is essentially the known 2LTT construction, whose open problem is removing the outer level.Source: §7 · pp. 6–7
8 An alternative: composition as a constructor
Making weakening and composition constructors of a HIIT removes the semantic transport problem in the standard model, but moves the coherence burden into the syntax. Overlapping associativity and computation paths generate critical pairs requiring higher-dimensional constructors, and the proposed route to a set-valued syntax remains uncompleted.
8 An alternative: composition as a constructor
- Making weakening and composition constructors and their recursive equations path constructors removes the semantic problem in the standard model, where composition is function composition and the paths interpret as refl.Source: §8 · p. 7
- The keep rule must be stated over associativity, whose overlap with computation rules creates critical pairs that require further higher-dimensional constructors.For example, the two paths for (ρ ∘ δ) ∘tε form an unfilled loop; resolving it would require a pentagon and further coherence.Source: §8 · p. 7
- The hoped-for equivalence from the HIIT to the inductive-recursive syntax was not carried out, and a sketch indicates it fails as stated under univalence.A model with an extra circle component in Thin sends the critical-pair loop to a non-reflexive loop.Source: §8 · p. 7
9 Fording the HIIT
Fording the HIIT replaces computed indices involving composition or weakening with stored paths and conditional rules, avoiding associativity as a named constructor. The resulting syntax is proved to be a set without K or postulates, but its naive semantics again requires UIP; composition coherence must still be supplied somewhere.
9 Fording the HIIT
- Fording replaces indices involving composition or weakening with stored paths and states the corresponding rules for every path, avoiding the associativity constructor.Conditional rules identify keeps despite differing stored paths; wkext is essential for arbitrary loops because the fixed-refl version leaves a cube boundary unfillable.Source: §9 · pp. 7–8
- The syntax is proved to be a set without K or postulates, by retracting it onto set-valued normal forms.The normal forms are the inductive-recursive syntax with codes; the proof uses maps nf and quote with quote (nf t) ≡ t.Source: §9 · p. 8
- The conditional rules make stored paths comparable in a set, so no coherence of the HIIT itself is needed.The proof uses termination pragmas for recursions through path arguments and endpoints of path constructors.Source: §9 · p. 8
- The conditional rules amount to UIP for the syntax, but do not restrict semantics that interpret stored paths through canonical paths computed from normal forms.The rules are respected because they become equations between normal forms, which form a set.Source: §9 · pp. 8–9
- The naive interpretation of t-k∘t-k must respect every stored path, including arbitrary loops, forcing loop transport in the semantic telescope to act trivially.This requirement fails for X0 = S1 and X1 y z = (y ≡ z), where transport sends u to loop^-1 · u; relevant identity types must therefore be trivial for the rules to hold in this model.Source: §9 · p. 9
- The naive model therefore again needs UIP for semantic types; the model of sets satisfies the conditional rules but gives only semi-simplicial sets.Source: §9 · p. 9
- The trade-off is that coherence either returns as critical pairs without the conditions or requires UIP in the naive semantics with them.A normal-form interpretation avoids UIP in the syntax, but still requires proving semantic-path coherence.Source: §9 · p. 9
10 Single substitutions and coherent syntax
Single substitutions move the coherence problem from composition into exchange, but do not eliminate it: the syntax still needs higher coherences, while the naive semantic interpretation still needs UIP. The proposed normalisation route for dependent syntax remains open.
10 Single substitutions and coherent syntax
- Normalisation was proposed to prove the syntax a set by pushing substitutions down to variables, but the dependent case remains open.Stability under substitution requires type-equation hypotheses under arbitrarily many lifted weakenings; these are too strong to establish, and generalising them leads to circular dependency.Source: §10 · p. 10
- The conditional single-substitution rules resemble those of the Forded HIIT, while the report’s simply typed λ-calculus case works because its types do not depend on terms.In the dependent theory needed for semi-simplicial types, the required equations are conditional.Source: §10 · pp. 9–10
- Exchange of single steps already creates critical triples and higher coherence obligations, so composition’s coherence tower persists in the syntax.Three faces can be reordered in two ways, forming a hexagon that needs a 2-cell; four faces need 3-cells, and so on.Source: §10 · p. 10
- The naive interpretation of conditional variable equations must work for every semantic path, forcing transports along loops to fix the generic variable and bringing UIP back.Under univalence, non-trivial loops can include an automorphism swapping the points of a two-point telescope.Source: §10 · p. 10
- The single-substitution calculus moves the problem like the Forded HIIT: conditional equations make the syntax a set but rule out the naive universe model.Stating equations for canonical paths keeps the model but requires composition coherences in the form of exchange.Source: §10 · p. 10
11 The obstruction is always there
The attempted presentations place composition coherence either in the syntax or in the semantics, where the naive interpretation needs UIP. The obstruction remains for non-invertible maps, and whether displayed type theory resolves it is still open.
11 The obstruction is always there
- Each version places composition coherence in syntax as critical pairs or in semantics, where the naive interpretation needs UIP.The comparison table lists presentations with critical pairs or triples and records whether they form a set and whether the naive model needs UIP.Source: §11 · p. 11
- For non-invertible maps, the coherence of composition is never removed; the authors suggest a genuinely directed principle may be needed.They point to two-level, simplicial, and displayed type theory as examples of such principles.Source: §11 · p. 11
- It remains open whether displayed type theory has a universe satisfying relativity, which is needed for its décalage construction of semi-simplicial types in a homotopical setting.In the nominal model of internal parametricity, bridges in the universe are not the same as families.Source: §11 · p. 11
Use of AI tools
The note and accompanying Agda development were produced in collaboration with Claude, used through Claude Code.
Use of AI tools
- Claude drafted text and Agda code, ran Agda experiments, and searched the literature under the author’s direction.The author checked the content and is responsible for it.Source: Use of AI tools · p. 11
- The author checked the content and accepts responsibility for it.Source: Use of AI tools · p. 11
- Claims described as sketches have not been formally verified.Source: Use of AI tools · p. 11