Library HoTT.Pointed.pEquiv

Require Import Basics.
Require Import Types.
Require Import WildCat.
Require Import Pointed.Core.

Local Open Scope pointed_scope.

(* Pointed equivalence is a reflexive relation. *)
Global Instance pequiv_reflexive : Reflexive pEquiv.
Proof.
  intro; apply pequiv_pmap_idmap.
Defined.

(* We can probably get rid of the following notation, and use ^-1*)
Notation "f ^-1*" := (@cate_inv pType _ _ _ _ hasequivs_ptype _ _ f) : pointed_scope.

(* Pointed equivalence is a symmetric relation. *)
Global Instance pequiv_symmetric : Symmetric pEquiv.
Proof.
  intros ? ?; apply pequiv_inverse.
Defined.

(* Pointed equivalences compose. *)
Definition pequiv_compose {A B C : pType} (f : A <~>* B) (g : B <~>* C)
  : A <~>* C
  := g $oE f.

(* Pointed equivalence is a transitive relation. *)
Global Instance pequiv_transitive : Transitive pEquiv.
Proof.
  intros ? ? ?; apply pequiv_compose.
Defined.

Notation "g o*E f" := (pequiv_compose f g) : pointed_scope.

(* Sometimes we wish to construct a pEquiv from an equiv and a proof that it is pointed. *)
Definition Build_pEquiv' {A B : pType} (f : A <~> B)
  (p : f (point A) = point B)
  : A <~>* B := Build_pEquiv _ _ (Build_pMap _ _ f p) _.

Arguments Build_pEquiv' & _ _ _ _.

(* A version of equiv_adjointify for pointed equivalences where all data is pointed. There is a lot of unnecessary data here but sometimes it is easier to prove equivalences using this. *)
Definition pequiv_adjointify {A B : pType} (f : A ->* B) (f' : B ->* A)
  (r : f o× f' ==* pmap_idmap) (s : f' o× f == pmap_idmap) : A <~>* B
  := (Build_pEquiv _ _ f (isequiv_adjointify f f' r s)).

(* In some situations you want the back and forth maps to be pointed but not the sections. *)
Definition pequiv_adjointify' {A B : pType} (f : A ->* B) (f' : B ->* A)
  (r : f o f' == idmap) (s : f' o f == idmap) : A <~>* B
  := (Build_pEquiv _ _ f (isequiv_adjointify f f' r s)).

Pointed versions of moveR_equiv_M and friends.
Definition moveR_pequiv_Mf {A B C} (f : B <~>* C) (g : A ->* B) (h : A ->* C)
           (p : g ==* f^-1* o× h)
  : (f o× g ==* h).
Proof.
  refine (pmap_postwhisker f p @* _).
  refine ((pmap_compose_assoc _ _ _)^* @* _).
  refine (pmap_prewhisker h (peisretr f) @* _).
  apply pmap_postcompose_idmap.
Defined.

Definition moveL_pequiv_Mf {A B C} (f : B <~>* C) (g : A ->* B) (h : A ->* C)
           (p : f^-1* o× h ==* g)
  : (h ==* f o× g).
Proof.
  refine (_ @* pmap_postwhisker f p).
  refine (_ @* (pmap_compose_assoc _ _ _)).
  refine ((pmap_postcompose_idmap _)^* @* _).
  apply pmap_prewhisker.
  symmetry; apply peisretr.
Defined.

Definition moveL_pequiv_Vf {A B C} (f : B <~>* C) (g : A ->* B) (h : A ->* C)
           (p : f o× g ==* h)
  : g ==* f^-1* o× h.
Proof.
  refine (_ @* pmap_postwhisker f^-1* p).
  refine (_ @* (pmap_compose_assoc _ _ _)).
  refine ((pmap_postcompose_idmap _)^* @* _).
  apply pmap_prewhisker.
  symmetry; apply peissect.
Defined.

Definition moveR_pequiv_Vf {A B C} (f : B <~>* C) (g : A ->* B) (h : A ->* C)
           (p : h ==* f o× g)
   : f^-1* o× h ==* g.
Proof.
  refine (pmap_postwhisker f^-1* p @* _).
  refine ((pmap_compose_assoc _ _ _)^* @* _).
  refine (pmap_prewhisker g (peissect f) @* _).
  apply pmap_postcompose_idmap.
Defined.

Definition moveR_pequiv_fV {A B C} (f : B ->* C) (g : A <~>* B) (h : A ->* C)
           (p : f o× g ==* h)
  : (f ==* h o× g^-1*).
Proof.
  refine (_ @* pmap_prewhisker g^-1* p).
  refine (_ @* (pmap_compose_assoc _ _ _)^*).
  refine ((pmap_precompose_idmap _)^* @* _).
  apply pmap_postwhisker.
  symmetry; apply peisretr.
Defined.

Definition pequiv_pequiv_precompose `{Funext} {A B C : pType} (f : A <~>* B)
  : (B ->** C) <~>* (A ->** C).
Proof.
  srapply Build_pEquiv'.
  - exact (equiv_precompose_cat_equiv f).
  - (* By using pelim f, we can avoid Funext in this part of the proof. *)
    cbn; unfold "o*", point_pforall; cbn.
    by pelim f.
Defined.

Definition pequiv_pequiv_postcompose `{Funext} {A B C : pType} (f : B <~>* C)
  : (A ->** B) <~>* (A ->** C).
Proof.
  srapply Build_pEquiv'.
  - exact (equiv_postcompose_cat_equiv f).
  - cbn; unfold "o*", point_pforall; cbn.
    by pelim f.
Defined.

Proposition equiv_pequiv_inverse `{Funext} {A B : pType}
  : (A <~>* B) <~> (B <~>* A).
Proof.
  refine (issig_pequiv' _ _ oE _ oE (issig_pequiv' A B)^-1).
  srapply (equiv_functor_sigma' (equiv_equiv_inverse _ _)); intro e; cbn.
  exact (equiv_moveR_equiv_V _ _ oE equiv_path_inverse _ _).
Defined.