Amélia Liao 🍊😈 on Nostr: nprofile1q…fw8t5 nprofile1q…4rrqe … it's not a bug that constructors for ...

nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyry2ysn5av9pr8m76kgpggcflz294t0pr9shd99kh8redys7ku0xkefw8t5 (nprofile…w8t5) nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzf5l64n2xk9azdrt6c96nwshexx45v4sduj7cyakmw005afuu05jm4rrqe (nprofile…rrqe) … it's not a bug that constructors for (non-higher) inductive types are disjoint and injective. in fact this is like agda's most sensible feature