#qtt — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #qtt, aggregated by home.social.
-
Ah, trying to make sure everything is erased in #Idris and I can't use the `Const : Type -> Type -> Type` functor from "base" because I need something that is `Type -> (0 _ : Type) -> Type`.
This feels like a _very_ niche problem. You'd basically have to be in #QTT or some other modal type theory where usage quantities are tracked.
I could change the test code to use a new "Const" with the right kind, but I wonder if this is a symptom where I need to change the quantities in my main code.
-
Ah, trying to make sure everything is erased in #Idris and I can't use the `Const : Type -> Type -> Type` functor from "base" because I need something that is `Type -> (0 _ : Type) -> Type`.
This feels like a _very_ niche problem. You'd basically have to be in #QTT or some other modal type theory where usage quantities are tracked.
I could change the test code to use a new "Const" with the right kind, but I wonder if this is a symptom where I need to change the quantities in my main code.
-
When binders have quantities like in #QTT, #Idris, or some versions of #GRTT do natural transformations have to have a irrelevant/erased/zero quantity on the universally qualified index/parameter? If so, when you you call it when the index in matchable? Is that a display map from category theory?
I'm calling them "NaturalTransformations" (https://gitlab.com/bss03/nested/-/blob/main/src/Nested.idr?ref_type=heads#L10) but I don't want to be abusing terminology. (I have a branch where I'm trying out the erased version, but it's not done.)
-
When binders have quantities like in #QTT, #Idris, or some versions of #GRTT do natural transformations have to have a irrelevant/erased/zero quantity on the universally qualified index/parameter? If so, when you you call it when the index in matchable? Is that a display map from category theory?
I'm calling them "NaturalTransformations" (https://gitlab.com/bss03/nested/-/blob/main/src/Nested.idr?ref_type=heads#L10) but I don't want to be abusing terminology. (I have a branch where I'm trying out the erased version, but it's not done.)