3 Pull requests merged by 1 person

• Addition for lower and upper Dedekind reals

  #1342 merged Mar 23, 2025

• Cauchy sequences in metric spaces

  #1347 merged Mar 23, 2025

• Transposing addition and subtraction through rational inequalities

  #1339 merged Mar 22, 2025

8 Pull requests opened by 4 people

• Zigzag construction of identity types of pushouts

  #1370 opened Mar 18, 2025

• Sequences of positive rational numbers

  #1371 opened Mar 19, 2025

• Depostulate function extensionality

  #1373 opened Mar 20, 2025

• Commutative semiring of formal power series on commutative semirings

  #1374 opened Mar 21, 2025

• Continuity of functions between metric spaces

  #1375 opened Mar 22, 2025

• Equivalence between a type and the coproduct of a decidable subtype and its complement

  #1376 opened Mar 23, 2025

• Level-polymorphic commutative monoid of lower and upper Dedekind real numbers under addition

  #1377 opened Mar 23, 2025

• limits sequences metric spaces

  #1378 opened Mar 24, 2025

1 Issue opened by 1 person

• Reasoning syntax doesn't produce the expected result for relations which aren't strictly left unital

  #1369 opened Mar 17, 2025

9 Unresolved conversations

Sometimes conversations happen on old items that aren’t yet closed. Here is a list of all the Issues and Pull Requests with unresolved conversations.

• Minimum and maximum on the lower, upper, and usual Dedekind real numbers

  #1335 commented on Mar 24, 2025 • 31 new comments

• Sums and products over arbitrary finite types

  #1367 commented on Mar 24, 2025 • 25 new comments

• Logic, equality, and compactness

  #1264 commented on Mar 23, 2025 • 8 new comments

• Multiplication on closed intervals of rational numbers

  #1351 commented on Mar 23, 2025 • 7 new comments

• Best practices: encapsulation

  #1359 commented on Mar 19, 2025 • 0 new comments

• Real analysis: basic power series

  #1354 commented on Mar 19, 2025 • 0 new comments

• Addition on real numbers

  #1336 commented on Mar 23, 2025 • 0 new comments

• Flattening lemma for equifibered dependent span diagrams

  #1366 commented on Mar 21, 2025 • 0 new comments

• Streams

  #1368 commented on Mar 19, 2025 • 0 new comments