-- 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?