English
The abstraction and representation are inverses up to bisimulation: applying abs to repr x yields the Cofix element x.
Русский
Абстракция и представление обратны друг другу в бисимуляционной эквивалентности: abs (repr x) = x.
LaTeX
$$$\\forall x:\\; \\mathrm{Cofix}\\,F\\,\\alpha, \\operatorname{Quot.mk}\\; MvQPF.Mcongr (x.repr) = x$$$
Lean4
theorem liftR_map_last [lawful : LawfulMvFunctor F] {α : TypeVec n} {ι ι'} (R : ι' → ι' → Prop) (x : F (α ::: ι))
(f g : ι → ι') (hh : ∀ x : ι, R (f x) (g x)) : LiftR' (RelLast' _ R) ((id ::: f) <$$> x) ((id ::: g) <$$> x) :=
let h : ι → { x : ι' × ι' // uncurry R x } := fun x => ⟨(f x, g x), hh x⟩
let b : (α ::: ι) ⟹ _ := @diagSub n α ::: h
let c :
(Subtype_ α.repeatEq ::: { x // uncurry R x }) ⟹
((fun i : Fin2 n => { x // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R)) :=
ofSubtype _ ::: id
have hh : subtypeVal _ ⊚ toSubtype _ ⊚ fromAppend1DropLast ⊚ c ⊚ b = ((id ::: f) ⊗' (id ::: g)) ⊚ prod.diag :=
by
dsimp [b]
apply eq_of_drop_last_eq
· dsimp
simp only [prod_map_id, TypeVec.id_comp]
erw [toSubtype_of_subtype_assoc, TypeVec.id_comp]
clear liftR_map_last q lawful F x R f g hh h b c
ext (i x) : 2
induction i with
| fz => rfl
| fs _ ih => apply ih
simp only [lastFun_from_append1_drop_last, lastFun_toSubtype, lastFun_appendFun, lastFun_subtypeVal,
Function.id_comp, lastFun_comp, lastFun_prod]
ext1
rfl
liftR_map _ _ _ _ (toSubtype _ ⊚ fromAppend1DropLast ⊚ c ⊚ b) hh
