search

UniMath / agda-unimath

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

Hereditary W-types #1112

Closed EgbertRijke closed 5 months ago

EgbertRijke commented 5 months ago

In this PR I generalized the equivalence constructed in #1110, to something that I called "hereditary W-types". This PR is independent of #1110.

EgbertRijke commented 5 months ago

If you're ok with it I'd prefer to do the characterizations of identity types another time. You're right that they are probably good to have around.

EgbertRijke commented 5 months ago

Also, thank you for the review!

fredrik-bakke commented 5 months ago

If you're ok with it I'd prefer to do the characterizations of identity types another time. You're right that they are probably good to have around.

Yep, totally fine