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
- map : {α β : TypeVec n} → TypeVec.Arrow α β → F α → F β
Multivariate map, if
f : α ⟹ β
andx : F α
thenf <$$> x : 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 β
Instances For
theorem
MvFunctor.of_mem_supp
{n : ℕ}
{F : TypeVec n → Type v}
[MvFunctor F]
{α : TypeVec n}
{x : F α}
{P : ⦃i : Fin2 n⦄ → α i → Prop}
(h : MvFunctor.LiftP P x)
(i : Fin2 n)
(y : α i)
:
y ∈ MvFunctor.supp x i → P i y
- id_map : ∀ {α : TypeVec n} (x : F α), MvFunctor.map TypeVec.id x = x
map
preserved identities, i.e., maps identity onα
to identity onF α
- comp_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)
map
preserves compositions
laws for MvFunctor
Instances
def
MvFunctor.LiftP'
{n : ℕ}
{α : TypeVec n}
{F : TypeVec n → Type v}
[MvFunctor F]
(P : TypeVec.Arrow α (TypeVec.repeat n Prop))
:
F α → Prop
adapt MvFunctor.LiftP
to accept predicates as arrows
Instances For
def
MvFunctor.LiftR'
{n : ℕ}
{α : TypeVec n}
{F : TypeVec n → Type v}
[MvFunctor F]
(R : TypeVec.Arrow (TypeVec.prod α α) (TypeVec.repeat n Prop))
:
F α → F α → Prop
adapt MvFunctor.LiftR
to accept relations as arrows
Instances For
@[simp]
theorem
MvFunctor.id_map
{n : ℕ}
{α : TypeVec n}
{F : TypeVec n → Type v}
[MvFunctor F]
[LawfulMvFunctor F]
(x : F α)
:
MvFunctor.map TypeVec.id x = x
@[simp]
theorem
MvFunctor.id_map'
{n : ℕ}
{α : TypeVec n}
{F : TypeVec n → Type v}
[MvFunctor F]
[LawfulMvFunctor F]
(x : F α)
:
MvFunctor.map (fun _i a => a) x = x
theorem
MvFunctor.map_map
{n : ℕ}
{α : TypeVec n}
{β : TypeVec n}
{γ : TypeVec n}
{F : TypeVec n → Type v}
[MvFunctor F]
[LawfulMvFunctor F]
(g : TypeVec.Arrow α β)
(h : TypeVec.Arrow β γ)
(x : F α)
:
MvFunctor.map h (MvFunctor.map g x) = MvFunctor.map (TypeVec.comp h g) x
theorem
MvFunctor.exists_iff_exists_of_mono
{n : ℕ}
{α : TypeVec n}
{β : TypeVec n}
(F : TypeVec n → Type v)
[MvFunctor F]
[LawfulMvFunctor F]
{P : F α → Prop}
{q : F β → Prop}
(f : TypeVec.Arrow α β)
(g : TypeVec.Arrow β α)
(h₀ : TypeVec.comp f g = TypeVec.id)
(h₁ : ∀ (u : F α), P u ↔ q (MvFunctor.map f u))
:
(∃ u, P u) ↔ ∃ u, q u
theorem
MvFunctor.LiftP_def
{n : ℕ}
{α : TypeVec n}
{F : TypeVec n → Type v}
[MvFunctor F]
(P : TypeVec.Arrow α (TypeVec.repeat n Prop))
[LawfulMvFunctor F]
(x : F α)
:
MvFunctor.LiftP' P x ↔ ∃ u, MvFunctor.map (TypeVec.subtypeVal P) u = x
theorem
MvFunctor.LiftR_def
{n : ℕ}
{α : TypeVec n}
{F : TypeVec n → Type v}
[MvFunctor F]
(R : TypeVec.Arrow (TypeVec.prod α α) (TypeVec.repeat n Prop))
[LawfulMvFunctor F]
(x : F α)
(y : F α)
:
MvFunctor.LiftR' R x y ↔ ∃ u,
MvFunctor.map (TypeVec.comp TypeVec.prod.fst (TypeVec.subtypeVal R)) u = x ∧ MvFunctor.map (TypeVec.comp TypeVec.prod.snd (TypeVec.subtypeVal R)) u = y
theorem
MvFunctor.LiftP_PredLast_iff
{n : ℕ}
{F : TypeVec (n + 1) → Type u_1}
[MvFunctor F]
[LawfulMvFunctor F]
{α : TypeVec n}
{β : Type u}
(P : β → Prop)
(x : F (α ::: β))
:
MvFunctor.LiftP' (TypeVec.PredLast' α P) x ↔ MvFunctor.LiftP (TypeVec.PredLast α P) x
theorem
MvFunctor.LiftR_RelLast_iff
{n : ℕ}
{F : TypeVec (n + 1) → Type u_1}
[MvFunctor F]
[LawfulMvFunctor F]
{α : TypeVec n}
{β : Type u}
(rr : β → β → Prop)
(x : F (α ::: β))
(y : F (α ::: β))
:
MvFunctor.LiftR' (TypeVec.RelLast' α rr) x y ↔ MvFunctor.LiftR (fun {i} => TypeVec.RelLast α rr) x y