Functors between the category of tuples of types, and the category Type
Features:
MvFunctor n
: the type class of multivariate functors
f <$$> x
: notation for map
Multivariate map, if
f : α ⟹ β⟹ β
andx : F α
thenf <$$> x : F β
.map : {α β : TypeVec n} → TypeVec.Arrow α β → F α → F β
Multivariate functors, i.e. functor between the category of type vectors and the category of Type
Instances
Multivariate map, if f : α ⟹ β⟹ β
and x : F α
then f <$$> x : F β
Equations
- One or more equations did not get rendered due to their size.
predicate lifting over multivariate functors
Equations
- MvFunctor.LiftP P x = ∃ u, MvFunctor.map (fun i => Subtype.val) u = x
relational lifting over multivariate functors
Equations
- MvFunctor.LiftR R x y = ∃ u, MvFunctor.map (fun i t => t.val.fst) u = x ∧ MvFunctor.map (fun i t => t.val.snd) u = y
given x : F α
and a projection i
of type vector α
, supp x i
is the set
of α.i
contained in x
Equations
- MvFunctor.supp x i = { y | ⦃P : (i : Fin2 n) → α i → Prop⦄ → MvFunctor.LiftP P x → P i y }
map
preserved identities, i.e., maps identity onα
to identity onF α
id_map : ∀ {α : TypeVec n} (x : F α), MvFunctor.map TypeVec.id x = xmap
preserves compositionscomp_map : ∀ {α β γ : TypeVec n} (g : TypeVec.Arrow α β) (h : TypeVec.Arrow β γ) (x : F α), MvFunctor.map (TypeVec.comp h g) x = MvFunctor.map h (MvFunctor.map g x)
laws for MvFunctor
Instances
adapt MvFunctor.LiftP
to accept predicates as arrows
Equations
- MvFunctor.LiftP' P = MvFunctor.LiftP fun i x => TypeVec.ofRepeat (P i x)
adapt MvFunctor.LiftR
to accept relations as arrows
Equations
- MvFunctor.LiftR' R = MvFunctor.LiftR fun i x y => TypeVec.ofRepeat (R i (TypeVec.prod.mk i x y))