Skip to content

Issues: rzk-lang/sHoTT

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

20 Open 22 Closed
20 Open 22 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Orientation conventions for 3-simplices
#146 opened Jul 24, 2024 by thchatzidiamantis
Formalize strict adjoint sections, LARI families and its closure properties
#133 opened Oct 23, 2023 by TashiWalde
3 tasks
@TashiWalde
Formalize closure properties of left orthogonal shapes and right orthogonal maps
#81 opened Sep 29, 2023 by TashiWalde
15 of 18 tasks
@TashiWalde
1
functorial maps/equivalences
#80 opened Sep 29, 2023 by TashiWalde
logical equivalence between weakfunext and funext
#73 opened Sep 28, 2023 by emilyriehl
6
strengthen definition of limits/colimits
#65 opened Sep 27, 2023 by TashiWalde
1
prove various things are propositions
#56 opened Sep 26, 2023 by emilyriehl
3
Representable -> Hom
#35 opened Sep 21, 2023 by emilyriehl
Formalise adjunctions (Section 11 of RS17 paper) RS17 Related to Riehl and Shulman's 2017 paper «Type theory for synthetic ∞-categories»
#26 opened Sep 14, 2023 by fizruk
5 of 16 tasks
3
Formalise representable isomorphisms (Proposition 10.11 of RS17 paper) RS17 Related to Riehl and Shulman's 2017 paper «Type theory for synthetic ∞-categories»
#25 opened Sep 14, 2023 by fizruk
@cesarbm03
1
Formalise Rezk-completeness (Section 10.2 of RS17 paper) RS17 Related to Riehl and Shulman's 2017 paper «Type theory for synthetic ∞-categories»
#24 opened Sep 14, 2023 by fizruk
4 of 6 tasks
2
Improve the proof of naturality of Yoneda lemma in a : A enhancement New feature or request RS17 Related to Riehl and Shulman's 2017 paper «Type theory for synthetic ∞-categories»
#19 opened Sep 13, 2023 by fizruk
Formalise closure properties of covariance (Section 8.7 of RS17 paper) RS17 Related to Riehl and Shulman's 2017 paper «Type theory for synthetic ∞-categories»
#18 opened Sep 13, 2023 by fizruk
1 of 2 tasks
1
Formalise multivariable covariance (Section 8.5 of RS17 paper) RS17 Related to Riehl and Shulman's 2017 paper «Type theory for synthetic ∞-categories»
#16 opened Sep 13, 2023 by fizruk
3 tasks
@nimarasekh
1
Formalise discrete fibers (Section 8.4 of RS17 paper) good first issue Good for newcomers RS17 Related to Riehl and Shulman's 2017 paper «Type theory for synthetic ∞-categories»
#15 opened Sep 13, 2023 by fizruk
3 tasks
2
Formalise dependent composition (Remark 8.11 of RS17 paper) good first issue Good for newcomers RS17 Related to Riehl and Shulman's 2017 paper «Type theory for synthetic ∞-categories»
#13 opened Sep 13, 2023 by fizruk
1
Formalise anodyne maps (Section 5.5 of RS17) RS17 Related to Riehl and Shulman's 2017 paper «Type theory for synthetic ∞-categories»
#8 opened Sep 13, 2023 by fizruk
2 of 4 tasks
1
Formalise 3D horn filling for Segal types (Proposition 5.16 of RS17 paper) RS17 Related to Riehl and Shulman's 2017 paper «Type theory for synthetic ∞-categories»
#7 opened Sep 13, 2023 by fizruk
1
Formalise propositions about extension extensionality (Section 4.4 of RS17 paper) RS17 Related to Riehl and Shulman's 2017 paper «Type theory for synthetic ∞-categories»
#5 opened Sep 13, 2023 by fizruk
7 of 8 tasks
@jonalfcam
1
Formalise joins of simplices (Section 3.3 from RS17 paper) RS17 Related to Riehl and Shulman's 2017 paper «Type theory for synthetic ∞-categories»
#4 opened Sep 13, 2023 by fizruk
1
ProTip! Follow long discussions with comments:>50.