Closed jkingdon closed 3 weeks ago
This is a theorem somewhat similar to an exercise in the HoTT book but which also arose out of our discussion at https://github.com/metamath/set.mm/issues/3757#issuecomment-1890009714 .
This is a theorem somewhat similar to an exercise in the HoTT book but which also arose out of our discussion at https://github.com/metamath/set.mm/issues/3757#issuecomment-1890009714 .