like, if you also have a type-level (^) operator, you could write
f : Int^2 -> Int
isn't that cute??
f : Int^2 -> Int
isn't that cute??
Comments
But_2 anyway Bool -> Int and Int x Int are iso so thats the same
_^_ : Type -> Nat -> Type
t ^ n = Fin n -> t
a^b remains as a synonym for b -> a and the type 2 denotes an anonymous enum with two inhabitants: .1 and .2
then the way you access the the two “fields” of `f : a^2` are f .1 and f .2
{ a = value, b = other value }
be the syntax for pattern matching (lambda case) in that case?
maybe with (x, y) being syntactic sugar for { .1 = x, .2 = y }
myPair : Π (Char, 2)
myPair = ('x', .1)
(where `Π B = (a : _) -> B a` in agda syntax)
you treat .n as a polymorphic variant that inhabits any anonymous enum with that tag, and since all “numeric” types N are defined as anonymous sums from .1 to .n then the tag .n inhabits all numeric types N and above
fromNat n = Fin n