Library UniMath.Folds.folds_isomorphism
Univalent FOLDS
Benedikt Ahrens, following notes by Michael Shulman
Contents of this file:
- Definition of type of isomorphism folds_iso a b in a FOLDS precategory
- Some lemmas expressing naturality of maps ϕX
- Components ϕ₂ and ϕ∙ are determined by ϕ₁
- Identity isomorphim id_folds_iso, inverse inv_folds_iso and composition
- Map folds_iso_from_iso associating to any FOLDS precat isomorphism an isomorphism in the corresponding precategory à la RezkCompletion
- Map iso_from_folds_iso doing the converse, still departing from a FOLDS precategory
- Lemma: folds_iso_from_iso and iso_from_folds_iso are inverse to each other
Require Import UniMath.Folds.UnicodeNotations.
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.Foundations.UnivalenceAxiom.
Require Import UniMath.CategoryTheory.total2_paths.
Require Import UniMath.CategoryTheory.Categories.
Require Import UniMath.Folds.aux_lemmas.
Require Import UniMath.Folds.folds_precat.
Require Import UniMath.Folds.from_precats_to_folds_and_back.
Local Notation "a ⇒ b" := (folds_morphisms a b).
Section folds_iso_def.
Variable C : folds_precat.
Local Notation C':= (precat_from_folds_precat C).
Local Notation "f □ g" := (compose (C:=C') f g) (at level 40, no associativity).
Local Notation "'id' a" := (identity (C:=C') a) (at level 30).
Definition folds_iso_data (a b : C) : UU :=
((∏ {x : C}, (x ⇒ a) ≃ (x ⇒ b))
× (∏ {z : C}, (a ⇒ z) ≃ (b ⇒ z)))
× ((a ⇒ a) ≃ (b ⇒ b)).
Definition ϕ₁ {a b : C} (f : folds_iso_data a b) {x : C} : (x ⇒ a) ≃ (x ⇒ b) :=
pr1 (pr1 f) x.
Definition ϕ₂ {a b : C} (f : folds_iso_data a b) {z : C} : (a ⇒ z) ≃ (b ⇒ z) :=
pr2 (pr1 f) z.
Definition ϕo {a b : C} (f : folds_iso_data a b) : (a ⇒ a) ≃ (b ⇒ b) :=
pr2 f.
Notation "ϕ∙" := ϕo.
Definition folds_iso_prop {a b : C} (i : folds_iso_data a b) : UU :=
((((∏ (x y : C) (f : x ⇒ y) (g : y ⇒ a) (h : x ⇒ a), T f g h ≃ T f ((ϕ₁ i) g) ((ϕ₁ i) h))
× (∏ (x z : C) (f : x ⇒ a) (g : a ⇒ z) (h : x ⇒ z), T f g h ≃ T ((ϕ₁ i) f) ((ϕ₂ i) g) h))
× (∏ (z w : C) (f : a ⇒ z) (g : z ⇒ w) (h : a ⇒ w), T f g h ≃ T ((ϕ₂ i) f) g ((ϕ₂ i) h)))
× (((∏ (x : C) (f : x ⇒ a) (g : a ⇒ a) (h : x ⇒ a), T f g h ≃ T ((ϕ₁ i) f) ((ϕo i) g) ((ϕ₁ i) h))
× (∏ (x : C) (f : a ⇒ x) (g : x ⇒ a) (h : a ⇒ a), T f g h ≃ T ((ϕ₂ i) f) ((ϕ₁ i) g) ((ϕ∙ i) h)))
× ((∏ (x : C) (f : a ⇒ a) (g h : a ⇒ x), T f g h ≃ T ((ϕ∙ i) f) ((ϕ₂ i) g) ((ϕ₂ i) h))
× (∏ f g h : a ⇒ a, T f g h ≃ T ((ϕ∙ i) f) ((ϕ∙ i) g) ((ϕ∙ i) h)))))
× (∏ f : a ⇒ a, I f ≃ I ((ϕ∙ i) f)).
Definition isaprop_folds_iso_prop (a b : C) (i : folds_iso_data a b) : isaprop (folds_iso_prop i).
Proof.
repeat (apply isapropdirprod);
repeat (apply impred; intro); apply isapropweqtoprop; apply pr2.
Qed.
Definition folds_iso (a b : C) := ∑ i : folds_iso_data a b, folds_iso_prop i.
Definition folds_iso_data_from_folds_iso {a b : C} : folds_iso a b → folds_iso_data a b
:= λ i, pr1 i.
Coercion folds_iso_data_from_folds_iso : folds_iso >-> folds_iso_data.
Lemma folds_iso_eq {a b : C} (i i' : folds_iso a b) :
folds_iso_data_from_folds_iso i = folds_iso_data_from_folds_iso i' → i = i'.
Proof.
intro H.
apply subtypeEquality.
- intro; apply isaprop_folds_iso_prop.
- assumption.
Qed.
Lemmas about FOLDS isomorphisms
the families of equivalences constituting a FOLDS isomorphism are given by compositionSection about_folds_isos.
Context {a b : C}.
Section fix_a_folds_iso.
Variable (i : folds_iso a b).
Lemma ϕ₁_is_comp (x : C) (f : x ⇒ a) : ϕ₁ i f = f □ (ϕ₁ i (id _ )).
Proof.
set (q:=pr1 (pr1 (pr1 (pr1 (pr2 i))))).
specialize (q _ _ f (id _ ) f).
set (q':=pr1 q ); clearbody q'.
assert (H: T f (id a) f).
{ set (H:= pr1 (pr2 (pr1 (pr2 C)))).
apply H. apply I_func_I. }
set (q'H:= q' H). clearbody q'H; clear H q' q.
apply path_to_ctr. assumption.
Qed.
Lemma ϕ₂_is_comp (z : C) (g : a ⇒ z) : ϕ₂ i g = ϕ₂ i (id _ ) □ g.
Proof.
set (q:=pr2 (pr1 (pr1 (pr2 i)))). simpl in q.
specialize (q _ _ (id _ ) g g).
set (q':=pr1 q ); clearbody q'.
assert (H: T (id a) g g).
{ set (H:= pr2 (pr2 (pr1 (pr2 C)))).
apply H. apply I_func_I. }
set (q'H:= q' H). clearbody q'H; clear H q' q.
apply path_to_ctr. assumption.
Qed.
Lemma ϕ₁_ϕ₂_id : ϕ₁ i (id _ ) □ (ϕ₂ i (id _ )) = id _.
Proof.
set (q:=pr2 (pr1 (pr1 (pr1 (pr2 i))))). simpl in q.
specialize (q _ _ (id _ ) (id _ ) (id _ )).
set (q':=pr1 q ); clearbody q'.
apply comp_compose2'.
apply q'.
apply comp_compose2.
apply T_I_l.
Qed.
Lemma ϕo_id : ϕ∙ i (id _ ) = id _ .
Proof.
apply id_identity2'.
apply (pr2 (pr2 i)).
apply I_func_I.
Qed.
Lemma ϕ₂_ϕ₁_id: ϕ₂ i (id a) □ ϕ₁ i (id a) = id b.
Proof.
set (H':= pr2 (pr1 (pr2 (pr1 (pr2 i))))).
simpl in H'.
specialize (H' _ (id _ ) (id _ ) (id _ )).
simpl in H'.
rewrite <- ϕo_id.
apply comp_compose2'.
apply H'.
apply comp_compose2.
apply T_I_l.
Qed.
Lemma ϕ₁_ϕ₂_are_inverse : is_inverse_in_precat (C:= C') (ϕ₁ i (id _ )) (ϕ₂ i (id _ )).
Proof.
split.
- apply ϕ₁_ϕ₂_id.
- apply ϕ₂_ϕ₁_id.
Qed.
Lemma ϕo_ϕ₁_ϕ₂ (f : a ⇒ a) : ϕ∙ i f = (ϕ₂ i (id _ ) □ f) □ ϕ₁ i (id _).
Proof.
set (q:=pr2 (pr1 (pr2 (pr1 (pr2 i))))); simpl in q; clearbody q.
specialize (q _ f (id _ ) f).
set (q':=pr1 q). clearbody q'. simpl in q'. clear q.
match goal with | [_ : ?a → _ |- _ ] ⇒ assert a end.
{ apply comp_compose2. apply (@id_right C'). }
specialize (q' X). clear X.
set (q:= comp_compose2' q'). clearbody q; clear q'.
simpl in ×.
change (ϕ∙ i f) with (ϕ∙ (pr1 i) f).
rewrite <- q. clear q.
rewrite ϕ₂_is_comp. apply idpath.
Qed.
End fix_a_folds_iso.
Variables i i' : folds_iso a b.
Hypothesis H : ϕ₁ i (id _ ) = ϕ₁ i' (id _ ).
Lemma ϕ₂_determined : ∏ x (f : a ⇒ x) , ϕ₂ i f = ϕ₂ i' f.
Proof.
intros x f.
rewrite (ϕ₂_is_comp i).
rewrite (ϕ₂_is_comp i').
assert (H': is_inverse_in_precat (C:=C') (ϕ₁ i (id _ )) (ϕ₂ i' (id _ ))).
{ split.
- rewrite H. apply ϕ₁_ϕ₂_id.
- rewrite H. apply ϕ₂_ϕ₁_id. }
assert (X : ϕ₂ i (id _ ) = ϕ₂ i' (id _ )).
{ set (H1:= inverse_unique_precat C' _ _ _ _ _ (ϕ₁_ϕ₂_are_inverse i) H').
assumption.
}
rewrite X.
apply idpath.
Qed.
Lemma ϕo_determined : ∏ f, ϕ∙ i f = ϕ∙ i' f.
Proof.
intro f.
do 2 rewrite ϕo_ϕ₁_ϕ₂.
rewrite ϕ₂_determined.
rewrite H.
apply idpath.
Qed.
Lemma folds_iso_equal : i = i'.
Proof.
apply folds_iso_eq.
apply dirprodeq.
- apply dirprodeq.
+ apply funextsec; intro.
apply subtypeEquality.
× intro. apply isapropisweq.
× apply funextfun; intro f.
eapply pathscomp0.
{ apply ϕ₁_is_comp. }
symmetry.
eapply pathscomp0.
{ apply ϕ₁_is_comp. }
rewrite H. apply idpath.
+ apply funextsec; intro.
apply subtypeEquality.
× intro; apply isapropisweq.
× apply funextfun. unfold homot. apply ϕ₂_determined.
- apply subtypeEquality.
intro. apply isapropisweq.
apply funextfun. intro t.
apply ϕo_determined.
Qed.
End about_folds_isos.
Definition id_folds_iso_data (a : C) : folds_iso_data a a.
Proof.
repeat split.
- intro x. apply idweq.
- intro z. apply idweq.
- apply idweq.
Defined.
Lemma id_folds_iso_prop (a : C) : folds_iso_prop (id_folds_iso_data a).
Proof.
repeat split; intros; apply idweq.
Qed.
Definition id_folds_iso (a : C) : folds_iso a a := tpair _ (id_folds_iso_data a) (id_folds_iso_prop a).
Section folds_iso_inverse.
Context {a b : C} (i : folds_iso a b).
Definition inv_folds_iso_data : folds_iso_data b a.
Proof.
repeat split.
- intro x. exact (invweq (ϕ₁ i)).
- intro z. exact (invweq (ϕ₂ i)).
- exact (invweq (ϕ∙ i)).
Defined.
Lemma inv_folds_iso_prop : folds_iso_prop inv_folds_iso_data.
Proof.
repeat split; intros.
- simpl. apply invweq.
set (q:=pr1 (pr1 (pr1 (pr1 (pr2 i))))). clearbody q.
set (q':= q _ _ f (invmap (ϕ₁ i) g) (invmap (ϕ₁ i) h)).
repeat rewrite (homotweqinvweq (ϕ₁ i)) in q'.
apply q'.
- simpl. apply invweq.
set (q:=pr2 (pr1 (pr1 (pr1 (pr2 i))))). simpl in q; clearbody q.
set (q':= q _ _ (invmap (ϕ₁ i) f) (invmap (ϕ₂ i) g) h); clearbody q'.
repeat rewrite homotweqinvweq in q'.
apply q'.
- simpl. apply invweq.
set (q:= ((pr2 (pr1 (pr1 (pr2 i)))))). clearbody q; simpl in q.
set (q':= q _ _ (invmap (ϕ₂ i) f) g (invmap (ϕ₂ i) h) ).
repeat rewrite homotweqinvweq in q'.
apply q'.
- simpl; apply invweq.
set (q:= pr1 (pr1 (pr2 (pr1 (pr2 i))))). clearbody q; simpl in q.
set (q':= q _ (invmap (ϕ₁ i) f) (invmap (ϕ∙ i) g) (invmap (ϕ₁ i) h)).
repeat rewrite homotweqinvweq in q'.
apply q'.
- simpl; apply invweq.
set (q:= pr2 (pr1 (pr2 (pr1 (pr2 i))))). clearbody q; simpl in q.
set (q':= q _ (invmap (ϕ₂ i) f) (invmap (ϕ₁ i) g) (invmap (ϕ∙ i) h)).
repeat rewrite homotweqinvweq in q'.
apply q'.
- simpl. apply invweq.
set (q:= pr1 (pr2 (pr2 (pr1 (pr2 i))))). clearbody q; simpl in q.
specialize (q _ (invmap (ϕ∙ i) f) (invmap (ϕ₂ i) g) (invmap (ϕ₂ i) h)).
repeat rewrite homotweqinvweq in q.
apply q.
- simpl. apply invweq.
set (q:= pr2 (pr2 (pr2 (pr1 (pr2 i))))). clearbody q; simpl in q.
specialize (q (invmap (ϕ∙ i) f) (invmap (ϕ∙ i) g) (invmap (ϕ∙ i) h)).
repeat rewrite homotweqinvweq in q.
apply q.
- simpl. apply invweq.
set (q:= pr2 (pr2 i)). simpl in q; clearbody q.
specialize (q (invmap (ϕ∙ i) f)).
rewrite homotweqinvweq in q.
apply q.
Qed.
Definition inv_folds_iso : folds_iso b a :=
tpair _ inv_folds_iso_data inv_folds_iso_prop.
End folds_iso_inverse.
Section folds_iso_comp.
Context {a b c : C} (i : folds_iso a b) (i' : folds_iso b c).
Definition folds_iso_comp_data : folds_iso_data a c.
Proof.
repeat split.
- intro x; apply (weqcomp (ϕ₁ i) (ϕ₁ i')).
- intro z; apply (weqcomp (ϕ₂ i) (ϕ₂ i')).
- apply (weqcomp (ϕ∙ i) (ϕ∙ i')).
Defined.
Lemma folds_iso_comp_prop : folds_iso_prop folds_iso_comp_data.
Proof.
repeat split.
- intros. simpl. eapply weqcomp.
+ apply (pr1 (pr1 (pr1 (pr1 (pr2 i))))).
+ apply (pr1 (pr1 (pr1 (pr1 (pr2 i'))))).
- intros; simpl; eapply weqcomp.
+ apply (pr2 (pr1 (pr1 (pr1 (pr2 i))))).
+ apply (pr2 (pr1 (pr1 (pr1 (pr2 i'))))).
- intros; simpl; eapply weqcomp.
+ apply (pr2 (pr1 (pr1 (pr2 i)))).
+ apply (pr2 (pr1 (pr1 (pr2 i')))).
- intros; simpl; eapply weqcomp.
+ apply (pr1 (pr1 (pr2 (pr1 (pr2 i))))).
+ apply (pr1 (pr1 (pr2 (pr1 (pr2 i'))))).
- intros; simpl; eapply weqcomp.
+ apply (pr2 (pr1 (pr2 (pr1 (pr2 i))))).
+ apply (pr2 (pr1 (pr2 (pr1 (pr2 i'))))).
- intros; simpl; eapply weqcomp.
+ apply (pr1 (pr2 (pr2 (pr1 (pr2 i))))).
+ apply (pr1 (pr2 (pr2 (pr1 (pr2 i'))))).
- intros; simpl; eapply weqcomp.
+ apply (pr2 (pr2 (pr2 (pr1 (pr2 i))))).
+ apply (pr2 (pr2 (pr2 (pr1 (pr2 i'))))).
- intros; simpl; eapply weqcomp.
+ apply (pr2 (pr2 i)).
+ apply (pr2 (pr2 i')).
Qed.
End folds_iso_comp.
Section from_iso_to_folds_iso.
Variables a b : C.
Variable f : z_iso (C:=C') a b.
Definition folds_iso_data_from_z_iso : folds_iso_data a b :=
dirprodpair (dirprodpair (z_iso_comp_left_weq f)
(z_iso_comp_right_weq (z_iso_inv_from_z_iso f)))
(z_iso_conjug_weq f).
Lemma folds_iso_data_prop : folds_iso_prop folds_iso_data_from_z_iso.
Proof.
repeat split; intros.
- simpl. apply logeqweq.
+ intro H. apply comp_compose2.
rewrite assoc. set (H2 := comp_compose2' H). rewrite H2.
apply idpath.
+ intro H. apply comp_compose2.
set (H2 := comp_compose2' H).
rewrite assoc in H2.
eapply post_comp_with_z_iso_is_inj.
apply (z_iso_is_inverse_in_precat f). apply H2.
- simpl. apply logeqweq.
+ intro H. apply comp_compose2.
apply pathsinv0. eapply pathscomp0.
× apply (pathsinv0 (comp_compose2' H)).
× transitivity ((f0 □ (f □ (inv_from_z_iso f))) □ g).
rewrite z_iso_inv_after_z_iso. rewrite id_right. apply idpath.
repeat rewrite assoc; apply idpath.
+ intro H. apply comp_compose2.
set (H2 := comp_compose2' H). apply pathsinv0.
eapply pathscomp0.
× apply (pathsinv0 H2).
× transitivity ((f0 □ (f □ (inv_from_z_iso f))) □ g).
repeat rewrite assoc; apply idpath.
rewrite z_iso_inv_after_z_iso. rewrite id_right. apply idpath.
- simpl. apply logeqweq.
+ intro H. apply comp_compose2.
rewrite <- assoc. rewrite (comp_compose2' H). apply idpath.
+ intro H. apply comp_compose2.
set (H2:= comp_compose2' H).
rewrite <- assoc in H2.
use (pre_comp_with_z_iso_inv_is_inj f). exact H2.
- simpl; apply logeqweq.
+ intro H; apply comp_compose2.
rewrite <- (comp_compose2' H).
transitivity
((f0 □ (f □ (inv_from_z_iso f))) □ (g □ f)).
× repeat rewrite assoc; apply idpath.
× rewrite z_iso_inv_after_z_iso. rewrite id_right; apply assoc.
+ intro H; apply comp_compose2.
set (H2 := comp_compose2' H).
repeat rewrite assoc in H2.
use pathscomp0.
× exact ((f0 □ (f □ (inv_from_z_iso f))) □ g).
× rewrite z_iso_inv_after_z_iso, id_right; apply idpath.
× repeat rewrite assoc.
use (post_comp_with_z_iso_is_inj f).
exact H2.
- simpl; apply logeqweq.
+ intro H. apply comp_compose2.
repeat rewrite assoc; rewrite assoc4.
rewrite (comp_compose2' H).
apply pathsinv0, assoc.
+ intro H; apply comp_compose2.
set (H2 := comp_compose2' H).
rewrite <- assoc in H2.
use (pre_comp_with_z_iso_inv_is_inj f).
use (post_comp_with_z_iso_is_inj f).
rewrite assoc. rewrite assoc in H2. rewrite assoc in H2.
use (pathscomp0 H2). rewrite <- assoc. apply idpath.
- simpl. apply logeqweq.
+ intro H; apply comp_compose2.
rewrite <- (comp_compose2' H); clear H.
repeat rewrite <- assoc. apply maponpaths. repeat rewrite assoc.
rewrite assoc4, z_iso_inv_after_z_iso, id_right.
apply idpath.
+ intro H; apply comp_compose2.
set (H':= comp_compose2' H); generalize H'; clear H' H; intro H.
repeat rewrite <- assoc in H.
use (pre_comp_with_z_iso_inv_is_inj f). use (pathscomp0 _ H).
rewrite (@assoc C' _ _ _ _ f). rewrite z_iso_inv_after_z_iso. rewrite id_left.
apply idpath.
- simpl; apply logeqweq.
+ intro H; set (H':=comp_compose2' H); clearbody H'; clear H;
rename H' into H; rewrite <- H; clear H.
apply comp_compose2.
repeat rewrite <- assoc; apply maponpaths; simpl.
set (H':=@assoc C' _ _ _ _ f0 g f); clearbody H';
simpl in ×. rewrite <- H'; clear H'.
apply maponpaths. simpl in ×.
repeat rewrite (@assoc C').
rewrite z_iso_inv_after_z_iso, id_left;
apply idpath.
+ intro H; set (H':=comp_compose2' H); clearbody H'; clear H;
rename H' into H.
apply comp_compose2.
repeat rewrite <- assoc in H.
use (post_comp_with_z_iso_is_inj f). use (pre_comp_with_z_iso_inv_is_inj f).
use (pathscomp0 _ H). rewrite (@assoc C' _ _ _ _ f). rewrite z_iso_inv_after_z_iso.
rewrite id_left. rewrite <- assoc. apply idpath.
- simpl. apply logeqweq.
+ intro H. apply id_identity2.
rewrite (id_identity2' H). rewrite (@id_left C').
apply (z_iso_after_z_iso_inv _ _ _ f).
+ intro H. apply id_identity2.
set (H':=id_identity2' H); clearbody H'; clear H.
set (H2:=z_iso_inv_to_left _ _ _ _ f _ _ H'); clearbody H2.
rewrite id_right in H2.
transitivity (f □ (inv_from_z_iso f)).
× apply (z_iso_inv_on_left C'), pathsinv0, H2.
× apply (z_iso_inv_after_z_iso C').
Qed.
Definition folds_iso_from_iso : folds_iso a b := tpair _ _ folds_iso_data_prop.
End from_iso_to_folds_iso.
Section from_folds_iso_to_iso.
Variables a b : C.
Variable i : folds_iso a b.
Let i': a ⇒ b := ϕ₁ i (id _ ).
Let i'inv : b ⇒ a := ϕ₂ i (id _ ).
Definition iso_from_folds_iso : z_iso (C:=C') a b.
Proof.
∃ i'.
∃ i'inv.
apply ϕ₁_ϕ₂_are_inverse.
Defined.
End from_folds_iso_to_iso.
Section iso_from_folds_from_iso.
Hypothesis (hs: has_homsets C').
Context {a b : C} (i : z_iso (C:=C') a b).
Lemma iso_from_folds_iso_folds_iso_from_iso : iso_from_folds_iso _ _ (folds_iso_from_iso _ _ i) = i.
Proof.
apply eq_z_iso. apply hs.
apply (@id_left C').
Qed.
Variable i' : folds_iso a b.
Lemma folds_iso_from_iso_iso_from_folds_iso : folds_iso_from_iso _ _ (iso_from_folds_iso _ _ i') = i'.
Proof.
apply folds_iso_equal.
apply (@id_left C').
Qed.
End iso_from_folds_from_iso.
End folds_iso_def.