rzk-lang/sHoTT

co/limits are unique up to equality in a Rezk type about 2 hours ago

good first issue sHoTT

rzk-lang/sHoTT

67

Formalisations for simplicial HoTT and synthetic ∞-categories.

Markdown

Initial and final objects are closed under isomorphisms about 7 hours ago

good first issue sHoTT

rzk-lang/sHoTT

67

Formalisations for simplicial HoTT and synthetic ∞-categories.

Markdown

define the inductive type of truncation levels about 9 hours ago

good first issue HoTT

rzk-lang/sHoTT

67

Formalisations for simplicial HoTT and synthetic ∞-categories.

Markdown

prove various things are propositions 2 days ago

good first issue HoTT

rzk-lang/sHoTT

67

Formalisations for simplicial HoTT and synthetic ∞-categories.

Markdown

extension types preserve truncation levels 2 days ago

good first issue prerequisites needed sHoTT

rzk-lang/sHoTT

67

Formalisations for simplicial HoTT and synthetic ∞-categories.

Markdown

equivalent characterizations of sets. 2 days ago

good first issue HoTT

rzk-lang/sHoTT

67

Formalisations for simplicial HoTT and synthetic ∞-categories.

Markdown

limits are unique up to isomorphism 2 days ago

good first issue sHoTT

rzk-lang/sHoTT

67

Formalisations for simplicial HoTT and synthetic ∞-categories.

Markdown

Hedberg's theorem 2 days ago

good first issue HoTT

rzk-lang/sHoTT

67

Formalisations for simplicial HoTT and synthetic ∞-categories.

Markdown

Props are "proof-irrelevant" 2 days ago

good first issue HoTT

rzk-lang/sHoTT

67

Formalisations for simplicial HoTT and synthetic ∞-categories.

Markdown

Formalise dependent composition (Remark 8.11 of RS17 paper) 3 months ago

good first issue RS17

rzk-lang/sHoTT

67

Formalisations for simplicial HoTT and synthetic ∞-categories.

Markdown

Formalise pointwise natural isomorphisms (Proposition 10.3 of RS17 paper) 7 months ago

good first issue RS17

rzk-lang/sHoTT

67

Formalisations for simplicial HoTT and synthetic ∞-categories.

Markdown

Open Issues Need Help