Over the weekend, I've taken a look at the Ambrus-Andras paper [1]. I immediately found myself in a jungle of syntaxes (external syntax, source sytax, target syntax, coherent problems) and syntactic translations. From the late Martin Hofmann, I have contracted an aversion to syntax. So in this email, let me cut down this jungle (and maybe lose some generality) by working with models and replacing syntactic translations by model constructions. Let me first recapitulate the constructions of the paper in my own language. In the second half, I will talk about higher categorical semantics. Many ideas here are Paolo's (using complete semi-Segal spaces in type theory, using this to give semantics to HITs). Metatheory ========== I will work in a 2-level type theory where the strict layer is extensional (has equality reflection). The intended model for this is presheaves over a cwf C that models HoTT, let's say the initial model of HoTT. The strict layer is interpreted as the extensional type theory internal language for presheaves over C. The fibrant types are interpreted as natural transformations to the presheaf Ty of types of C. Then strict equalities between elements of fibrant types are interpreted as definitional equalities in HoTT. In particular, one obtains specifications and semantics for HITs in HoTT. (On a side note, this would be the right setting to prove the equivalence of the two versions of the sphere recently discussed on the HoTT list; but note that Guillaume has pointed out that this could in principle also be done internally in HoTT.) I treat the strict fragment of the 2-level type theory as my metatheory. So my metatheory is extensional type theory, with universes of types written Set_i. In the metatheory, I am given constants - Ty_i : Set = Set_0 for the hierarchy of fibrant types, - Tm_i : Ty_i → Set for going from a fibrant type to its strict type of elements, and all the other operations of the fibrant fragment (including ty_i : Ty_{i+1} with el_i : Tm_i(ty_i) ≃ Ty_i). For convenience, I assume the fibrant fragment has η for Π and Σ. I will use Agda syntax for my metatheory. A type A is /fibrant/ if we have A' : Ty wirh A ≃ Tm(A'). Note that this is structure, not property. It is /strictly fibrant/ if the isomorphism is an equality. Signatures ========== The "theory of signatures" is defined as the initial /signature cwf/ Sig. A signature cwf Sig is a cwf with the operations in Figure 1 of your paper. I will only deal with small HITs, i.e. signatures for HITs that should end up in Ty = Ty_0. So for example, rules (2) are: - for Δ ∈ Sig, we have U : Ty_Sig(Δ), - for Δ ∈ Sig and A : Tm_Sig(Δ, U), we have El(A) : Ty_Sig(Δ), both stably under substitution in Δ. And the rules (6) are: - for A : Ty, Δ ∈ Sig, B : Tm(A) → Ty_Sig(Δ), we have Π-param(A, B) : Ty_Sig(Δ), - for A : Ty, Δ ∈ Sig, B : Tm(A) → Ty_Sig(Δ), f : Tm_Sig(Δ, Π-param(A, B)), a : Tm(A), we have Π-param-app(f, a) : Tm_Sig(Δ, B a), both stably under substitution in Δ. We can summarize this as saying that Sig is the initial cwf with: - a universe U (2), [I write Sig_U for the cwf induced by U, i.e. same contexts but types are terms of U] - Π-types with domain in U (3), - Sig_U has identity types (4), - I omit (5) (paths between types), - Sig (6) and Sig_U (7) have products of arity Tm : Ty → Set (6). Here, Π-types and products don't have introduction rules. [Why don't you make them proper Π-types and products?] As you know, one can avoid having to mention Δ (including laws for substitutional stability in Δ) by specifying the operations in presheaves over Sig. I will use extensional type theory as internal language for presheaves over Sig, writing '∷' for its typing relation. I have a global type Ty_Sig and a family Tm_Sig over Ty_Sig. The constants Ty and Tm embed as discrete presheaves, giving a global type Ty (should really be written 'const Ty', but I won't do this) and a family Tm over it. The rules read as follows, with (1) already taken care of by saying that Sig is a cwf. For rules (2), we have - U ∷ Ty_Sig, - El ∷ Tm_Sig(U) → Ty_Sig. For rules (3), given A ∷ Tm_Sig(U) B ∷ Tm_Sig(El(A)) → Ty_Sig we have - Π(A, B) ∷ Ty_Sig, - Π-app ∷ [f ∷ Tm_Sig(Π(A, B)), a ∷ Tm_Sig(El(A))] → Tm_Sig(B a). For rules (4), given A ∷ Tm_Sig(U) and a ∷ Tm_Sig(El(A)), we have - Id(a, x) ∷ Tm_Sig(U) for x ∷ Tm_Sig(El(A)), - refl ∷ Tm_Sig(El(Id(a, a))). Given further P ∷ [x ∷ Tm_Sig(El(A)), p ∷ Tm_Sig(El(Id(a, x)))] → Tm_Sig(U) d ∷ Tm_Sig(El(P(a, refl))), we have - J ∷ [x ∷ Tm_Sig(El(A)), p ∷ Tm_Sig(El(Id(a, x)))] → Tm_Sig(El(P(x, p))) such that J(a, refl) = d if we truly wanted to model identity types, or - J-β ∷ Id(J(a, refl), d) for propositional identity types as in the paper. I omit rules (5) (paths between types). For rules (6), given A ∷ Ty B ∷ Tm(A) → Ty_Sig we have - Π-param(A, B) ∷ Ty_Sig, - Π-param-app ∷ [f ∷ Tm_Sig(Π-param(A, B)), a ∷ Tm(A)] → Tm_Sig(B a). For rules (7), given A ∷ Ty B ∷ Tm(A) → U we have - Π-U-param(A, B) ∷ Tm_Sig(U), - Π-U-param-app ∷ [f ∷ Tm_Sig(El(Π-U-param(A, B))), a ∷ Tm(A)] → Tm_Sig(El(B a)). Internal higher categorical semantics ===================================== I see now (section 7 of [1]) that you actually started from the logical relation model for your definition of algebra homomorphism. So what I said yesterday about interpreting U as functional relations is already there. The reason I prefer the variant with functorial relations instead of functions is that it generalizes easier to higher dimensions. Of course, both are equivalent in the sense of the fibrant fragment. But I can see that the variant in the paper gets you closer to the desired rules for HIT elimination (although you don't model definitional β-rules; why?). I don't think it is possible to directly define identity morphisms by recursing over Sig. But there is also no expectation that this should be possible. Instead, something like the following might work. For internal higher categorical semantics, we wish to associate to each signature a complete Segal type of its algebras. Instead of separately building the fibrant type of algebras, the fibrant type of homomorphisms, and so on, each by elimination on signatures, it is better to put all of them together into one "infinitary record", which we can express using the strict layer, i.e. our extensional metalanguage, as a semisimplicial Reedy fibrant type, and construct this record by recursing over signatures. Conceptually speaking, this means we should build a signature cwf C out of complete Segal types. The signature cwf C is defined as follows (see the next subsection for details): - The underlying category is marked semisimplicial types. - A type is a type of the cwf of marked semisimplicial types that in addition is Reedy fibrant, inner fibrant, and complete. This means that its extension is a relatively complete inner fibration, meaning a Reedy fibration that has: * propositional fibrant type of markings, * contractible inner horn and special outer horn filling, * relative 2-out-of-3 and 2-out-of-6 for markings. - U is sent to the universe of left fibrations. Left fibrations are inner fibrations that in addition: * have contractible fibrant type of markings, * have contractible filling for {0} → Δ^1. [Note that a more local version of these conditions is used to define U.] Crucially, U is a complete Segal type. - The Π-type with domain a left fibration preserves relatively complete inner fibrations. - Left fibrations support identity types. - Infinitary products of types of C and elements of U work levelwise. By initiality of Sig, we then obtain a morphism of signature cwfs Sig → C which gives the higher categorical semantics (internal with respect to the fibrant fragment). Using contextuality of Sig (contexts are canonically isomorphic to telescopes of types), every signature is interpreted as a relatively complete inner fibration over 1, i.e. a complete Segal type. In a complete Segal type, we can then construct identity morphisms as usual by filling of 1- and 2-dimensional special outer horns. For the details, let's recall some basics about Reedy fibrant semisimplicial types. Reedy fibrant semisimplicial types ---------------------------------- Let Δ_+ denote the semisimplex category. A /semisimplicial type/ X is a presheaf over Δ_+, i.e. a functor X : Δ_+^op → Set. Presheaves over Δ_+ form a cwf SSet (semisimplicial, not simplicial) that models extensional type theory. A context Γ is a semisimplicial type and a type over Γ is a presheaf over the category of elements ∫ Γ. Note that there is an equivalence natural in X between: - maps in Presheaf(Δ_+) with target X, - the category with objects Ty_SSet(X) and maps given by maps between context extensions over X. We will frequently pass via the equivalence. For maps i : A → B and f : Y → X of semisimplicial types, we have the /Leibniz hom/ (hom)(i : A → B, f : Y → X) : hom(B, Y) --> hom(A, Y) ×_{hom(A, X)} hom(B, X). Its fibers represent the type of solutions to lifting problems from i : A → B against f : Y → X. If we start with Y : Ty_SSet(X) instead, this gives us (using the internal language of SSet) (hom)(A → B, Y) : (f : hom(B, X)) × (g : Tm_SSet(A, Y f i)) → Set (hom)(A → B, Y)(f, g) = (g' : Tm_SSet(B, Y f)) × (g' i = g). If we also represent A ∈ Ty_SSet(B), this writes as (hom)(A, Y) : (f : hom(B, X)) × Tm_SSet(B, (a : A) → Y f) (hom)(A, Y)(f, g) = (g' : Tm_SSet(B, Y f)) × (lam (g' p) = g). Important maps in semisimplicial types are the boundary inclusions I : ℕ → Presheaf(Δ_+)^→ I(n) : ∂Δ^n → Δ^n and the /horn inclusions/ J : (n : ℕ_{>0}) × (k : {0, …, n}) → Presheaf(Δ_+)^→ J(n, k) : Λ^n_k → Δ^n. A horn inclusion J(n, k) is /inner/ if 0 < k < n. Otherwise, it is /outer/, either /outer left/ (k = 0) or /outer right/ (k = n). A horn is /left/ if it is inner or outer left. It is /right/ if it is inner or outer right. We write J_inner, J_left, J_{outer left}, etc. for the corresponding restrictions of J. Outer horns have a /critical edge/ (that points in the wrong direction if one wishes to compose to fill the horn), the edge from 0 to 1 for outer left horns and the edge from n-1 to n for outer right horns. We say Y : Ty_SSet(X) is /(strictly) Reedy fibrant/ if for each [n] ∈ Δ₊, the family (hom)(I(n), Y) is (strictly) fibrant. In particular, a semisimplicial type X is Reedy fibrant if for each [n] ∈ Δ₊ the map X_n → M_n X to the matching object M_n X = hom(∂Δ^n, X) has fibers that are fibrant. Note that (strict) Reedy fibrancy is structure, not property. A /Reedy fibration/ Y → X is a map is Reedy fibrant seen as an element of Ty_SSet(X). Equivalenty, the Leibniz homs (hom)(I(n), Y → X) have fibers that are fibrant. Maps between Reedy fibrant semisimplicial types are just natural transformations. Note that such a map u : X → Y gives rise to maps between fibrant families on each level: for for each [n] ∈ Δ_+ there is uniquely determined u'_n : (x : M_n X) → Tm (X'_n x → Y'_n (M_n(u) x)) such that under the above equalities for X and Y, u_n corresponds to λ(x, t). (M_n(u) x, app(u'_n x, t)). Given a family K : M → Presheaf(Δ_+)^→ of maps of semisimplicial types, we have a derived family Cell(K) : M → Presheaf(Δ_+)^→ of /finite cell complexes/ of maps in K. These are finite compositions of pushouts of maps in K. For example, a map in Cell(I) consists of a levelwise decidable monomorphism between semisimplicial types that misses finitely many elements together with an extension to a total order of the partial order of these missed elements given by the face relation. Given i : A → B in Cell(I) and Y : Ty_SSet(X) Reedy fibrant, then (hom)(i : A → B, Y) is a fibrant family, the /family of fillers/ to lifting problems of i against Y. We say that it is contractible if each element of the family is contractible. In that case, we say that Y is /orthogonal/ to i and write i ⊥ Y. Given a family K : M → Presheaf(Δ_+)^→ contained in Cell(I), this extensions via universal quantification to K ⊥ Y. Given Reedy fibrant Y : Ty_SSet(X), we say that Y is - /Kan fibrant/ if J ⊥ Y, - /inner fibrant/ if J_inner ⊥ Y, - /left fibrant/ if J_left ⊥ Y, - /right fibrant/ if J_right ⊥ Y. We won't use these notions very much: they are ill-behaved in that they don't model identities correctly. Instead, we will switch to marked semisimplicial types soon. Let Y : Ty_SSet(X) be inner fibrant. An edge y : Y_1 over x is said to be /invertible/ if all lifting problems of two-dimensional outer horns against Y in which y is the critical edge have contractible types of fillers. This defines a fibrant h-proposition on edges in Y. For technical reasons, I like to work with so-called /marked semisimplicial types/. Those are presheaves over a modification Δ_{+,m} of Δ_+ that has an additional object [1]_m of marked edges that sits after [1] (there is a unique map [1] → [1]_m). Given such a presheaf X, its value at [1]_m is called its /markings/. This gives a cwf SSet_m of marked semisimplicial types modelling extensional type theory. There is a marked variation I_m of I that additionally has a map for Δ^1_m → Δ^1 (where Δ^1_m is Yoneda of [1]_m). This defines a notion of Reedy fibrancy in SSet_m. Given a semisimplicial type A and a subtype W of its edges, then (A, W) denotes the evident marked semisimplicial type with marked edges a subtype of edges. We have families of maps for talking about closure conditions on markings: - W_{2-out-of-3} is the family of maps (Δ^2, A) → (Δ^2, {01, 02, 12}) where A is any 2-element subset of {01, 02, 12}. - W_{2-out-of-6} is the singleton family of the map (T, {02, 13}) → (T, {01, 02, 03, 12, 13, 23}) where T = Δ^{0,1,2} +_{Δ^{1,2}} Δ^{1,2,3}. We define marked variations of the J families. - J_m is just J, - J_{m,inner} is the version of J that has all critical edges marked. So note that the shape of the horn in J_{m,inner} can be outer, but this is compensated by markings, We also add W_{2-out-of-3} to J_{m,inner}. - J_{m,left} is the sum of J_{m,inner} and J_left, - J_{m,right} is the sum of J_{m,inner} and J_right. Given Reedy fibrant Y : Ty_{SSet,m}(X), we say that Y is - /Kan fibrant/ if J_m ⊥ Y, - /inner fibrant/ if J_{m,inner} ⊥ Y, - /left fibrant/ if J_{m,left} ⊥ Y, - /right fibrant/ if J_{m,right} ⊥ Y and the fibrant family of markings of Y is propositional. Note that if Y is left or right fibrant, then its fibrant family of markings is contractible. Thus, a left or right fibrant Y carries no essential information in its markings. Inner fibrant Y : Ty_{SSet,m}(X) is called ‌/complete/ if W_{2-out-of-6} ⊥ Y. All these notions are defined by lifting properties, hence they are stictly stable under substitution in X. An inner fibrant semisimplicial type is called a /Segal type/. If it is complete, it is called a /complete Segal type/. Note that in a Segal type, every marked edge is invertible. It is /complete/ exactly if every invertible edge is marked. Thus, the markings in a complete Segal type are determined uniquely up to equivalence in the fibrant layer as the invertible edges. But it is technically convenient to keep them around so that it is easier to speak about allowable lifting problems. This also makes it easier to work with relative notions (fibrations rather than fibrant objects). Universe of left fibrations --------------------------- We internalize Shulman's construction of Reedy diagram models. Let's write Ty_{SSet,rf} for the restriction (recall this is actually structure) for Ty_SSet to strictly Reedy fibrant object. Then Ty_{SSet,rf} is represented by a semisimplicial type Ty_rf, classifying strictly Reedy fibrant types in SSet. That is, naturally in X : SSet, maps X → Ty_rf are in bijection with Y : Ty_{SSet,rf}(X). The important point is that Ty_Reedy, when restricted to small fibrant types, is itself Reedy fibrant. That is, naturally in X : SSet, there is ty_rf : Ty_{SSet,rf}(X) such that the elements of ty_rf are in bijection with Reedy ty-fibrant types over X in SSet, where ty : Ty is a universe in the fibrant fragment. This extends to a universe ty_Reedy for Reedy ty-fibrant types in marked semisimplicial types SSet_m. We modify it so that it classifies left fibrations. Naturally in X : SSet_m, we define ty_left : Ty_{SSet_m,rf}(X) el_left : Ty_{SSet_m,rf}(X.ty_left) as follows, leaving arguments from X and applications of el : Tm ty → Ty implicit: ty_left_0 = ty ty_left_1(T_0, T_1) = (T_01 : T_0 × T_1 → ty) × [(t_0 : T_0) → isContr (t_1 : T_1) × T_01(t_0, t_1)] ty_left_1m(T_0, T_1, T_01) = (t_1 : T_1) → isContr (t_0 : T_0) × T_01(t_0, t_1) ty_left_2(…) = (T_012 : … → ty) × … ty_left_n(…) = (T_{0…n} : … → ty) × and el_left_0(T_0) = T_0 el_left_1(T_0, T_1, T_01, t_0, t_1) = T_01(t_0, t_1) el_left_1m(…) = 1 el_left_2(…) = T_012(…) …. One easily check that el_left is indeed left fibrant. This does not strictly classify left fibrations as we have defined them, but this is not important: we can change our definition so that it matches this universe strictly (note that both notions are equivalent in a suitable sense, in particular equal in the fibrant layer in the presence of Reedy ω-limits). Importantly, ty_left is a complete Segal type. (this uses univalence). In fact, just looking at the situation over X = 1, the semisimplicial type ty_left is a Reedy fibrant replacement of the nerve N ty of ty seen as a category (with objects Tm ty and morphisms from X to Y given by Tm (el X → el Y)). Because N ty : Δ_+^op → Set is the nerve of a category, it preserves pullbacks in its domain that are formed by taking the pushout of 0 : [0] → [a] and b : [0] → [b] in Δ_+. In fact, the image of this square under N ty has fibrations has legs, hence is a homotopy pullback. It follows that also its Reedy fibrant replacement ty_left : Δ_+^op → Set sends these squares to homotopy pullback. This shows that ty_left is inner fibrant. The invertible edges in ty_left are those maps el X → el Y that are equivalences. So completeness of ty_left is just univalence. One also uses univalence to see that (ty_left)_0 ≃ ty, (ty_left)_1(X, Y) ≃ el(X) → el(Y). Π-types with domain in ty_left ------------------------------ We justify that the Π-type P = Π(Y, Z) of a left fibrant Y ∈ Ty_{SSet_m}(X) and a complete inner fibrant Z ∈ Ty_{SSet_m}(X.Y) is again complete inner fibrant. From the universal property of dependent products in SSet_m, we compute - P_0(x) = (y : Y_0(x)) → Z_0(y), - P_1(x, f_0, f_1) = (y_0 : Y_0(x|0)) (y_1 : Y_0(x|1)) (y_01 : Y_1(x|01, y_0, y_1)) → Z_1(x, y, f_0 y|0, f_1 y|1), - P_{1m}(x, f_0, f_1, f_01) = (y_0 : Y_0(x|0)) (y_1 : Y_0(x|1)) (y_01 : Y_1(x|01, y_0, y_1)) → Z_1m(x, y, f_0 y|0, f_1 y|1, f_01 y|01), - P_2(x, f_0, f_1, f_2, f_01, f_02, f_12) = (y_0 : Y_0(x|0)) (y_1 : Y_0(x|1)) (y_2 : Y_0(x|2)) (y_01 : Y_1(x|01, y_0, y_1)) (y_02 : Y_1(x|02, y_0, y_2)) (y_12 : Y_1(x|12, y_1, y_2)) → Z_2(x, y, f_0 y|0, f_1 y|1, f_2 y|2, f_01 y|01, f_02 y|02, f_12 y|12) and so on. Here …|c for c : [k] → [n] denotes the restriction of a family of elements along Δ_{+,m}/[n] → Δ_{+,m}/[k]. Note that for c : [0] → [n], we have …|c = …_c. In general, we have P_n(x, f) = (y : Y_n(x)) → Z_n(x, (f_i y_i)_{i ∈ ∂Δ^n}) where an occurrence of Y_n with omitted y parameters denotes the corresponding total space. Let j : Λ^n_k → Δ^n be an inner horn. We check that j ⊥ P. We have (hom)(j, P) : (x : hom(Δ^n, X)) × (f : Tm_SSet(Λ^n_k, P x j)) → Set (hom)(j, P)(x, f) = (f' : Tm_SSet(Δ^n, P x)) × (f' j = f) = (f_{[n]-k} : P_{n-1}(x||Δ^{n-1}, f|∂Δ^{n-1})) × (f_[n] : P_n(x, f, u)) = (f_{[n]-k} : (y : Y_{n-1}(x|…)) → Z_{n-1}(x|…, (f_i y_i)_{i ∈ ∂Δ^{[n]-k}})) × (f_[n] : (y : Y_n(x)) → Z_n(x, (f_i y_i)_{i ∈ ∂Δ^n})) = (y : Y_{n-1}(x|…)) → [ (f_{[n]-k} : Z_{n-1}(x|…, (f_i y_i)_{i ∈ ∂Δ^{[n]-k}})) × → Z_n(x, (f_i y_i)_{i ∈ ∂Δ^n}) ]. It will suffice to check that the expression [ … ] is contractible. This is a consequence of j ⊥ Z as soon as we verify that is contractible. This is an instance of Δ^{[n]-k} → Δ^n ⊥ Y. This follows from closure properties of orthogonality from {0} → Δ^{[n]-k} ⊥ Y and {0} → Δ^n ⊥ Y. We have {0} → Δ^m ⊥ Y for all m since Y is left fibrant (the map {0} → Δ^m is in Cell(J_{left outer}). A similar argument applies when j : Λ^n_k → Δ^n is an outer horn, but with critical edge marked. Let for example be k = 0 and the edge from 0 to 1 marked. Then the check comes down to Δ^{1,…,n} → (Δ^n, 01) ⊥ j. This follows from {0} → Δ^m ⊥ Y and {1} → (Δ^1, {01]) by considering the maps {0} → (Δ^1, {01]) ← {1} → Δ^{1,…,n}. Let's check W_{2-out-of-3} ⊥ P. We are given x : X_2 and f_j : P(x|j, f|∂Δ^m) for j : [m] → [2]. We are also given witnesses that x_01, x_02, x_12 are marked. Two of f_01, f_02, f_12 are marked and we have to show that the third is marked. The domains of the exponentials of the types of f_01, f_02, f_12 are equivalent to Y_2(x) via the canonical projection. For f_ij, this amounts to (Δ^{i,j}, {ij}) → (Δ^2, {01, 02, 02}) ⊥ Y, which holds since Y is inner fibrant. Given y : Y_2(x), we have a triangle f_012 y in Z with sides f_01 y|01, f_02 y|02, f_12 y|12. Since W_{2-out-of-3} ⊥ Z, these are marked if two of them are. Let's check W_{2-out-of-6} ⊥ P. Recall T = Δ^{0,1,2} +_{Δ^{1,2}} Δ^{1,2,3}. Given x : T → X with all edges marked and f_j : P(x|j, f|∂Δ^m) for j ∈ (T, {02}, {13}), we have to show that f_01, f_12, f_23, f_03 are marked. Using W_{2-out-of-3} ⊥ P, it suffices to show that f_01 is marked. Using that Δ^{0,1} → T ⊥ Y since Y is left fibrant, this reduces to W_{2-out-of-6} ⊥ Z as in the previous case. Identity types in ty_left ------------------------- Identity types in Reedy fibrant marked semisimplicial types are constructed using Reedy fibrant replacment of the diagonal morphism. This is an internalization of the construction given by Shulman. It remains to check that left fibrant Y : Ty_{SSet_m,rf}(X) has identity type Id_Y : Ty_{SSet_m,rf}(X.Y.Y) that is again left fibrant. This follows from cancellation properties of left fibrations: - Y : Ty_{SSet_m,rf}(X.Y) is left fibrant, - Σ(Y, Id_Y) : Ty_{SSet_m,rf}(X.Y) is contractible, hence left fibrant, hence Id_Y is also left fibrant. (Generally, given Reedy fibrations Y → X and Z → Y, if Y → X and Z → Y are left fibrations, then so is Z → Y). [1] https://arxiv.org/abs/1902.00297v3