-- Descent Data Operations and Constructive Sheaf Models of Type Theory -- ------------------------------------------------------------------- j.w.w. Fabian Ruch and Christian Sattler The details can be found in the arXiv paper Constructive Sheaf Models of Type Theory Here I will try to present the main ideas, without going too much in technical issues Last time, Steve made use of the model E ̂Σ E cubical set model and Σ groupoid of permutations E^Σ₂ where Σ₂ symmetric group on 2 elements An object in E^Σ₂ is a cubical set with a Σ₂ action For instance the equivariant square II₂ = I² with the swap operation No problem to present this model -since- cubical set models are described in a constructive and essentially algebraic way Compare this with the simplicial set model! There the model is built using classical logic not trivial at all to have a presheaf version of this model (cf. recent work by Mike Shulman), even for simplicial sets with a Σ₂ action We can replace Σ₂ or the groupoid Σ by an arbitrary base category C and consider -presheaf- models An object is now a family of cubical sets A(X) indexed by the objects of C with transition/restriction maps A(X) -> A(Y) for f : Y -> X We shall write u ↦ u|f this restriction map More or less notation of Dana Scott 1980 Relating the theories of the λ-calculus Natural questions: (1) if we have a presheaf model of univalence (such as cubical sets) we can build from it a Quillen Model Structure, which satisfies -Frobenius (and right properness) -Equivalence Extension Property -Fibration Extension Property (a.k.a. "Joyal's trick") We can do this for this presheaf model, e.g. E^Σ₂ Is it the case that an object which is pointwise contractible is contractible or that a pointwise equivalence is an equivalence? -- Answer: NO Example: let A be the groupoid with two isomorphic objects a and b that are swapped by Σ₂ Then A is pointwise contractible but is not contractible since there is no map 1 -> A in the E^Σ₂ model (strict speaking, cubical nerve of ...) A -> 1 is not an equivalence in E^Σ₂ (2) For presheaf 1-topos, we can build -sheaf- topos using the notion of Lawvere-Tierney topology, modal operation on the object of truth values can we do something similar for type theory? -- Answer: if we have a Grothendieck topology Cov on the base category C so that Cov(X) set of sieves over X Cov can be seen internally as a strict set in the presheaf model and then we are going to define a family of -lex modalities- D_S indexed by S : Cov -- The types that are D_S modal, for all S, will form a new model of type theory + univalence + HIT These two questions are connected. By (2), in particular, for the -trivial- topology and corresponding modal operation we get a model This model has the property that a map is an equivalence iff it is a pointwise equivalence By (1) this model may be different from the original presheaf model, in particular over Σ₂ Special case: trivial topology Cov = 1 Cov(X) = maximal sieve on X one special lex modality D for this lex modality a new model of type theory -> QMS injective model structure cobar operation Mike Shulman D(A) type for A type -- First part: result about Lex and Descent Data Operations purely type theory + univalence + HIT -- Second part: presheaf models, new models of type theory -- Third part/conclusion: potential applications Recall that to have a notion of sheaf of higher sets was the purpose of the first part of the 84 letter from Joyal to Grothendieck Use the QMS on simplifical set + Barr theorem also used by Grothendieck in his Tohoku 57 paper where he defines cohomology groups for sheaves via injective resolutions Sheaves over topological space X consider Xdisc and the surjective map Xdisc -> X to reduce questions about X-sheaves to questions about Xdisc-sheaves We now have a constructive version of "higher sheaves"; in particular a constructive way to define cohomology groups in sheaf models via Eilenberg-MacLane spaces Brauer group of a field? condensed sets? -- part I Lex and Descent Data Operations ------------------------------- The kind of operations on types E(X) we are going to analyse are direct generalisations of the exponential operation E(A) = A^R for a fixed type R : U0 What are the properties of such an operation? -Strict- endofunctor f : A -> B E(f) : E(A) -> E(B) E(f) u = f ∘ u we have E(id) = id and E(g ∘ f) = E(g) ∘ E(f) strict equalities -If A : U then E(A) : U for any universe U -E(Σ (x:A) B)?? distributivity law E(Σ A B) iso Σ E(A) E'(B) (Σ A B)^R Σ A^R ... where E'(B) u = Π (r:R) B(u r) for u : E(A) = A^R and the isomorphism is "definitional" or "strict" or "judgemental" -E is a pointed endofunctor η : A -> E(A) η a r = a These properties define (roughly) what is a -lex operation- Note that we can define η' a a' : E'(P)(η a) for P : A -> U and a' : P(a) definition η' a a' = E(π₂)(η (a,a')) η : Σ A P -> E(Σ A P) This definition mentions only Π, Σ, U no mention of Id type!! For the presheaf model what will be this operation? A is now a family of "spaces" A(X) with transition map E(A) new family u : E(A)(X) means u family u_f : A(Y) for f : Y -> X η : A -> E(A) a : A(X) η a : E(A)(X) (η a)(f) = a|f : A(Y) over a context Γ, if ρ in Γ(X) then u : E(A)ρ means u family u_f in Aρ|f if B family over A, B(X,a) for a in A(X) v : E'(B)(X,u) means v family v_f : B(Y,u_f) for f : Y -> X we then have E(Σ A B) ≃ Σ E(A) E'(B) strict isomorphism What happens if we also have Id type? Then E -automatically- preserves equivalences! Simply because if f, g are path equal then so are E(f) and E(g) This implies that E preserves all finite homotopy limits Definition: A is E-modal iff η_A : A -> E(A) is an equivalence ---------- -- Main Theorem of Part 1: ---------------------- Let E be a lex operation so we have E' and η for E to define a lex modality (property) it is enough to have -E(η_A) is an equivalence (property) -η_{EA} and E(η_A) : E(A) -> E²(A) are path equal (structure) These conditions are also necessary Furthermore, in this case we have that U_E = Σ U E_modal -is- E-modal The "canonical" example is E(A) = A^R where R is a -proposition- In this case, A is E-modal as soon as η_A has a left inverse The left inverse of U_E -> E(U_E) will be essentially given by E(U) -> U which is given by E'(id_U) : E(U) -> U we have E'(id_U)(η_U A) =_U A if A : U is E-modal by univalence -- Semantically, to build a lex operation it is enough to build -- a pointed endo-pseudomorphism on a cwf The cwf is given by a category of contexts Con We have E : Con -> Con -pointed- endofunctor η : Γ -> E(Γ) E pseudo-morphism we have E_t(A) type over E(Γ) for A type over Γ If A is type over Γ then E_t(A) is a type over E(Γ) and we can use η to pull back E_t(A) as a type E(A) over Γ We can define E'(B) type over Γ.E(A) if B type over Γ.A in a similar way -- check natural transformation If we have a -descent data- operation D we can define a -new- model of type theory A type in this new model is a type A -together with- a proof that A is D-modal We have universes since universe of modal types is modal -- In this model, we have inductive types and HIT For instance the new type of natural numbers is the HIT defined as the HIT with constructors zero : nat succ : nat -> nat patch : D(nat) -> nat linv : Π (n:nat) patch (η n) ≡ n the -constructor- linv expresses that the patch function is a left inverse of η : nat -> D(nat) Note that the fact that we have a D' operation on family of types allows us to write the elimination rule for this type If we have P(n), n : nat to prove Π (n:nat) P(n) we have to prove P(zero) P(succ n) from P(n) P(patch u) from D'(P)(u) for u : D(nat) P(linv n i) from P(n) with suitable boundary conditions we can write this with computation rules This is completely uniform in the data types (no problem for the W type) Similarly the suspension T of a type A will be defined by constructors north : T and south : T merid : A -> north ≡ south patch : D T -> T linv : Π (z : T) patch (η z) ≡ z In the models below, the fact that D is a -strict- functor is essential to ensure that these inductive definitions make sense Using that D is a strict functor we can write the computation rules for these types being abstract w.r.t. the actual definition of D -- Part 2 Examples of Descent Data Operations ----------------------------------- Two examples E(A) = A^R E(A)(X) = Π_{Y, f:Y->X} A(Y) Neither are descent data operations in general E(A) = A^R is a descent data operation if R is a proposition Since E is a pointed endofunctor we have a co-semisimplicial diagrem E(A) -> E²(A) -> E³(A) -> ... two maps E(A) -> E²(A) η_A and E(η_A) three maps E²(A) -> E³(A) η_EA and E(η_EA) and E²(η_A) ... We define D(A) to be the homotopy limit of this diagram We are going to present a special way to represent this limit so that D is a strict functor and we have -- Main Theorem 2 : D(A) defines a descent data operation -------------- I will describe this in both examples E(A) = A^R E(A)(X) = Π_{Y, f:Y->X} A(Y) For computing this limit, I introduce Pⁿ Pⁿ space of (i0,i1,...,in) such that i0 = 1 ∨ ... ∨ in = 1 subspace of I^{n+1} (cf. analogy with projective space) fat wedge Computation of D(A) for E(A) = A^R An element of D(A) is an infinite sequence u(i0,...,in) : E^{n+1}(A) u(1) : R -> A u(1)(r₀) : A for r₀ : R u(i₀,i₁)(r₀,r₁) : A for r₀ r₁ : R with u(1,0)(r₀,r₁) = u(1)(r₀) and u(0,1)(r₀,r₁) = u(1)(r₁) u(i₀,i₁,i₂)(r₀,r₁,r₂) : A for r₀ r₁ r₂ : R with u(i₀,i₁,0)(r₀,r₁) = u(i₀,i₁)(r₀,r₁) and u(0,i₁,i₂)(r₁,r₂) = u(i₁,i₂)(r₁,r₂) and u(i₀,0,i₂)(r₀,r₂) = u(i₀,i₂)(r₀,r₂) ... u(1,i)(r₀,r₁) provides a path between u(1)(r₀) and u(1,1)(r₀,r₁) u(i,1)(r₀,r₁) provides a path between u(1)(r₁) and u(1,1)(r₀,r₁) So u(1)(r) and u(1)(s) are both path equal to u(1,1)(r,s) in this sense u(1) : R -> A is weakly constant u(i,j,k)(r,s,t) provides then a coherence condition between the proofs that u(1)(r), u(1)(s), u(1)(t) are pairwise path equal and so on, with higher coherence conditions This is exactly (but in a cubical setting) a -coherently constant function- in the sense of Nicolai Krauss example of id : S1 -> S1 which is weakly constant not coherently constant u(i0,...,in) is like a choice sequence but extended in a -spatial- dimension instead of a -temporal- dimension This provides a rather canonical encoding of these coherence conditions where the only boundary we consider are i=0 and i=1 (never i=j) It is rather direct to check that the two conditions of Main Theorem of Part 1: for D to be a lex modality (property) if is enough to have -D(η_A) is an equivalence (property) -η_{DA} and D(η_A) : D(A) -> D²(A) are path equal (structure) are satisfied in this case and for this we really need the homotopy limit all coherence conditions!!! This allows for a short argument for Nicolai Krauss' result: a coherently constant function R -> A factors through || R || -> A Indeed, we have R -> isEquiv(η_A) and hence || R || -> isEquiv(η_A) In particular || R || -> D(A) -> A and so D(A) -> (|| R || -> A) D(A) is the space of coherently constant functions Similarly we build in a similar way D(A) for E(A)(X) = Π_{Y, f:Y->X}(Y) In this case, an element u : D(A)(X) is a family u(i0,i1,...,in)(f0,f1,...,fn) : A(X(n+1)) for f0 : X1 -> X, f1 : X2 -> X1, ..., fn : X(n+1) -> Xn and i0,...,in in Pⁿ satisfying conditions u(1,0)(f₀,f₁) = u(1)(f₀)|f₁ and u(0,1)(f₀,f₁) = u(1)(f₀f₁) both are path equal to u(1,1)(f₀,f₁) u(i₀,i₁,0)(f₀,f₁,f₂) = u(i₀,i₁)(f₀,f₁)|f₂ u(i₀,0,i₂)(f₀,f₁,f₂) = u(i₀,i₂)(f₀,f₁f₂) u(0,i₁,i₂)(f₀,f₁,f₂) = u(i₁,i₂)(f₀f₁,f₂) ... In particular u(1,...,1)(f0,...,fn) select and element in A(X(n+1)) u_id : A(X) f : Y -> X u_f : A(Y) u_id|f path equal u_f So u(1)(fg) and u(1)(f)|g are both path equal to u(1,1)(f,g) Any element a in A(X) defines an element η a in E(A)(X) by (η a)(i0,...,in)(f0,...,fn) = a|(f0...fn) In this case we have a -strict- equality (η a)(1)(fg) = a|(fg) = (η a)(1)(f)|g D(A) itself is a strict presheaf with the restriction operation u|f(i0,...,in)(f0,...,fn) = u(i0,...,un)(ff0,...,fn) We get a "semisimplicial" version of the cobar operation We can now prove (by direct checking; there is potentially a more abstract argument) the two conditions of Main Theorem of Part 1: for D to be a lex modality (property) if is enough to have -D(η_A) is an equivalence (property) -η_{DA} and D(η_A) : D(A) -> D²(A) are path equal (structure) -- This cobar operation is a lex modality We get in this way a new presheaf model of type theory Theorem: ------- (1) if A is pointwise contractible then D(A) is contractible (2) if σ : A -> B is pointwise an equivalence then D(σ) : D(A) -> D(B) is an equivalence (3) if σ : A -> B is pointwise an equivalence and A and B are D-modal then σ is an equivalence Why? A -> D(A) B -> D(B) Corollary: in this new model, an equivalence is exactly a pointwise equivalence --------- Particular case E^Σ₂ we get a new model The counter example a ≅ b provides an example of a non modal type In this new model the equivariant square II₂ considered by Steve -is- weakly contractible since it is pointwise weakly contractible II₂ -> 1 weak equivalence since it is X -> 1 weak equivalence what is a name for this property If we have a Grothendieck topology Cov(X) on the base category C We have internally a -family- of lex operation E_S, S : Cov Cov is a global presheaf Cov(X) = set of covering sieves over X How do I define a family A over Γ I should define a family of (cubical) sets Aρ for ρ in Γ(X) If A type over Γ and ρ in Γ(X) and S in Cov ρ = Cov(X) then E_S(A)ρ is the set of family u_f in Aρ f for f in S Γ |- A type Γ |- S : Cov --------------------- Γ |- E_S(A) type We define then a family of corresponding descent data operations D_S, S : Cov Question: what happens over the point? -- Part 3: applications and potential applications In the arXiv paper, we give an application: countable choice is not provable This is an example where the base category is a poset Another application is the work of M. Weaver and D. Licata on model of directed univalence hope to get a cubical notion of Segal spaces Potentially, all topos examples can be lifted to "higher topos" examples in this way with a computational interpretation E.g. Dana Scott stochastic λ-calculus I would like to mention some special examples that may be interesting to explore further Both are connected to étale topology While this notion might not be so easy yet to explore constructively, there are two special cases that seem reachable -over Boolean algebra -- condensed sets -over k algebra for k discrete field -- Brauer group k-algebra reduced 0-dimensional I will say a few word about the second example The topology is A k-algebra covered by A -> A/(e) and A -> A/(1-e) if e idempotent of A A -> A[X]/(P) if P in A[X] unitary and separable The intuition is that each A is a "finite approximation" of the separable closure of k We can decide if a polynomial is -separable-, but not if it is -irreducible- This motivates the first clause of the covering: we add a root of a separable polynomial and we split the corresponding -algebra- if, later on, during the course of a computation, we discover a factor of this polynomial (classically we can decide irreducibility and we consider only field extensions) "Lazy" computation D5 solution of the problem to compute with algebraic numbers The first example is similar the covering are B -> B/(e) and B -> B/(1-e) and B -> B' corresponding to a surjective open map of spaces i.e. we have ∃ : B' -> B giving a structure of monadic Boolean algebra The first example gives a model of the Fan Theorem (but for this we only need the first notion of covering) Over this 1-topos the set-valued functor A ↦ A as a set is a separable algebraic closure of k This functor is represented by the algebra k[X] In the 1-topos case, this has been used by Bassel Mannaa and myself to give a constructive reading of Abhyankar's proof of Newton-Puiseux Theorem (branches of an algebraic curve) This has been implemented in Haskell For type theory, we can start to study cohomology groups of objects in the model Gm presheaf on the category of k-algebras E.g. Gm(A) = set of invertible elements of A Gm is a sheaf for the topology described above Gm is represented by k[X,1/X] Gm is an abelian group in this model, we can look at corresponding Eilenberg-MacLane spaces H¹ : What are the Gm-torsors? Theorem (Hilbert's Theorem 90) all Gm torsors are trivial ------- H² : What are the Gm-gerbes? a Gm-gerbe is a connected groupoid X with a Gm-link i.e. a family of equalities Gm ≡ (x ≡ x) for x : X the type of all Gm-gerbes is K(Gm,2) S1 is a Z-gerbe set truncation of the type of Gm-gerbe we get H^2(Gm) = Br(k) Brauer group of k We expect that Gm gerbes should correspond to the elements of the Brauer group of k i.e. central simple algebra (in general not commutative) over k modulo the equivalence A ~ B iff M_p(A) ≃ M_q(B) for some p and q e.g. Br(R) = Z/2Z In order to define this it is essential to have a setting where -we have a representation of Eilenberg-MacLane spaces in type theory -we have a representation of sheaf models of type theory We should be able to at least state Merkuriev-Suslin or Milnor's conjecture in this setting Voevodsky conjecture: solved by Kapulkin and Sattler Normalisation for cubical type theory: use a presheaf model over cubical sets to be done do we need this refined presheaf model?