All issues

Search results

Add License

documentationImprovements or additions to documentationImprovements or additions to documentation

Status: Open.

#192 In rzk-lang/sHoTT;

· fredrik-bakke opened on Aug 21, 2026

Hedberg's theorem

good first issueGood for newcomersGood for newcomers

HoTT

Status: Open.

#181 In rzk-lang/sHoTT;

· fredrik-bakke opened on Aug 19, 2026

co/limits are unique up to equality in a Rezk type

good first issueGood for newcomersGood for newcomers

sHoTT

Status: Open.

#179 In rzk-lang/sHoTT;

· emilyriehl opened on Aug 17, 2026

dualize 5.16 to treat the (3,2)-horn inclusion ([RS17, Proposition 5.16])

sHoTT

Status: Open.

#176 In rzk-lang/sHoTT;

· emilyriehl opened on Aug 14, 2026

Equivalent characterizations of sets

good first issueGood for newcomersGood for newcomers

HoTT

Status: Open.

#175 In rzk-lang/sHoTT;

· emilyriehl opened on Aug 14, 2026

extension types preserve truncation levels

good first issueGood for newcomersGood for newcomers

prerequisites needed

sHoTT

Status: Open.

#174 In rzk-lang/sHoTT;

· emilyriehl opened on Aug 14, 2026

define the inductive type of truncation levels

good first issueGood for newcomersGood for newcomers

HoTT

Status: Open.

#173 In rzk-lang/sHoTT;

· emilyriehl opened on Aug 14, 2026

Full embeddings are embeddings

sHoTT

Status: Open.

#156 In rzk-lang/sHoTT;

· TashiWalde opened on Nov 5, 2025

the Yoneda lemma implies the dependent Yoneda lemma

sHoTT

Status: Open.

#152 In rzk-lang/sHoTT;

· emilyriehl opened on May 27, 2025

dependent Yoneda lemma implies the Yoneda lemma

sHoTT

Status: Open.

#151 In rzk-lang/sHoTT;

· emilyriehl opened on May 27, 2025

Prove associativity of composition using the dependent Yoneda lemma

sHoTT

Status: Open.

#150 In rzk-lang/sHoTT;

· emilyriehl opened on May 27, 2025

Formalize strict adjoint sections, LARI families and its closure properties

sHoTT

Status: Open.

#133 In rzk-lang/sHoTT;

· TashiWalde opened on Oct 23, 2023