Require Import UniMath.Foundations.PartA.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.PartA.
Require Import UniMath.MoreFoundations.Tactics.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.

Local Open Scope cat.

Definition idtoiso {C : precategory} {a b : ob C}:
      a = b -> z_iso a b.
Proof.
  intro H.
  induction H.
  exact (identity_z_iso a).
Defined.

Proposition idtoiso_idpath
            {C : category}
            (x : C)
  : pr1 (idtoiso (idpath x)) = identity x.
Proof.
  apply idpath.
Qed.

Definition is_univalent (C : category) :=
  ∏ (a b : ob C), isweq (fun p : a = b => idtoiso p).


Lemma eq_idtoiso_idtomor {C:precategory} (a b:ob C) (e:a = b) :
    pr1 (idtoiso e) = idtomor _ _ e.
Proof.
  destruct e; reflexivity.
Defined.

Lemma isaprop_is_univalent (C : category) : isaprop (is_univalent C).
Proof.
  apply impred.
  intro a.
  apply impred.
  intro b.
  apply isapropisweq.
Qed.

Definition univalent_category : UU := ∑ C : category, is_univalent C.

Definition make_univalent_category (C : category) (H : is_univalent C) : univalent_category
  := tpair _ C H.

Coercion univalent_category_to_category (C : univalent_category) : category := pr1 C.

Coercion univalent_category_has_homsets (C : univalent_category)
  : has_homsets C
  := pr2 (pr1 C).

Definition univalent_category_is_univalent (C : univalent_category) : is_univalent C := pr2 C.

Lemma univalent_category_has_groupoid_ob (C : univalent_category): isofhlevel 3 (ob C).
Proof.
  change (isofhlevel 3 C) with
        (∏ a b : C, isofhlevel 2 (a = b)).
  intros a b.
  apply (isofhlevelweqb _ (tpair _ _ (pr2 C a b))).
  apply isaset_z_iso.
Qed.

Definition isotoid (C : category) (H : is_univalent C) {a b : ob C}:
      z_iso a b -> a = b := invmap (make_weq _ (H a b)).

Lemma idtoiso_isotoid (C : category) (H : is_univalent C) (a b : ob C)
    (f : z_iso a b) : idtoiso (isotoid _ H f) = f.
Proof.
  unfold isotoid.
  set (Hw := homotweqinvweq (make_weq idtoiso (H a b))).
  simpl in Hw.
  apply Hw.
Qed.

Lemma isotoid_idtoiso (C : category) (H : is_univalent C) (a b : ob C)
    (p : a = b) : isotoid _ H (idtoiso p) = p.
Proof.
  unfold isotoid.
  set (Hw := homotinvweqweq (make_weq idtoiso (H a b))).
  simpl in Hw.
  apply Hw.
Qed.

Definition double_transport {C : precategory_ob_mor} {a a' b b' : ob C}
   (p : a = a') (q : b = b') (f : a --> b) : a' --> b' :=
  transportf (λ c, a' --> c) q (transportf (λ c, c --> b) p f).

Lemma double_transport_transpose
  {C : precategory_ob_mor}
  {a a' b b' : C} {f : a --> b} {g : a' --> b'}
  {px : a' = a} {py : b' = b}
  : double_transport px py g = f -> g = double_transport (!px) (!py) f.
Proof.
  intro H.
  destruct H.
  destruct px, py.
  reflexivity.
Qed.

Lemma double_transport_transpose'
  {C : precategory_ob_mor}
  {a a' b b' : C} {f : a' --> b'} {g : a --> b}
  {px : a' = a} {py : b' = b}
  : f = double_transport (!px) (!py) g -> double_transport px py f = g.
Proof.
  intro H.
  destruct (!H).
  destruct px, py.
  reflexivity.
Qed.

Lemma double_transport_compose
  {C : precategory}
  {a a' b b' c c' : C} {f : a --> b} {g : b --> c}
  {px : a = a'} {py : b = b'} {pz : c = c'}
  : double_transport px py f
  · double_transport py pz g =
  double_transport px pz (f · g).
Proof.
  unfold double_transport.
  destruct px, py, pz.
  reflexivity.
Qed.

Lemma idtoiso_postcompose (C : precategory) (a b b' : ob C)
  (p : b = b') (f : a --> b) :
      f · idtoiso p = transportf (λ b, a --> b) p f.
Proof.
  destruct p.
  apply id_right.
Qed.

Lemma idtoiso_postcompose_iso (C : category) (a b b' : ob C)
  (p : b = b') (f : z_iso a b) :
    z_iso_comp f (idtoiso p) = transportf (λ b, z_iso a b) p f.
Proof.
  destruct p.
  apply z_iso_eq.
  apply id_right.
Qed.

Lemma idtoiso_precompose (C : precategory) (a a' b : ob C)
  (p : a = a') (f : a --> b) :
      (idtoiso (!p)) · f = transportf (λ a, a --> b) p f.
Proof.
  destruct p.
  apply id_left.
Qed.

Lemma idtoiso_precompose_iso (C : category) (a a' b : ob C)
  (p : a = a') (f : z_iso a b) :
      z_iso_comp (idtoiso (!p)) f = transportf (λ a, z_iso a b) p f.
Proof.
  destruct p.
  apply z_iso_eq.
  apply id_left.
Qed.

Lemma double_transport_idtoiso (C : precategory) (a a' b b' : ob C)
  (p : a = a') (q : b = b') (f : a --> b) :
  double_transport p q f = inv_from_z_iso (idtoiso p) · f · idtoiso q.
Proof.
  destruct p.
  destruct q.
  intermediate_path (identity _ · f).
  - apply pathsinv0; apply id_left.
  - apply pathsinv0; apply id_right.
Defined.

Lemma idtoiso_inv (C : category) (a a' : ob C)
  (p : a = a') : idtoiso (!p) = z_iso_inv_from_z_iso (idtoiso p).
Proof.
  destruct p.
  simpl. apply z_iso_eq.
  apply idpath.
Defined.

Lemma idtoiso_concat (C : category) (a a' a'' : ob C)
  (p : a = a') (q : a' = a'') :
  idtoiso (p @ q) = z_iso_comp (idtoiso p) (idtoiso q).
Proof.
  destruct p.
  destruct q.
  apply z_iso_eq.
  simpl; apply pathsinv0, id_left.
Qed.

Definition pr1_idtoiso_concat
           {C : category}
           {x y z : C}
           (f : x = y) (g : y = z)
  : pr1 (idtoiso (f @ g)) = pr1 (idtoiso f) · pr1 (idtoiso g).
Proof.
  exact (maponpaths pr1 (idtoiso_concat _ _ _ _ f g)).
Qed.

Lemma idtoiso_inj (C : category) (H : is_univalent C) (a a' : ob C)
   (p p' : a = a') : idtoiso p = idtoiso p' -> p = p'.
Proof.
  apply invmaponpathsincl.
  apply isinclweq.
  apply H.
Qed.

Lemma isotoid_inj (C : category) (H : is_univalent C) (a a' : ob C)
   (f f' : z_iso a a') : isotoid _ H f = isotoid _ H f' -> f = f'.
Proof.
  apply invmaponpathsincl.
  apply isinclweq.
  apply isweqinvmap.
Qed.

Lemma isotoid_comp (C : category) (H : is_univalent C) (a b c : ob C)
  (e : z_iso a b) (f : z_iso b c) :
  isotoid _ H (z_iso_comp e f) = isotoid _ H e @ isotoid _ H f.
Proof.
  apply idtoiso_inj.
    assumption.
  rewrite idtoiso_concat.
  repeat rewrite idtoiso_isotoid.
  apply idpath.
Qed.

Lemma isotoid_identity_iso (C : category) (H : is_univalent C) (a : C) :
  isotoid _ H (identity_z_iso a) = idpath _ .
Proof.
  apply idtoiso_inj; try assumption.
  rewrite idtoiso_isotoid;
  apply idpath.
Qed.

Lemma inv_isotoid (C : category) (H : is_univalent C) (a b : C)
    (f : z_iso a b) : ! isotoid _ H f = isotoid _ H (z_iso_inv_from_z_iso f).
Proof.
  apply idtoiso_inj; try assumption.
  rewrite idtoiso_isotoid.
  rewrite idtoiso_inv.
  rewrite idtoiso_isotoid.
  apply idpath.
Qed.

Lemma transportf_isotoid (C : category) (H : is_univalent C)
   (a a' b : ob C) (p : z_iso a a') (f : a --> b) :
 transportf (λ a0 : C, a0 --> b) (isotoid C H p) f = inv_from_z_iso p · f.
Proof.
  rewrite <- idtoiso_precompose.
  rewrite idtoiso_inv.
  rewrite idtoiso_isotoid.
  apply idpath.
Qed.

Lemma transportf_isotoid' (C : category) (H : is_univalent C)
   (a b b' : ob C) (p : z_iso b b') (f : a --> b) :
 transportf (λ a0 : C, a --> a0) (isotoid C H p) f = f · p.
Proof.
  rewrite <- idtoiso_postcompose.
  apply maponpaths.
  rewrite idtoiso_isotoid.
  apply idpath.
Qed.

Lemma transportb_isotoid (C : category) (H : is_univalent C)
  (a b b' : ob C) (p : z_iso b b') (f : a --> b') :
  transportb (λ b0 : C, a --> b0) (isotoid C H p) f = f · inv_from_z_iso p.
Proof.
  apply pathsinv0.
  apply transportb_transpose_right.
  change (precategory_morphisms a) with (λ b0 : C, a --> b0).
  rewrite transportf_isotoid'.
  rewrite <- assoc.
  rewrite z_iso_after_z_iso_inv.
  apply id_right.
Qed.

Lemma transportf_isotoid_dep (C : precategory)
   (a a' : C) (p : a = a') (f : ∏ c, a --> c) :
 transportf (λ x : C, ∏ c, x --> c) p f = λ c, idtoiso (!p) · f c.
Proof.
  destruct p.
  simpl.
  apply funextsec.
  intro.
  rewrite id_left.
  apply idpath.
Qed.

Lemma forall_isotoid (A : category) (a_is : is_univalent A)
      (a a' : A) (P : z_iso a a' -> UU) :
  (∏ e, P (idtoiso e)) → ∏ i, P i.
Proof.
  intros H i.
  rewrite <- (idtoiso_isotoid _ a_is).
  apply H.
Defined.

Lemma transportf_isotoid_dep' (J : UU) (C : precategory) (F : J -> C)
  (a a' : C) (p : a = a') (f : ∏ c, a --> F c) :
  transportf (λ x : C, ∏ c, x --> F c) p f = λ c, idtoiso (!p) · f c.
Proof.
  now destruct p; apply funextsec; intro x; rewrite id_left.
Defined.

 Lemma transportf_isotoid_dep'' (J : UU) (C : precategory) (F : J -> C)
   (a a' : C) (p : a = a') (f : ∏ c, F c --> a) :
   transportf (λ x : C, ∏ c, F c --> x) p f = λ c, f c · idtoiso p.
Proof.
  now destruct p; apply funextsec; intro x; rewrite id_right.
Defined.