make A → B a subsingleton if A is empty #23

New issue

Closed

opened 2023-08-02 13:14:55 -04:00 by rhi · 0 comments

rhi commented

2023-08-02 13:14:55 -04:00

Owner

in the base case of a w type, you have a function with a type like 0.{} → (x:A) ⊲ B.

obviously it is something equivalent to λ(). there are no other options
agda (e.g.) needs a postulate like {f g : ⊥ → A} → f ≡ g
xtt can see it propositionally
being able to see it judgmentally would make writing base cases much less annoying though

in the base case of a w type, you have a function with a type like `0.{} → (x:A) ⊲ B`. - obviously it is something equivalent to `λ()`. there are no other options - agda (e.g.) needs a postulate like `{f g : ⊥ → A} → f ≡ g` - xtt can see it _propositionally_ - being able to see it _judgmentally_ would make writing base cases much less annoying though