English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

We present a way of constructing a Quillen model structure on a full subcategory of an elementary topos, starting with an interval object with connections and a certain dominance. The advantage of this method is that it does not require the underlying topos to be cocomplete. The resulting model category structure gives rise to a model of homotopy type theory with identity types, Σ- and Π-types, and functional extensionality. We apply the method to the effective topos with the interval object ∇2. In the resulting model structure we identify uniform inhabited objects as contractible objects, and show that discrete objects are fibrant. Moreover, we show that the unit of the discrete reflection is a homotopy equivalence and the homotopy category of fibrant assemblies is equivalent to the category of modest sets. We compare our work with the path object category construction on the effective topos by Jaap van Oosten.

A homotopy-theoretic model of function extensionality in the effective topos