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.
Show proof.

Proposition idtoiso_idpath
            {C : category}
            (x : C)
  : pr1 (idtoiso (idpath x)) = identity x.
Show proof.

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.
Show proof.

Lemma isaprop_is_univalent (C : category) : isaprop (is_univalent C).
Show proof.

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

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.
Show proof.

Lemma isotoid_idtoiso (C : category) (H : is_univalent C) (a b : ob C)
    (p : a = b) : isotoid _ H (idtoiso p) = p.
Show proof.

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.
Show proof.

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.
Show proof.

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

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.
Show proof.

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.
Show proof.

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.
Show proof.

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.
Show proof.

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.
Show proof.

Lemma idtoiso_inv (C : category) (a a' : ob C)
  (p : a = a') : idtoiso (!p) = z_iso_inv_from_z_iso (idtoiso p).
Show proof.

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

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

Lemma idtoiso_inj (C : category) (H : is_univalent C) (a a' : ob C)
   (p p' : a = a') : idtoiso p = idtoiso p' -> p = p'.
Show proof.

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'.
Show proof.

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.
Show proof.

Lemma isotoid_identity_iso (C : category) (H : is_univalent C) (a : C) :
  isotoid _ H (identity_z_iso a) = idpath _ .
Show proof.

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

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.
Show proof.

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.
Show proof.

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.
Show proof.

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.
Show proof.

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.
Show proof.

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.
Show proof.

 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.
Show proof.