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}
(p : Π (i : fin2 n), α i → Prop)
(x : F α) :
Prop
predicate lifting over multivariate functors
Equations
- mvfunctor.liftp p x = ∃ (u : F (λ (i : fin2 n), subtype (p i))), (λ (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)
(H : y ∈ mvfunctor.supp x i) :
p y
def
mvfunctor.liftp'
{n : ℕ}
{α : typevec n}
{F : typevec n → Type v}
[mvfunctor F]
(p : α ⟹ typevec.repeat n Prop)
(a : 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]
(r : α ⊗ α ⟹ typevec.repeat n Prop)
(a a_1 : 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 α) :
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 α) :
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 : α ⟹ β)
(g : β ⟹ α)
(h₀ : f ⊚ g = typevec.id)
(h₁ : ∀ (u : F α), p u ↔ q (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 : α ⟹ typevec.repeat n Prop)
[is_lawful_mvfunctor F]
(x : F α) :
mvfunctor.liftp' p x ↔ ∃ (u : F (typevec.subtype_ p)), typevec.subtype_val p <$$> u = x
theorem
mvfunctor.liftr_def
{n : ℕ}
{α : typevec n}
{F : typevec n → Type v}
[mvfunctor F]
(r : α ⊗ α ⟹ typevec.repeat n Prop)
[is_lawful_mvfunctor F]
(x y : F α) :
mvfunctor.liftr' r x y ↔ ∃ (u : F (typevec.subtype_ r)), (typevec.prod.fst ⊚ typevec.subtype_val r) <$$> u = x ∧ (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