In the latest HoTTEST seminar

https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html

Matthew Weaver made a reference to our work with Fabian Ruch on
constructive sheaf models. A link is

 https://arxiv.org/abs/1912.10407


 Here are some remarks (and an important correction) that may help in following
what we wrote and that will be incorporated in a future version:

 -the analogy with morphisms of tribes (Section 1) is misleading.
We should have stated it instead as an analogy with the notion of morphisms
of -fibration category- (involving fibrations, equivalences, terminal objects and
pullbacks along fibrations).  We owe this correction to Christian Sattler.

 -indeed what we use implicitly  in Section 1 is the notion of fibration category associated
to a type theory. This is described in particular in the work of Avigad-Kapulkin-Lumsdaine,
that we should have cited since it illuminates what is going on in the Appendix

 -a lex operation D (figure 1 in the Appendix) is in particular a pointed endofunctor \eta_X : X -> DX
and we isolate in Section 1 two conditions for it to generate a lex modality

 (1)  if \eta_X has a homotopy left inverse, it is an equivalence
 (2)  D preserves etale fibration

(a fibration is etale if the corresponding diagram with the \eta maps is a homotopy pullback)

 If MX, X -> MX is the homotopy initial D-algebra generated by X, then (1) implies that M defines a -modality-
(such that X is M-modal iff \eta_X is an equivalence)
and (1)+(2) imply that M is a -left exact modality- (the proof makes use of a universe)

 -Definition 1.2 provides two sufficient conditions that imply respectively (1) and (2).
We check in Section 4 that these conditions hold for the “intuitive” notion of descent data
which is described in the introduction (and that Matthew described in his talk). If correct, this
provides a constructive description of the model of sheaf of spaces over a 1-site

 -as mentioned by Matthew in his talk, the connections between this notion of descent data
and the cobar operation used by Mike Shulman in his recent work on strict univalent universes
need to be better understood

 Best regards,
 Thierry