Families over telescopes

UniMath / agda-unimath

The agda-unimath library

https://unimath.github.io/agda-unimath/

MIT License

222 stars 71 forks source link

Closed fredrik-bakke closed 8 months ago

fredrik-bakke commented 8 months ago

Defines the type of families over a telescope. Also defines the translation map from small telescopes to telescopes.

fredrik-bakke commented 8 months ago

I don't know how you want to manage authorship for this one, but I'm happy to share

EgbertRijke commented 8 months ago

LGTM!

EgbertRijke commented 8 months ago

I don't know how you want to manage authorship for this one, but I'm happy to share

Oh, no worries about it.