agda-unimath

agda-unimath copied to clipboard

Pulls logic additions from #1264.

fredrik-bakke

fredrik-bakke

- [X] Improve universe polymorphism of descent data for pushouts - [X] Define equifibered dependent span diagrams - [ ] ~State flattening lemma for equifibered dependent span diagrams~ - [...

fredrik-bakke

Since `finite-sequences` are there now, it might make sense, though I suppose `lists` currently only contains finite structures.

lowasser

Analysis: series

4

I'm getting back to this and trying to build a good definition for _series_. Wikipedia uses the term "series" to refer only to infinite sums, and I buy that. I...

lowasser

Syntax modules

14

I'm curious about opinions and input on this one @EgbertRijke @VojtechStep @lowasser. This is the kind of thing I had in mind when I mentioned syntax modules for wild categories...

fredrik-bakke

I thought it would be nice to add some abstract nonsense to the library. Since agda (and in particular, agda-unimath) is new to me, I would like to get some...

arnoudvanderleer

> My auto-completion messed up this link and I'm surprised it passed the link-check. I guess it's a bug caused by the ℚ character but maybe it's something you want...

fredrik-bakke

large premetric spaces

7

malarbol

Self-review guidelines for maintainers

1

Document a process for maintainers to self-review and merge pull requests when other maintainers are not available to review.

fredrik-bakke