Library UniMath.Induction.M.ComputationalM
Refinement of M-types
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.Induction.FunctorCoalgebras_legacy.
Require Import UniMath.CategoryTheory.Categories.Type.Core.
Require Import UniMath.Induction.PolynomialFunctors.
Require Import UniMath.Induction.M.Core.
Require Import UniMath.Induction.M.Uniqueness.
The construction is called a refinement: as input we take any final coalgebra
for the respective polynomial functor describing an M-type (hence, with the
provable coiteration rule), the output is the refined final coalgebra with the
equational rule of coiteration holding definitionally: Lemma corec_computation
is proved merely by idpath. Of course, both coalgebras are equal - provably
(Lemma coalgebras_eq).
Local Open Scope cat.
Section Refinement.
Context (A : UU).
Context (B : A → UU).
Local Definition F : type_precat ⟶ type_precat
:= polynomial_functor A B.
Variable M0 : coalgebra F.
Local Definition carrierM0 : type_precat := coalgebra_ob F M0.
Local Definition destrM0 : type_precat ⟦ carrierM0, F carrierM0 ⟧
:= coalgebra_mor F M0.
Variable finalM0 : is_final M0.
Local Definition corecM0 (C : coalgebra F) : type_precat ⟦ coalgebra_ob F C, carrierM0 ⟧
:= pr1 (iscontrpr1 (finalM0 C)).
Lemma corec_equational_aux (C : coalgebra F) (c : coalgebra_ob F C) : is_coalgebra_homo F (corecM0 C).
Proof.
exact (pr2 (iscontrpr1 (finalM0 C))).
Defined.
Section Refinement.
Context (A : UU).
Context (B : A → UU).
Local Definition F : type_precat ⟶ type_precat
:= polynomial_functor A B.
Variable M0 : coalgebra F.
Local Definition carrierM0 : type_precat := coalgebra_ob F M0.
Local Definition destrM0 : type_precat ⟦ carrierM0, F carrierM0 ⟧
:= coalgebra_mor F M0.
Variable finalM0 : is_final M0.
Local Definition corecM0 (C : coalgebra F) : type_precat ⟦ coalgebra_ob F C, carrierM0 ⟧
:= pr1 (iscontrpr1 (finalM0 C)).
Lemma corec_equational_aux (C : coalgebra F) (c : coalgebra_ob F C) : is_coalgebra_homo F (corecM0 C).
Proof.
exact (pr2 (iscontrpr1 (finalM0 C))).
Defined.
recall the provable equation governing corec
Lemma corec_equational (C : coalgebra F) (c : coalgebra_ob F C) :
destrM0 (corecM0 C c) = # F (corecM0 C) (coalgebra_mor F C c).
Proof.
set (aux := toforallpaths _ _ _ (corec_equational_aux C c)).
apply pathsinv0, aux.
Defined.
Local Open Scope functions.
destrM0 (corecM0 C c) = # F (corecM0 C) (coalgebra_mor F C c).
Proof.
set (aux := toforallpaths _ _ _ (corec_equational_aux C c)).
apply pathsinv0, aux.
Defined.
Local Open Scope functions.
refinement of the final coalgebra to purely coiterative elements
Definition is_purelycoiterativeM0 (m0 : carrierM0) : UU := ∃ (C : coalgebra F) (c : coalgebra_ob F C), corecM0 C c = m0.
Definition carrierM : UU := total2 is_purelycoiterativeM0.
Definition carrierM : UU := total2 is_purelycoiterativeM0.
definition of the corecursor
Definition corecM (C : coalgebra F) (c : coalgebra_ob F C) : carrierM.
Proof.
exists (corecM0 C c). apply hinhpr. exists C, c. apply idpath.
Defined.
Proof.
exists (corecM0 C c). apply hinhpr. exists C, c. apply idpath.
Defined.
a form of functoriality of F w.r.t. convertibility
Lemma corecM_corecM0 (C : coalgebra F) (cf: F (coalgebra_ob F C)) :
#F pr1 (#F (corecM C) cf) = #F (corecM0 C) cf.
Proof.
apply idpath.
Defined.
#F pr1 (#F (corecM C) cf) = #F (corecM0 C) cf.
Proof.
apply idpath.
Defined.
definition of a proposition we factor the computation through
in order to show P to be a proposition, a not obviously equivalent
formulation is given for which it is easy to show isaprop
Local Definition P' (m0 : carrierM0) : UU :=
∑ ap : (∑ a : A, pr1 (destrM0 m0) = a),
∏ b : B (pr1 ap),
∑ mp : (∑ m0' : carrierM0,
transportf (λ a : A, B a -> carrierM0)
(pr2 ap)
(pr2 (destrM0 m0)) b =
m0'),
is_purelycoiterativeM0 (pr1 mp).
∑ ap : (∑ a : A, pr1 (destrM0 m0) = a),
∏ b : B (pr1 ap),
∑ mp : (∑ m0' : carrierM0,
transportf (λ a : A, B a -> carrierM0)
(pr2 ap)
(pr2 (destrM0 m0)) b =
m0'),
is_purelycoiterativeM0 (pr1 mp).
the easy auxiliary lemma
Local Lemma P'_isaprop (m0 : carrierM0) : isaprop (P' m0).
Proof.
apply isofhleveltotal2.
- apply isofhlevelcontr.
apply iscontrcoconusfromt.
- intro ap; induction ap as [a p].
apply impred; intros b.
apply isofhleveltotal2.
+ apply isofhlevelcontr.
apply iscontrcoconusfromt.
+ intro mp; induction mp as [m0' q].
apply isapropishinh.
Defined.
Proof.
apply isofhleveltotal2.
- apply isofhlevelcontr.
apply iscontrcoconusfromt.
- intro ap; induction ap as [a p].
apply impred; intros b.
apply isofhleveltotal2.
+ apply isofhlevelcontr.
apply iscontrcoconusfromt.
+ intro mp; induction mp as [m0' q].
apply isapropishinh.
Defined.
the crucial lemma
Local Lemma P_isaprop (m0 : carrierM0) : isaprop (P m0).
Proof.
use (@isofhlevelweqb _ _ (P' m0) _ (P'_isaprop m0)).
eapply weqcomp.
{ apply weqtotal2asstor. }
eapply weqcomp.
2: { apply invweq.
apply weqtotal2asstor. }
apply weqfibtototal; intro a.
eapply weqcomp.
{ apply weqfibtototal; intro f.
apply total2_paths_equiv.
}
unfold PathPair. simpl.
eapply weqcomp.
{ apply weqtotal2comm. }
apply weqfibtototal; intro p.
match goal with |[ |- _ ≃ ?rhs] => set (therhs := rhs) end.
eapply weqcomp.
{ set (H1 := weqfuntototaltototal (B a) is_purelycoiterativeM0).
apply (weqbandf H1 _ (fun fg => transportf (λ a : A, B a -> carrierM0) p (pr2 (destrM0 m0)) = pr1 fg)). cbn.
intro f.
apply idweq.
}
simpl.
eapply weqcomp.
{ apply weqtotal2asstor. }
simpl.
eapply weqcomp.
{ apply weqfibtototal; intro f.
apply weqfibtototal; intro Hyp.
apply weqtoforallpaths.
}
simpl.
unfold homot.
eapply weqcomp.
{ apply weqfibtototal; intro f.
apply invweq.
apply (weqforalltototal _ (fun x _ => transportf (λ a0 : A, B a0 → carrierM0) p (pr2 (destrM0 m0)) x = f x)). }
simpl.
eapply weqcomp.
{ apply invweq.
apply (weqforalltototal _ (fun b y => ∑ _ : is_purelycoiterativeM0 y, transportf (λ a0 : A, B a0 → carrierM0) p (pr2 (destrM0 m0)) b = y)). }
apply weqonsecfibers; intro b.
clear therhs.
eapply weqcomp.
{ apply weqfibtototal; intro m0'.
apply weqdirprodcomm.
}
simpl.
apply invweq.
apply weqtotal2asstor. Defined.
Local Lemma destrM'_aux (m0 : carrierM0) (C : coalgebra F) (c : coalgebra_ob F C) (H1 : corecM0 C c = m0) :
destrM0 m0 = # F pr1 ((# F (corecM C) ∘ coalgebra_mor F C) c).
Proof.
etrans.
{ rewrite <- H1. apply corec_equational. }
apply pathsinv0, corecM_corecM0.
Defined.
Local Definition destrM' (m : carrierM) : P (pr1 m).
Proof.
induction m as [m0 H]. apply (squash_to_prop H); [apply P_isaprop|].
intros [C [c H1]].
exists ((# F (corecM C) ∘ (coalgebra_mor F C)) c).
cbn [pr1].
apply destrM'_aux.
assumption.
Defined.
Definition destrM (m : carrierM) : F carrierM :=
pr1 (destrM' m).
Definition M : coalgebra F :=
(carrierM,, destrM).
Proof.
use (@isofhlevelweqb _ _ (P' m0) _ (P'_isaprop m0)).
eapply weqcomp.
{ apply weqtotal2asstor. }
eapply weqcomp.
2: { apply invweq.
apply weqtotal2asstor. }
apply weqfibtototal; intro a.
eapply weqcomp.
{ apply weqfibtototal; intro f.
apply total2_paths_equiv.
}
unfold PathPair. simpl.
eapply weqcomp.
{ apply weqtotal2comm. }
apply weqfibtototal; intro p.
match goal with |[ |- _ ≃ ?rhs] => set (therhs := rhs) end.
eapply weqcomp.
{ set (H1 := weqfuntototaltototal (B a) is_purelycoiterativeM0).
apply (weqbandf H1 _ (fun fg => transportf (λ a : A, B a -> carrierM0) p (pr2 (destrM0 m0)) = pr1 fg)). cbn.
intro f.
apply idweq.
}
simpl.
eapply weqcomp.
{ apply weqtotal2asstor. }
simpl.
eapply weqcomp.
{ apply weqfibtototal; intro f.
apply weqfibtototal; intro Hyp.
apply weqtoforallpaths.
}
simpl.
unfold homot.
eapply weqcomp.
{ apply weqfibtototal; intro f.
apply invweq.
apply (weqforalltototal _ (fun x _ => transportf (λ a0 : A, B a0 → carrierM0) p (pr2 (destrM0 m0)) x = f x)). }
simpl.
eapply weqcomp.
{ apply invweq.
apply (weqforalltototal _ (fun b y => ∑ _ : is_purelycoiterativeM0 y, transportf (λ a0 : A, B a0 → carrierM0) p (pr2 (destrM0 m0)) b = y)). }
apply weqonsecfibers; intro b.
clear therhs.
eapply weqcomp.
{ apply weqfibtototal; intro m0'.
apply weqdirprodcomm.
}
simpl.
apply invweq.
apply weqtotal2asstor. Defined.
Local Lemma destrM'_aux (m0 : carrierM0) (C : coalgebra F) (c : coalgebra_ob F C) (H1 : corecM0 C c = m0) :
destrM0 m0 = # F pr1 ((# F (corecM C) ∘ coalgebra_mor F C) c).
Proof.
etrans.
{ rewrite <- H1. apply corec_equational. }
apply pathsinv0, corecM_corecM0.
Defined.
Local Definition destrM' (m : carrierM) : P (pr1 m).
Proof.
induction m as [m0 H]. apply (squash_to_prop H); [apply P_isaprop|].
intros [C [c H1]].
exists ((# F (corecM C) ∘ (coalgebra_mor F C)) c).
cbn [pr1].
apply destrM'_aux.
assumption.
Defined.
Definition destrM (m : carrierM) : F carrierM :=
pr1 (destrM' m).
Definition M : coalgebra F :=
(carrierM,, destrM).
the destructor satisfies the corecursion equation definitionally
Lemma corec_computation (C : coalgebra F) (c : coalgebra_ob F C) :
destrM (corecM C c) = # F (corecM C) (coalgebra_mor F C c).
Proof.
apply idpath.
Defined.
destrM (corecM C c) = # F (corecM C) (coalgebra_mor F C c).
Proof.
apply idpath.
Defined.
for the moment only an experiment
Goal ∏ (m0 : carrierM0), P m0 -> is_purelycoiterativeM0 m0.
Proof.
intros m0 [[a f] Hyp].
simpl in Hyp.
unfold polynomial_functor_arr in Hyp.
simpl in Hyp.
Abort.
Proof.
intros m0 [[a f] Hyp].
simpl in Hyp.
unfold polynomial_functor_arr in Hyp.
simpl in Hyp.
Abort.
the two carriers are equal
Lemma eq_corecM0 (m0 : carrierM0) :
corecM0 M0 m0 = m0.
Proof.
apply pathsinv0.
assert (aux := path_to_ctr _ _ (finalM0 M0) (pr1 (coalgebra_homo_id F M0)) (pr2 (coalgebra_homo_id F M0))).
apply toforallpaths in aux.
apply aux.
Defined.
Definition injectM0 (m0 : carrierM0) :
∃ C c, corecM0 C c = m0.
Proof.
apply hinhpr. exists M0, m0. apply eq_corecM0.
Defined.
Lemma carriers_weq :
carrierM ≃ carrierM0.
Proof.
apply (weq_iso pr1 (λ m0, m0,, injectM0 m0)).
- intros [m H]. cbn. apply maponpaths, ishinh_irrel.
- intros x. cbn. apply idpath.
Defined.
Lemma carriers_eq :
carrierM = carrierM0.
Proof.
apply weqtopaths, carriers_weq.
Defined.
corecM0 M0 m0 = m0.
Proof.
apply pathsinv0.
assert (aux := path_to_ctr _ _ (finalM0 M0) (pr1 (coalgebra_homo_id F M0)) (pr2 (coalgebra_homo_id F M0))).
apply toforallpaths in aux.
apply aux.
Defined.
Definition injectM0 (m0 : carrierM0) :
∃ C c, corecM0 C c = m0.
Proof.
apply hinhpr. exists M0, m0. apply eq_corecM0.
Defined.
Lemma carriers_weq :
carrierM ≃ carrierM0.
Proof.
apply (weq_iso pr1 (λ m0, m0,, injectM0 m0)).
- intros [m H]. cbn. apply maponpaths, ishinh_irrel.
- intros x. cbn. apply idpath.
Defined.
Lemma carriers_eq :
carrierM = carrierM0.
Proof.
apply weqtopaths, carriers_weq.
Defined.
needs to be transparent
Local Lemma eq1 (m0 : carrierM0) :
transportf (λ X, X → F X) carriers_eq destrM m0
= transportf (λ X, F X) carriers_eq (destrM (transportf (λ X, X) (!carriers_eq) m0)).
Proof.
destruct carriers_eq. apply idpath.
Defined.
Local Lemma eq2 (m0 : carrierM0) :
transportf (λ X, X) (!carriers_eq) m0 = m0,, injectM0 m0.
Proof.
apply (transportf_pathsinv0' (idfun UU) carriers_eq).
unfold carriers_eq. rewrite weqpath_transport. apply idpath.
Defined.
Local Lemma eq3 (m0 : carrierM0) :
destrM (m0,, injectM0 m0) = pr1 (destrM0 m0),, corecM M0 ∘ pr2 (destrM0 m0).
Proof.
apply idpath.
Defined.
Lemma coalgebras_eq :
M = M0.
Proof.
use total2_paths_f; [apply carriers_eq|].
apply funextfun. intro m0.
rewrite eq1. rewrite eq2. rewrite eq3.
cbn. unfold polynomial_functor_obj.
rewrite transportf_total2_const.
use total2_paths_f; [apply idpath|].
cbn. apply funextsec. intros b. rewrite <- UniMath.MoreFoundations.PartA.helper_A.
unfold carriers_eq. rewrite weqpath_transport.
cbn. rewrite eq_corecM0. apply idpath.
Defined.
Lemma finalM : is_final M.
Proof.
rewrite coalgebras_eq. apply finalM0.
Defined.
End Refinement.