Discussions

• 1 You must be logged in to vote

  🙌

  A simple Ltac2 tactic to debug broken "refine" statements

  patrick-nicodemus started Mar 22, 2025 in Show and tell

  

  

  3
• 2 You must be logged in to vote

  💬

  Canonical structures

  patrick-nicodemus started Mar 18, 2025 in General

  

  

  

  

  3
• 1 You must be logged in to vote

  💡

  A variant of the WildCat Yoneda lemma

  jdchristensen started Aug 30, 2023 in Ideas · Closed

  

  

  7
• 1 You must be logged in to vote

  🙏

  Does Coq (especially HoTT Coq) has formalised pre-∞-categories and ∞-categories? If not - what can it take to do so?

  alexandre-emmanuel asked Oct 21, 2024 in Q&A · Unanswered

  

  

  1
• 1 You must be logged in to vote

  💬

  Merge queues

  Alizter started Sep 3, 2023 in General · Closed

  

  

  5
• 3 You must be logged in to vote

  💬

  Compiling library against multiple versions of Coq at the same time

  Alizter started Mar 8, 2023 in General

  

  

  0
• 1 You must be logged in to vote

  💬

  Should we drop proviola support?

  Alizter started Feb 26, 2023 in General · Closed

  

  

  

  

  2
• 1 You must be logged in to vote

  💬

  WildCat Equiv.compose_cate can't compose maps between different universes

  jdchristensen started Jan 27, 2023 in General · Closed

  

  

  

  

  16
• 1 You must be logged in to vote

  💡

  Should we wrap comments?

  Alizter started Feb 19, 2023 in Ideas

  

  

  

  

  2
• 1 You must be logged in to vote

  💡

  Should we use cumulative inductives by default?

  Alizter started Jun 25, 2021 in Ideas

  

  

  

  

  2
• 1 You must be logged in to vote

  💡

  Discussions page for repo

  discussion

  Alizter started Jun 18, 2021 in Ideas

  

  

  

  

  10
• 0 You must be logged in to vote

  📣

  Welcome to HoTT Discussions!

  Alizter announced Jun 19, 2021 in Announcements

  

  

  0