Post #2590500
2026-04-20 23:21 UTC
@constantine@types.pl Can we also postulate fracture by saying every (A : Set) is isomorphic to the Sigma type over a pair of (A^○ : Tyᵇ, A^● : Tyᶠ A^○)? This should make inductive types a little easier to deal with.
Replies (1)
-
@constantine@types.pl 2026-04-21 11:29
@trebor@types.pl Yeah that should be possible. You should also be able to implement the whole signature (opaquely) through a proposition with realignment, rather than postulating everything, and your suggestion would become a theorem.