# Library UniMath.Bicategories.WkCatEnrichment.internal_equivalence

Require Import UniMath.Foundations.PartD.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.ProductCategory.
Require Import UniMath.CategoryTheory.HorizontalComposition.
Require Import UniMath.CategoryTheory.Equivalences.Core.

Require Import UniMath.Bicategories.WkCatEnrichment.prebicategory.
Require Import UniMath.Bicategories.WkCatEnrichment.whiskering.
Require Import UniMath.Bicategories.WkCatEnrichment.Notations.

Definition inv {C:precategory} {a b : C}
(f : iso a b)
:= iso_inv_from_iso f.

Definition is_int_equivalence {C : prebicategory} {a b : C}
(f : a -1-> b) : UU
:= g : b -1-> a,
(iso (identity1 a) (f ;1; g)) ×
(iso (g ;1; f) (identity1 b)).

Definition int_equivalence {C : prebicategory} (a b : C) : UU
:= f : a -1-> b, is_int_equivalence f.

Definition identity_int_equivalence {C : prebicategory} (a : C)
: int_equivalence a a.
Proof.
(identity1 a).
(identity1 a).
split.
- exact (inv (left_unitor (identity1 a))).
- exact (left_unitor (identity1 a)).
Defined.

Definition id_to_int_equivalence {C : prebicategory} (a b : C)
: (a = b) int_equivalence a b.
Proof.
intros p.
induction p.
exact (identity_int_equivalence a).
Defined.

Definition is_adj_int_equivalence {C : prebicategory} { a b : C }
(f : a -1-> b)
:= (g : b -1-> a)
(etaeps : (iso (identity1 a) (f ;1; g)) ×
(iso (g ;1; f) (identity1 b))),
let eta := pr1 etaeps in
let eps := pr2 etaeps in
(
(inv (left_unitor f))
;v; (whisker_right eta f)
;v; (inv (associator _ _ _))
;v; (whisker_left f eps)
;v; (right_unitor _)
= (identity f)
) × (
(inv (right_unitor g))
;v; (whisker_left g eta)
;v; (associator _ _ _)
;v; (whisker_right eps g)
;v; (left_unitor _) = (identity g)
).

Definition adj_int_equivalence {C : prebicategory} (a b : C) : UU
:= f : a -1-> b, is_adj_int_equivalence f.

Local Definition identity_triangle1 {C : prebicategory} (a : C)
: (inv (left_unitor (identity1 a)))
;v; (whisker_right (inv (left_unitor (identity1 a))) (identity1 a))
;v; (inv (associator _ _ _))
;v; (whisker_left (identity1 a) (right_unitor (identity1 a)))
;v; (right_unitor _)
= identity (identity1 a).
Proof.
apply iso_inv_to_right.
rewrite id_left.
rewrite <- !assoc.
apply iso_inv_on_right.

intermediate_path (identity (identity1 a ;1; identity1 a)).
rewrite whisker_right_inv.
apply iso_inv_on_right.
apply iso_inv_on_right.
rewrite id_right.
simpl.
unfold whisker_left.
unfold whisker_right.
rewrite <- left_unitor_id_is_right_unitor_id.
rewrite (triangle_axiom (identity1 a) (identity1 a)).
rewrite <- left_unitor_id_is_right_unitor_id.
reflexivity.

simpl.
apply pathsinv0.
rewrite left_unitor_id_is_right_unitor_id.

apply (iso_inv_after_iso (right_unitor _)).
Defined.

Local Definition identity_triangle2 {C : prebicategory}
(a : C) :
(inv (right_unitor (identity1 a)))
;v; (whisker_left (identity1 a) (inv (left_unitor (identity1 a))))
;v; (associator _ _ _)
;v; (whisker_right (right_unitor (identity1 a)) (identity1 a))
;v; (left_unitor _)
= (identity (identity1 a)).
Proof.
rewrite <- (assoc _ _ (whisker_right _ _)).
unfold whisker_right at 1.
simpl.
rewrite <- triangle_axiom.
fold (whisker_left (identity1 a) (left_unitor_2mor (identity1 a))).
rewrite <- (assoc _ _ (whisker_left _ _)).
rewrite <- whisker_left_on_comp.

set (W := iso_after_iso_inv (left_unitor (identity1 a))).
simpl in W.
rewrite W.
clear W.

fold (identity (identity1 a)).
rewrite whisker_left_id_2mor.
rewrite id_right.

rewrite left_unitor_id_is_right_unitor_id.

set (W := iso_after_iso_inv (right_unitor (identity1 a))).
simpl in W.
rewrite W.
reflexivity.
Defined.

Definition identity_adj_int_equivalence {C : prebicategory}
(a : C) : adj_int_equivalence a a.
Proof.
(identity1 a).
(identity1 a).
use tpair.
- (inv (left_unitor (identity1 a))).
exact (right_unitor (identity1 a)).
- split.
+ apply identity_triangle1.
+ apply identity_triangle2.
Defined.

Definition path_to_adj_int_equivalence {C : prebicategory}
(a b : C) :
a = b adj_int_equivalence a b.
Proof.
intros p.
induction p.
exact (identity_adj_int_equivalence a).
Defined.