Skip to content

Issues: sinhp/groupoid_model_in_lean4

Beta
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

15 Open 12 Closed
15 Open 12 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
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Universal property of sigma pullback square C-grpd Component: groupoid model D-unk Difficulty: unknown I-crit Impact: critical
#87 opened May 1, 2025 by Jlh18
@Jlh18
Use pair_naturality to prove naturality in the definition of smallUPair C-grpd Component: groupoid model D-low Difficulty: low I-high Impact: high
#86 opened May 1, 2025 by Jlh18
pairSection_naturality C-grpd Component: groupoid model D-unk Difficulty: unknown I-high Impact: high
#85 opened May 1, 2025 by Jlh18
Complete interpretation function C-model Component: abstract natural model C-syntax Component: typing rules, interpretation function O-group Other: issue group
#83 opened May 1, 2025 by Vtec234
sigma_naturality (formerly sigmaBeckChevalley) C-grpd Component: groupoid model D-low Difficulty: low I-crit Impact: critical
#69 opened Mar 12, 2025 by Jlh18
Groupoid model Pi types C-grpd Component: groupoid model D-unk Difficulty: unknown I-crit Impact: critical
#68 opened Mar 12, 2025 by Jlh18
1
Type theory rules D-low Difficulty: low I-low Impact: low O-doc Other: documentation, blueprint
#61 opened Feb 27, 2025 by Jlh18
Show that polynomial functors preserve pullbacks C-model Component: abstract natural model D-low Difficulty: low I-crit Impact: critical O-poly Other: improvements to Poly
#57 opened Feb 19, 2025 by Vtec234
Define composition of polynomial functors C-model Component: abstract natural model D-unk Difficulty: unknown I-crit Impact: critical O-poly Other: improvements to Poly
#56 opened Feb 19, 2025 by Vtec234
2
Define mapping from cartesian squares to cartesian natural transformations between polynomial functors C-model Component: abstract natural model D-high Difficulty: high I-crit Impact: critical O-poly Other: improvements to Poly
#55 opened Feb 19, 2025 by Vtec234
Automate proofs in Interpretation.lean more C-syntax Component: typing rules, interpretation function D-unk Difficulty: unknown I-high Impact: high
#50 opened Feb 12, 2025 by Vtec234
1
Establish naturality of type/term formers C-model Component: abstract natural model D-unk Difficulty: unknown I-crit Impact: critical
#49 opened Feb 11, 2025 by Vtec234
4 tasks
Define code and el C-model Component: abstract natural model D-unk Difficulty: unknown I-crit Impact: critical
#48 opened Feb 11, 2025 by Vtec234
@Vtec234
Identify better ways of dealing with intensionality D-high Difficulty: high I-high Impact: high
#47 opened Feb 11, 2025 by Vtec234
Write outline of project D-low Difficulty: low I-high Impact: high O-doc Other: documentation, blueprint
#44 opened Feb 11, 2025 by Vtec234
ProTip! Follow long discussions with comments:>50.