@acid2
First define a fixity for ~>. Then,
(~>) : (Type -> Type) -> (Type -> Type) -> Type
f ~> g = (i : Type) -> f i -> g i
-
-
Replying to @d_christiansen
@acid2 Note that you'll have to give it the i at most use sites.1 reply 0 retweets 0 likes -
Replying to @d_christiansen
@d_christiansen@acid2 The type seems incorrect and unnecessarily restricted, too: (~>) : (a -> Type) -> (a -> Type) -> a -> Type1 reply 0 retweets 0 likes -
Replying to @ertesx
@ertesx@d_christiansen@acid2 I thought (in agdris, apols) (~>) : (I -> Type) -> (I -> Type) -> Type (~>) {I} F G = (i : I) -> F i -> G i.2 replies 0 retweets 1 like -
Replying to @pigworker
@pigworker@d_christiansen@acid2 Wow, that looks weird. My Agda instinct does not like the pseudo-implicit i.1 reply 0 retweets 0 likes -
Replying to @ertesx
@ertesx@d_christiansen@acid2 In Agda, _~>_ : {I : Set} -> (I -> Set) -> (I -> Set) -> Set F ~> G = forall {i} -> F i -> G i2 replies 0 retweets 0 likes -
Replying to @pigworker
@pigworker@ertesx@d_christiansen@acid2 In idris: (~>) : {i : Type} -> (i -> Type) -> (i -> Type) -> Type f ~> g = {i : _} -> f i -> g i3 replies 0 retweets 0 likes -
Replying to @edwinbrady
@edwinbrady Do you have implicit lambda now?@ertesx@d_christiansen@acid21 reply 0 retweets 0 likes -
Replying to @pigworker
@pigworker@ertesx@d_christiansen@acid2 Yes. Not widely tested so I'd like to know if it works properly.2 replies 0 retweets 0 likes -
Replying to @edwinbrady
@edwinbrady If {x : S} -> T is now a first class type, then there are weird unavoidable corners.@ertesx@d_christiansen@acid21 reply 0 retweets 0 likes
@pigworker @ertesx @d_christiansen @acid2 It's not quite first class. Far too fiddly… I must write down the rules I've implemented.
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.