search

UniMath / agda-unimath

The agda-unimath library
https://unimath.github.io/agda-unimath/
MIT License
222 stars 71 forks source link

Cleanup of finite types #1166

Closed fredrik-bakke closed 2 months ago

fredrik-bakke commented 2 months ago

So uhh, I felt a little inspired while reading Chris Grossack's blog post on Finiteness in Sheaf Topoi this evening, and decided to have a look around and see if I could add any small definitions or external links to the library. Then things kind of derailed when I stumbled upon our file on pi-finite types. Turns out this file entangled three concepts (pi-finite types, locally finite types, and types with finite connected components). So I, uh..., unentangled it! 😬 I hope I'm not stepping on your toes, @EgbertRijke, I really did not intend to.

EgbertRijke commented 2 months ago

Are you planning to do more refactoring in this PR? It is almost mergeable as it is

fredrik-bakke commented 2 months ago

Are you planning to do more refactoring in this PR? It is almost mergeable as it is

If anything I was planning to do less 😅

fredrik-bakke commented 2 months ago

I'll just wrap up the open conversations and then I'm done

fredrik-bakke commented 2 months ago

Alright, the last conversation is awaiting input from you, otherwise I am done.

EgbertRijke commented 2 months ago

Excellent, I'm merging this now