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
@[class]
multivariate functors, i.e. functor between the category of type vectors and the category of Type
def
mvfunctor.liftp
{n : ℕ}
{F : typevec n → Type v}
[mvfunctor F]
{α : typevec n} :
(Π (i : fin2 n), α i → Prop) → F α → Prop
predicate lifting over multivariate functors
Equations
- mvfunctor.liftp p x = ∃ (u : F (λ (i : fin2 n), subtype (p i))), mvfunctor.map (λ (i : fin2 n), subtype.val) u = x
def
mvfunctor.supp
{n : ℕ}
{F : typevec n → Type v}
[mvfunctor F]
{α : typevec n}
(x : F α)
(i : fin2 n) :
set (α i)
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 : α i | ∀ ⦃p : Π (i : fin2 n), α i → Prop⦄, mvfunctor.liftp p x → p i y}
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 y
@[class]
- id_map : ∀ {α : typevec n} (x : F α), mvfunctor.map typevec.id x = x
- comp_map : ∀ {α β γ : typevec n} (g : α.arrow β) (h : β.arrow γ) (x : F α), mvfunctor.map (typevec.comp h g) x = mvfunctor.map h (mvfunctor.map g x)
laws for mvfunctor
def
mvfunctor.liftp'
{n : ℕ}
{α : typevec n}
{F : typevec n → Type v}
[mvfunctor F] :
α.arrow (typevec.repeat n Prop) → F α → Prop
adapt mvfunctor.liftp to accept predicates as arrows
Equations
- mvfunctor.liftp' p = mvfunctor.liftp (λ (i : fin2 n) (x : α i), typevec.of_repeat (p i x))
def
mvfunctor.liftr'
{n : ℕ}
{α : typevec n}
{F : typevec n → Type v}
[mvfunctor F] :
(α.prod α).arrow (typevec.repeat n Prop) → F α → F α → Prop
adapt mvfunctor.liftp to accept relations as arrows
Equations
- mvfunctor.liftr' r = mvfunctor.liftr (λ (i : fin2 n) (x y : α i), typevec.of_repeat (r i (typevec.prod.mk i x y)))
@[simp]
theorem
mvfunctor.id_map
{n : ℕ}
{α : typevec n}
{F : typevec n → Type v}
[mvfunctor F]
[is_lawful_mvfunctor F]
(x : F α) :
mvfunctor.map typevec.id x = x
@[simp]
theorem
mvfunctor.id_map'
{n : ℕ}
{α : typevec n}
{F : typevec n → Type v}
[mvfunctor F]
[is_lawful_mvfunctor F]
(x : F α) :
mvfunctor.map (λ (i : fin2 n) (a : α i), a) x = x
theorem
mvfunctor.map_map
{n : ℕ}
{α β γ : typevec n}
{F : typevec n → Type v}
[mvfunctor F]
[is_lawful_mvfunctor F]
(g : α.arrow β)
(h : β.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}
(F : typevec n → Type v)
[mvfunctor F]
[is_lawful_mvfunctor F]
{p : F α → Prop}
{q : F β → Prop}
(f : α.arrow β)
(g : β.arrow α) :
typevec.comp f g = typevec.id → (∀ (u : F α), p u ↔ q (mvfunctor.map f u)) → ((∃ (u : F α), p u) ↔ ∃ (u : F β), q u)
theorem
mvfunctor.liftp_def
{n : ℕ}
{α : typevec n}
{F : typevec n → Type v}
[mvfunctor F]
(p : α.arrow (typevec.repeat n Prop))
[is_lawful_mvfunctor F]
(x : F α) :
mvfunctor.liftp' p x ↔ ∃ (u : F (typevec.subtype_ p)), mvfunctor.map (typevec.subtype_val p) u = x
theorem
mvfunctor.liftr_def
{n : ℕ}
{α : typevec n}
{F : typevec n → Type v}
[mvfunctor F]
(r : (α.prod α).arrow (typevec.repeat n Prop))
[is_lawful_mvfunctor F]
(x y : F α) :
mvfunctor.liftr' r x y ↔ ∃ (u : F (typevec.subtype_ r)), mvfunctor.map (typevec.comp typevec.prod.fst (typevec.subtype_val r)) u = x ∧ mvfunctor.map (typevec.comp typevec.prod.snd (typevec.subtype_val r)) u = y
theorem
mvfunctor.liftp_last_pred_iff
{n : ℕ}
{F : typevec (n + 1) → Type u_1}
[mvfunctor F]
[is_lawful_mvfunctor F]
{α : typevec n}
{β : Type u}
(p : β → Prop)
(x : F (α ::: β)) :
mvfunctor.liftp' (α.pred_last' p) x ↔ mvfunctor.liftp (α.pred_last p) x
theorem
mvfunctor.liftr_last_rel_iff
{n : ℕ}
{F : typevec (n + 1) → Type u_1}
[mvfunctor F]
[is_lawful_mvfunctor F]
{α : typevec n}
{β : Type u}
(rr : β → β → Prop)
(x y : F (α ::: β)) :
mvfunctor.liftr' (α.rel_last' rr) x y ↔ mvfunctor.liftr (α.rel_last rr) x y