Library UniMath.Folds.folds_isomorphism

Univalent FOLDS
Benedikt Ahrens, following notes by Michael Shulman
Contents of this file:

Definition of FOLDS precat isomorphisms

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 subtypePath.
- intro; apply isaprop_folds_iso_prop.
- assumption.
Qed.

the families of equivalences constituting a FOLDS isomorphism are given by composition

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.

A FOLDS isomorphism is determined by the first family of isos

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 subtypePath.
× 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 subtypePath.
× intro; apply isapropisweq.
× apply funextfun. unfold homot. apply ϕ₂_determined.
- apply subtypePath.
intro. apply isapropisweq.
apply funextfun. intro t.
apply ϕo_determined.
Qed.

Identity FOLDS isomorphism

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).

Inverse of a FOLDS isomorphism

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.

Composition of FOLDS isomorphisms

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.

From isomorphisms to FOLDS isomorphisms

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 :=
make_dirprod (make_dirprod (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.

from FOLDS isomorphism to isomorphism

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.

from FOLDS isos to isos and back, and the other way round

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.