Search results

the Yoneda lemma implies the dependent Yoneda lemma

Status: Open.

#152 In rzk-lang/sHoTT;

· emilyriehl opened on May 27, 2025

dependent Yoneda lemma implies the Yoneda lemma

Status: Open.

#151 In rzk-lang/sHoTT;

· emilyriehl opened on May 27, 2025

Prove associativity of composition using the dependent Yoneda lemma

Status: Open.

#150 In rzk-lang/sHoTT;

· emilyriehl opened on May 27, 2025

Orientation conventions for 3-simplices

Status: Open.

#146 In rzk-lang/sHoTT;

· thchatzidiamantis opened on Jul 24, 2024

Formalize strict adjoint sections, LARI families and its closure properties

Status: Open.

#133 In rzk-lang/sHoTT;

· TashiWalde opened on Oct 23, 2023

Formalize closure properties of left orthogonal shapes and right orthogonal maps

Status: Open.

#81 In rzk-lang/sHoTT;

· TashiWalde opened on Sep 29, 2023

functorial maps/equivalences

Status: Open.

#80 In rzk-lang/sHoTT;

· TashiWalde opened on Sep 29, 2023

logical equivalence between weakfunext and funext

Status: Open.

#73 In rzk-lang/sHoTT;

· emilyriehl opened on Sep 28, 2023

strengthen definition of limits/colimits

Status: Open.

#65 In rzk-lang/sHoTT;

· TashiWalde opened on Sep 27, 2023

prove various things are propositions

Status: Open.

#56 In rzk-lang/sHoTT;

· emilyriehl opened on Sep 26, 2023

Representable -> Hom

Status: Open.

#35 In rzk-lang/sHoTT;

· emilyriehl opened on Sep 21, 2023

Formalise adjunctions (Section 11 of RS17 paper)

RS17Related to Riehl and Shulman's 2017 paper «Type theory for synthetic ∞-categories»Related to Riehl and Shulman's 2017 paper «Type theory for synthetic ∞-categories»

Status: Open.

#26 In rzk-lang/sHoTT;

· fizruk opened on Sep 14, 2023