[GOAL]
n : ℕ
A : Type u
F : A → TypeVec n → Type u
inst✝¹ : (α : A) → MvFunctor (F α)
inst✝ : (α : A) → MvQPF (F α)
⊢ ∀ {α : TypeVec n} (x : Sigma F α), (fun {α} => Sigma.abs F) ((fun {α} => Sigma.repr F) x) = x
[PROOFSTEP]
rintro α ⟨x, f⟩
[GOAL]
case mk
n : ℕ
A : Type u
F : A → TypeVec n → Type u
inst✝¹ : (α : A) → MvFunctor (F α)
inst✝ : (α : A) → MvQPF (F α)
α : TypeVec n
x : A
f : F x α
⊢ (fun {α} => Sigma.abs F) ((fun {α} => Sigma.repr F) { fst := x, snd := f }) = { fst := x, snd := f }
[PROOFSTEP]
simp only [Sigma.abs, Sigma.repr, Sigma.eta, abs_repr]
[GOAL]
n : ℕ
A : Type u
F : A → TypeVec n → Type u
inst✝¹ : (α : A) → MvFunctor (F α)
inst✝ : (α : A) → MvQPF (F α)
⊢ ∀ {α β : TypeVec n} (f : α ⟹ β) (p : MvPFunctor.Obj (Sigma.P F) α),
    (fun {α} => Sigma.abs F) (f <$$> p) = f <$$> (fun {α} => Sigma.abs F) p
[PROOFSTEP]
rintro α β f ⟨x, g⟩
[GOAL]
case mk
n : ℕ
A : Type u
F : A → TypeVec n → Type u
inst✝¹ : (α : A) → MvFunctor (F α)
inst✝ : (α : A) → MvQPF (F α)
α β : TypeVec n
f : α ⟹ β
x : (Sigma.P F).A
g : MvPFunctor.B (Sigma.P F) x ⟹ α
⊢ (fun {α} => Sigma.abs F) (f <$$> { fst := x, snd := g }) = f <$$> (fun {α} => Sigma.abs F) { fst := x, snd := g }
[PROOFSTEP]
simp only [Sigma.abs, MvPFunctor.map_eq]
[GOAL]
case mk
n : ℕ
A : Type u
F : A → TypeVec n → Type u
inst✝¹ : (α : A) → MvFunctor (F α)
inst✝ : (α : A) → MvQPF (F α)
α β : TypeVec n
f : α ⟹ β
x : (Sigma.P F).A
g : MvPFunctor.B (Sigma.P F) x ⟹ α
⊢ { fst := x.fst, snd := abs { fst := x.snd, snd := f ⊚ g } } =
    f <$$> { fst := x.fst, snd := abs { fst := x.snd, snd := g } }
[PROOFSTEP]
simp only [(· <$$> ·), ← abs_map, ← MvPFunctor.map_eq]
[GOAL]
n : ℕ
A : Type u
F : A → TypeVec n → Type u
inst✝¹ : (α : A) → MvFunctor (F α)
inst✝ : (α : A) → MvQPF (F α)
⊢ ∀ {α : TypeVec n} (x : Pi F α), Pi.abs F (Pi.repr F x) = x
[PROOFSTEP]
rintro α f
[GOAL]
n : ℕ
A : Type u
F : A → TypeVec n → Type u
inst✝¹ : (α : A) → MvFunctor (F α)
inst✝ : (α : A) → MvQPF (F α)
α : TypeVec n
f : Pi F α
⊢ Pi.abs F (Pi.repr F f) = f
[PROOFSTEP]
simp only [Pi.abs, Pi.repr, Sigma.eta, abs_repr]
[GOAL]
n : ℕ
A : Type u
F : A → TypeVec n → Type u
inst✝¹ : (α : A) → MvFunctor (F α)
inst✝ : (α : A) → MvQPF (F α)
⊢ ∀ {α β : TypeVec n} (f : α ⟹ β) (p : MvPFunctor.Obj (Pi.P F) α), Pi.abs F (f <$$> p) = f <$$> Pi.abs F p
[PROOFSTEP]
rintro α β f ⟨x, g⟩
[GOAL]
case mk
n : ℕ
A : Type u
F : A → TypeVec n → Type u
inst✝¹ : (α : A) → MvFunctor (F α)
inst✝ : (α : A) → MvQPF (F α)
α β : TypeVec n
f : α ⟹ β
x : (Pi.P F).A
g : MvPFunctor.B (Pi.P F) x ⟹ α
⊢ Pi.abs F (f <$$> { fst := x, snd := g }) = f <$$> Pi.abs F { fst := x, snd := g }
[PROOFSTEP]
simp only [Pi.abs, (· <$$> ·), ← abs_map]
[GOAL]
case mk
n : ℕ
A : Type u
F : A → TypeVec n → Type u
inst✝¹ : (α : A) → MvFunctor (F α)
inst✝ : (α : A) → MvQPF (F α)
α β : TypeVec n
f : α ⟹ β
x : (Pi.P F).A
g : MvPFunctor.B (Pi.P F) x ⟹ α
⊢ (match MvPFunctor.map (Pi.P F) f { fst := x, snd := g } with
    | { fst := a, snd := f } => fun x => abs { fst := a x, snd := fun i y => f i { fst := x, snd := y } }) =
    fun a => abs (MvPFunctor.map (P (F a)) f { fst := x a, snd := fun i y => g i { fst := a, snd := y } })
[PROOFSTEP]
rfl
