SkySkimmer/bug.v

## bug.v
(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-noinit" "-indices-matter" "-type-in-type" "-w" "-notation-overridden" "-w" "-deprecated-native-compiler-option" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/UniMath/UniMath" "UniMath" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "UniMath.CategoryTheory.LeftKanExtension" "-native-compiler" "no") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 688 lines to 71 lines, then from 84 lines to 800 lines, then from 799 lines to 123 lines, then from 136 lines to 646 lines, then from 650 lines to 171 lines, then from 184 lines to 570 lines, then from 572 lines to 204 lines, then from 217 lines to 880 lines, then from 884 lines to 284 lines, then from 297 lines to 626 lines, then from 630 lines to 328 lines, then from 341 lines to 1806 lines, then from 1797 lines to 365 lines, then from 375 lines to 363 lines, then from 376 lines to 1153 lines, then from 1151 lines to 410 lines, then from 423 lines to 1670 lines, then from 1650 lines to 487 lines, then from 500 lines to 828 lines, then from 833 lines to 504 lines, then from 517 lines to 1523 lines, then from 1515 lines to 1015 lines *)
(* coqc version 8.18+alpha compiled with OCaml 4.13.1
   coqtop version buildkitsandbox:/home/coq/.opam/4.13.1+flambda/.opam-switch/build/coq-core.dev/_build/default,master (284b7133ff792dab82c658a274db0c5e0a04d2d5)
   Expected coqc runtime on this file: 9.261 sec *)
Require Coq.Init.Logic.
Require Coq.Init.Ltac.
Require Coq.Init.Notations.
Require UniMath.Foundations.Init.
Require UniMath.Foundations.Preamble.
Require UniMath.Foundations.PartA.
Require UniMath.Foundations.PartB.
Require UniMath.Foundations.UnivalenceAxiom.
Require UniMath.Foundations.PartC.
Require UniMath.Foundations.PartD.
Require UniMath.Foundations.Propositions.
Require UniMath.Foundations.UnivalenceAxiom2.
Require UniMath.Foundations.HLevels.
Require UniMath.Foundations.Sets.
Require UniMath.Foundations.NaturalNumbers.
Require UniMath.Foundations.All.
Require UniMath.MoreFoundations.Notations.
Require UniMath.MoreFoundations.Tactics.
Require UniMath.MoreFoundations.PartA.
Require UniMath.CategoryTheory.Core.Categories.

Declare ML Module "coq-core.plugins.ltac".
Module Export AdmitTactic.
Module Import LocalFalse.
Inductive False : Prop := .
End LocalFalse.
Axiom proof_admitted : False.
Global Set Default Proof Mode "Classic".
Tactic Notation "admit" := abstract case proof_admitted.
End AdmitTactic.

Module UniMath_DOT_CategoryTheory_DOT_Core_DOT_Isos_WRAPPED.
Module Isos.


Import UniMath.Foundations.PartA.
Import UniMath.Foundations.Propositions.
Import UniMath.Foundations.Sets.
Import UniMath.MoreFoundations.Tactics.
Import UniMath.CategoryTheory.Core.Categories.

Local Open Scope cat.


Definition precomp_with {C : precategory_data} {a b : C} (f : a --> b) {c : C} (g : b --> c): a --> c :=
   f · g.

Definition is_iso {C : precategory_data} {a b : C} (f : a --> b) :=
  ∏ c, isweq (precomp_with f (c:=c)).

Lemma isaprop_is_iso {C : precategory_data} (a b : C) (f : a --> b) : isaprop (is_iso f).
Admitted.

Definition iso {C: precategory_data} (a b : C) := ∑ f : a --> b, is_iso f.
Definition morphism_from_iso {C : precategory_data} {a b : C} (f : iso a b) : a --> b := pr1 f.
Coercion morphism_from_iso : iso >-> precategory_morphisms.

Definition make_iso {C : precategory_data} {a b : C} (f : a --> b) (fiso: is_iso f) : iso a b := (f,,fiso).

Definition inv_from_iso {C : precategory_data} {a b : C} (f : iso a b) : b --> a :=
   invmap (make_weq (precomp_with f) (pr2 f a)) (identity _ ).

Definition iso_inv_after_iso {C : precategory_data} {a b : C} (f: iso a b) :
   f · inv_from_iso f = identity _ .
Admitted.

Definition iso_after_iso_inv {C : precategory} {a b : C} (f : iso a b) :
  inv_from_iso f · f = identity _ .
Admitted.

Definition is_iso_inv_from_iso {C : precategory} {a b : C} (f : iso a b) : is_iso (inv_from_iso f).
Admitted.

Definition iso_inv_from_iso {C : precategory} {a b : C} (f : iso a b) : iso b a :=
  tpair _ _ (is_iso_inv_from_iso f).

Lemma eq_iso {C: precategory_data} {a b : C} (f g : iso a b) : pr1 f = pr1 g -> f = g.
Admitted.

Lemma isaset_iso {C : precategory_data} (hs : has_homsets C) (a b : ob C) :
  isaset (iso a b).
Admitted.

Lemma identity_is_iso (C : precategory) (a : ob C) : is_iso (identity a).
Admitted.

Definition identity_iso {C : precategory} (a : ob C) :
   iso a a := tpair _ _ (identity_is_iso C a).

Lemma iso_inv_on_right {C : precategory} (a b c : ob C)
  (f : iso a  b) (g : b --> c) (h : a --> c) (H : h = f · g) :
     inv_from_iso f · h = g.
Admitted.

Lemma iso_inv_on_left {C : precategory} (a b c : ob C)
  (f : a --> b) (g : iso b c) (h : a --> c) (H : h = f · g) :
     f = h · inv_from_iso g.
Admitted.

Lemma iso_inv_to_left {C : precategory} (a b c : ob C)
  (f : iso a  b) (g : b --> c) (h : a --> c) :
    inv_from_iso f · h = g -> h = f · g.
Admitted.

Lemma iso_inv_to_right {C : precategory} (a b c : ob C)
  (f : a --> b) (g : iso b c) (h : a --> c) :
     f = h · inv_from_iso g -> f · g = h.
Admitted.


Definition isweqhomot' {X Y} (f g : X -> Y) (H : isweq f)
      (homot : ∏ x, f x = g x) : isweq g.
Admitted.

Lemma is_iso_comp_of_isos {C : precategory} {a b c : ob C}
  (f : iso a b) (g : iso b c) : is_iso (f · g).
Admitted.

Lemma is_iso_comp_of_is_isos {C : precategory} {a b c : ob C}
      (f : a --> b) (g : b --> c) (H1 : is_iso f) (H2 : is_iso g) : is_iso (f · g).
Admitted.

Definition iso_comp {C : precategory} {a b c : ob C}
  (f : iso a b) (g : iso b c) : iso a c.
Admitted.

Lemma inv_iso_unique (C : precategory) (a b : C) (f : iso a b) (g : iso b a) :
  precomp_with f g = identity _ -> g = iso_inv_from_iso f.
Admitted.

Lemma inv_iso_unique' (C : precategory) (a b : C) (f : iso a b) (g : b --> a) :
  precomp_with f g = identity _ -> g = inv_from_iso f.
Admitted.

Lemma iso_inv_of_iso_comp (C : precategory) (a b c : ob C)
   (f : iso a b) (g : iso b c) :
   iso_inv_from_iso (iso_comp f g) = iso_comp (iso_inv_from_iso g) (iso_inv_from_iso f).
Admitted.

Lemma iso_inv_of_iso_id {C : precategory} (a : ob C) :
   iso_inv_from_iso (identity_iso a) = identity_iso a.
Admitted.

Lemma iso_inv_iso_inv {C : precategory} (a b : ob C) (f : iso a b) :
     iso_inv_from_iso (iso_inv_from_iso f) = f.
Admitted.

Lemma pre_comp_with_iso_is_inj {C : precategory_data} (a b c : ob C)
    (f : a --> b) (H : is_iso f) (g h : b --> c) : f · g = f · h -> g = h.
Admitted.

Lemma cancel_precomposition_iso {C : precategory_data} {a b c : C}
    (f : iso a b) (g h : b --> c) : f · g = f · h -> g = h.
Admitted.

Lemma post_comp_with_iso_is_inj {C : precategory} (b c : ob C)
     (h : b --> c) (H : is_iso h)
   (a : ob C) (f g : a --> b) : f · h = g · h -> f = g.
Admitted.

Lemma cancel_postcomposition_iso {C : precategory} {a b c : C}
    (h : iso b c) (f g : a --> b) : f · h = g · h -> f = g.
Admitted.

Lemma iso_comp_right_isweq {C : precategory_data} {a b : ob C} (h : iso a b) (c : C) :
  isweq (fun f : b --> c => h · f).
Admitted.

Lemma iso_comp_left_isweq {C : precategory} {a b : ob C} (h : iso a b) (c : C) :
  isweq (fun f : c --> a => f · h).
Admitted.

Definition postcomp_with {C : precategory_data} {b c : C} (h : b --> c) {a : C}
  (f : a --> b) : a --> c := f · h.

Definition is_iso' {C : precategory} {b c : C} (f : b --> c) :=
  ∏ a, isweq (postcomp_with f (a:=a)).

Definition is_inverse_in_precat {C : precategory_data} {a b : C}
  (f : a --> b) (g : b --> a) :=
          (f · g = identity a) ×
          (g · f = identity b).

Definition is_inverse_in_precat1 {C : precategory_data} {a b : C} {f : a --> b} {g : b --> a}
           (H : is_inverse_in_precat f g) :
  f · g = identity a := dirprod_pr1 H.

Definition is_inverse_in_precat2 {C : precategory_data} {a b : C} {f : a --> b} {g : b --> a}
           (H : is_inverse_in_precat f g) :
  g · f = identity b := dirprod_pr2 H.

Definition is_inverse_in_precat_inv {C : precategory_data} {a b : C} {f : a --> b} {g : b --> a}
           (H : is_inverse_in_precat f g) : is_inverse_in_precat g f :=
  make_dirprod (is_inverse_in_precat2 H) (is_inverse_in_precat1 H).

Definition is_inverse_in_precat_comp {C : precategory} {a b c : C} {f1 : a --> b} {f2 : b --> c}
           {g1 : b --> a} {g2 : c --> b} (H1 : is_inverse_in_precat f1 g1)
           (H2 : is_inverse_in_precat f2 g2) : is_inverse_in_precat (f1 · f2) (g2 · g1).
Admitted.

Definition is_inverse_in_precat_identity {C : precategory} (c : C) :
  is_inverse_in_precat (identity c) (identity c).
Admitted.

Definition is_iso_qinv {C:precategory} {a b : C} (f : a --> b) (g : b --> a) :
  is_inverse_in_precat f g -> is_iso f.
Admitted.


Section are_isomorphic.

  Context {C : precategory}.


  Definition are_isomorphic : hrel C := λ a b, ∥iso a b∥.

  Lemma iseqrel_are_isomorphic : iseqrel are_isomorphic.
Admitted.

End are_isomorphic.


Lemma isaprop_is_inverse_in_precat {C : category} (a b : ob C)
   (f : a --> b) (g : b --> a) : isaprop (is_inverse_in_precat f g).
Admitted.

Lemma inverse_unique_precat {C : precategory} (a b : ob C)
   (f : a --> b) (g g': b --> a) (H : is_inverse_in_precat f g)
    (H' : is_inverse_in_precat f g') : g = g'.
Admitted.

Definition is_z_isomorphism {C : precategory_data} {a b : ob C}
           (f : a --> b) := ∑ g, is_inverse_in_precat f g.

Definition make_is_z_isomorphism {C : precategory_data} {a b : C} (f : a --> b)
           (g : b --> a) (H : is_inverse_in_precat f g) : is_z_isomorphism f := (g,,H).

Definition is_z_isomorphism_mor {C : precategory_data} {a b : C} {f : a --> b}
           (I : is_z_isomorphism f) : b --> a := pr1 I.

Definition is_z_isomorphism_is_inverse_in_precat {C : precategory_data} {a b : C}
           {f : a --> b} (I : is_z_isomorphism f) :
  is_inverse_in_precat f (is_z_isomorphism_mor I) := pr2 I.
Coercion is_z_isomorphism_is_inverse_in_precat : is_z_isomorphism >-> is_inverse_in_precat.

Definition is_z_isomorphism_inv {C : precategory_data} {a b : C} {f : a --> b}
           (I : is_z_isomorphism f) : is_z_isomorphism (is_z_isomorphism_mor I).
Admitted.

Definition is_z_isomorphism_comp {C : precategory} {a b c : C} {f1 : a --> b} {f2 : b --> c}
           (H1 : is_z_isomorphism f1) (H2 : is_z_isomorphism f2) :
  is_z_isomorphism (f1 · f2).
Admitted.

Definition is_z_isomorphism_identity {C : precategory} (c : C) : is_z_isomorphism (identity c).
Admitted.

Lemma isaprop_is_z_isomorphism {C : category} {a b : ob C}
     (f : a --> b) : isaprop (is_z_isomorphism f).
Admitted.

Lemma is_z_isomorphism_mor_eq {C : precategory} {a b : C} {f g : a --> b}
      (e : f = g) (I1 : is_z_isomorphism f) (I2 : is_z_isomorphism g) :
  is_z_isomorphism_mor I1 = is_z_isomorphism_mor I2.
Admitted.

Definition z_iso {C : precategory_data} (a b : ob C) := ∑ f : a --> b, is_z_isomorphism f.

Definition make_z_iso {C : precategory_data} {a b : C} (f : a --> b) (g : b --> a)
  (H : is_inverse_in_precat f g) : z_iso a b := (f,,make_is_z_isomorphism f g H).

Definition z_iso_mor {C : precategory_data} {a b : ob C} (f : z_iso a b) : a --> b := pr1 f.
Coercion z_iso_mor : z_iso >-> precategory_morphisms.

Definition inv_from_z_iso {C : precategory_data} {a b : C} (i : z_iso a b) : b --> a :=
  is_z_isomorphism_mor (pr2 i).

Definition z_iso_is_inverse_in_precat {C : precategory_data} {a b : C} (i : z_iso a b) :
  is_inverse_in_precat i (inv_from_z_iso i) := pr2 i.
Coercion z_iso_is_inverse_in_precat : z_iso >-> is_inverse_in_precat.

Definition z_iso_inv {C : precategory_data} {a b : C} (I : z_iso a b) : z_iso b a.
Admitted.

Definition z_iso_comp {C : precategory} {a b c : C} (I1 : z_iso a b) (I2 : z_iso b c) :
  z_iso a c.
Admitted.

Lemma is_z_iso_comp_of_is_z_isos {C : precategory} {a b c : ob C}
      (f : a --> b) (g : b --> c) (H1 : is_z_isomorphism f) (H2 : is_z_isomorphism g) : is_z_isomorphism (f · g).
Admitted.


Definition z_iso_is_z_isomorphism {C : precategory_data} {a b : C} (I : z_iso a b) :
  is_z_isomorphism I.
Admitted.

Definition is_z_iso_inv_from_z_iso {C : precategory_data} {a b : C} (I : z_iso a b) :
  is_z_isomorphism (inv_from_z_iso I).
Admitted.

Lemma post_comp_with_z_iso_is_inj {C : precategory} {a' a b : C} {f : a --> b} {g : b --> a}
      (i : is_inverse_in_precat f g) : ∏ (f' g' : a' --> a), f' · f = g' · f -> f' = g'.
Admitted.

Lemma post_comp_with_z_iso_inv_is_inj {C : precategory} {a b b' : C} {f : a --> b} {g : b --> a}
      (i : is_inverse_in_precat f g) : ∏ (f' g' : b' --> b), f' · g = g' · g -> f' = g'.
Admitted.

Lemma pre_comp_with_z_iso_is_inj {C : precategory} {a b b' : C} {f : a --> b} {g : b --> a}
      (i : is_inverse_in_precat f g) : ∏ (f' g' : b --> b'), f · f' = f · g' -> f' = g'.
Admitted.

Lemma cancel_precomposition_z_iso {C : precategory} {a b c : C}
    (f : z_iso a b) (g h : b --> c) : f · g = f · h -> g = h.
Admitted.

Lemma pre_comp_with_z_iso_is_inj' {C : precategory} {a b b' : C} {f : a --> b}
      (i : is_z_isomorphism f) : ∏ (f' g' : b --> b'), f · f' = f · g' -> f' = g'.
Admitted.

Lemma pre_comp_with_z_iso_inv_is_inj {C : precategory} {a' a b : C} {f : a --> b} {g : b --> a}
      (i : is_inverse_in_precat f g) : ∏ (f' g' : a --> a'), g · f' = g · g' -> f' = g'.
Admitted.

Lemma z_iso_eq {C : category} {a b : C} (i i' : z_iso a b) (e : z_iso_mor i = z_iso_mor i') :
  i = i'.
Admitted.

Lemma z_iso_eq_inv {C : category} {a b : C} (i i' : z_iso a b)
      (e2 : inv_from_z_iso i = inv_from_z_iso i') : i = i'.
Admitted.

Definition morphism_from_z_iso {C : precategory_data} (a b : ob C)
   (f : z_iso a b) : a --> b := pr1 f.
Coercion morphism_from_z_iso : z_iso >-> precategory_morphisms.

Lemma isaset_z_iso {C : category} (a b : ob C) : isaset (z_iso a b).
Admitted.

Lemma identity_is_z_iso {C : precategory} (a : ob C) :
    is_z_isomorphism (identity a).
Admitted.

Definition identity_z_iso {C : precategory} (a : ob C) :
   z_iso a a := tpair _ _ (identity_is_z_iso a).

Definition z_iso_inv_from_z_iso {C : precategory_data} {a b : ob C}
  (f : z_iso a b) : z_iso b a.
Admitted.

Definition z_iso_inv_after_z_iso {C : precategory_data} {a b : ob C}
   (f : z_iso a b) : f · inv_from_z_iso f = identity _ :=
      pr1 (pr2 (pr2 f)).

Definition z_iso_after_z_iso_inv {C : precategory_data} {a b : ob C}
   (f : z_iso a b) : inv_from_z_iso f · f = identity _ :=
      pr2 (pr2 (pr2 f)).

Lemma z_iso_inv_on_right {C : precategory} (a b c : ob C)
  (f : z_iso a  b) (g : b --> c) (h : a --> c) (H : h = f · g) :
     inv_from_z_iso f · h = g.
Admitted.

Lemma z_iso_inv_on_left {C : precategory} (a b c : ob C)
  (f : a --> b) (g : z_iso b c) (h : a --> c) (H : h = f · g) :
     f = h · inv_from_z_iso g.
Admitted.

Lemma z_iso_inv_to_left {C : precategory} (a b c : ob C)
  (f : z_iso a  b) (g : b --> c) (h : a --> c) :
    inv_from_z_iso f · h = g -> h = f · g.
Admitted.

Lemma z_iso_inv_to_right {C : precategory} (a b c : ob C)
  (f : a --> b) (g : z_iso b c) (h : a --> c) :
     f = h · inv_from_z_iso g -> f · g = h.
Admitted.

Lemma wrap_inverse {M : precategory} {x y : M} (g : x --> x) (f : z_iso x y) :
  g = identity x -> z_iso_inv f · g · f = identity y.
Admitted.

Lemma wrap_inverse' {M : precategory} {x y : M} (g : x --> x) (f : z_iso y x) :
  g = identity x -> f · g · z_iso_inv f = identity y.
Admitted.

Lemma cancel_z_iso {M : precategory} {x y z : M} (f f' : x --> y) (g : z_iso y z) :
  f · g = f' · g -> f = f'.
Admitted.

Lemma cancel_z_iso' {M : precategory} {w x y : M} (g : z_iso w x) (f f' : x --> y) :
  g · f = g · f' -> f = f'.
Admitted.

Definition are_z_isomorphic {C : precategory_data} : hrel C := λ a b, ∥z_iso a b∥.

Lemma iseqrel_are_z_isomorphic {C : precategory} : iseqrel (are_z_isomorphic(C:=C)).
Admitted.


Lemma are_inverse_comp_of_inverses {C : precategory} (a b c : C)
     (f : z_iso a b) (g : z_iso b c) :
  is_inverse_in_precat (f · g) (inv_from_z_iso g · inv_from_z_iso f).
Admitted.

Lemma inv_z_iso_unique {C : category} (a b : ob C)
  (f : z_iso a b) (g : z_iso b a) :
  is_inverse_in_precat f g -> g = z_iso_inv_from_z_iso f.
Admitted.

Lemma inv_z_iso_unique' (C : precategory) (a b : C) (f : z_iso a b) (g : b --> a) :
  precomp_with f g = identity _ -> g = inv_from_z_iso f.
Admitted.

Lemma z_iso_inv_of_z_iso_comp {C : category} (a b c : ob C)
   (f : z_iso a b) (g : z_iso b c) :
   z_iso_inv_from_z_iso (z_iso_comp f g) =
       z_iso_comp (z_iso_inv_from_z_iso g) (z_iso_inv_from_z_iso f).
Admitted.

Lemma z_iso_inv_of_z_iso_id {C : category} (a : ob C) :
   z_iso_inv_from_z_iso (identity_z_iso a) = identity_z_iso a.
Admitted.

Lemma z_iso_inv_z_iso_inv {C : category} (a b : ob C) (f : z_iso a b) :
     z_iso_inv_from_z_iso (z_iso_inv_from_z_iso f) = f.
Admitted.

Lemma z_iso_comp_right_isweq {C : precategory} {a b : ob C} (h : z_iso a b) (c : C) :
  isweq (fun f : b --> c => h · f).
Admitted.

Lemma z_iso_comp_left_isweq {C : precategory} {a b : ob C} (h : z_iso a b) (c : C) :
  isweq (fun f : c --> a => f · h).
Admitted.

Lemma is_iso_from_is_z_iso {C : precategory} {a b : C} (f: a --> b) :
     is_z_isomorphism f -> is_iso f.
Admitted.

Definition z_iso_to_iso {C : precategory} {b c : C} (f : z_iso b c) : iso b c
  := pr1 f ,, is_iso_from_is_z_iso (pr1 f) (pr2 f).

Lemma is_z_iso_from_is_iso {C : precategory} {a b : C} (f : a --> b):
     is_iso f -> is_z_isomorphism f.
Admitted.

Lemma is_z_iso_from_is_iso' (C : precategory) {b c : C} (f : b --> c) :
  is_iso' f -> is_z_isomorphism f.
Admitted.

Definition iso_to_z_iso {C : precategory} {b c : C} : iso b c -> z_iso b c
  := λ f, pr1 f ,, is_z_iso_from_is_iso (pr1 f) (pr2 f).

Lemma roundtrip1_iso_z_iso {C : precategory} {b c : C} (f: iso b c) :
  z_iso_to_iso (iso_to_z_iso f) = f.
Admitted.

Lemma roundtrip2_iso_z_iso {C : category} {b c : C} (f: z_iso b c) :
  iso_to_z_iso (z_iso_to_iso f) = f.
Admitted.

Definition weq_iso_z_iso {C : category} {b c : C} : iso b c ≃ z_iso b c.
Admitted.


Lemma right_inverse_of_iso_is_inverse {C : precategory} {c c' : C}
      (f : c --> c')
      (g : c' --> c) (H  : is_inverse_in_precat f g)
      (h : c' --> c) (HH : f · h = identity _) :
  h = g.
Admitted.

Lemma left_inverse_of_iso_is_inverse {C : precategory} {c c' : C}
      (f : c --> c')
      (g : c' --> c) (H  : is_inverse_in_precat f g)
      (h : c' --> c) (HH : h · f = identity _) :
  h = g.
Admitted.

End Isos.

End UniMath_DOT_CategoryTheory_DOT_Core_DOT_Isos_WRAPPED.
Module Export UniMath_DOT_CategoryTheory_DOT_Core_DOT_Isos.
Module Export UniMath.
Module Export CategoryTheory.
Module Export Core.
Module Isos.
Include UniMath_DOT_CategoryTheory_DOT_Core_DOT_Isos_WRAPPED.Isos.
End Isos.

End Core.

End CategoryTheory.

End UniMath.

End UniMath_DOT_CategoryTheory_DOT_Core_DOT_Isos.

Import UniMath.Foundations.PartA.
Import UniMath.CategoryTheory.Core.Categories.
Import UniMath.CategoryTheory.Core.Isos.

Definition idtoiso {C : precategory} {a b : ob C}:
      a = b -> z_iso a b.
Admitted.

Definition is_univalent (C : category) :=
  ∏ (a b : ob C), isweq (fun p : a = b => idtoiso p).
Definition univalent_category : UU.
exact (∑ C : category, is_univalent C).
Defined.
Definition make_univalent_category (C : category) (H : is_univalent C) : univalent_category.
exact (tpair _ C H).
Defined.
Coercion univalent_category_to_category (C : univalent_category) : category.
exact (pr1 C).
Defined.

Import UniMath.Foundations.PartD.

Local Open Scope cat.
Definition functor_data (C C' : precategory_ob_mor) : UU.
exact (total2 ( fun F : ob C -> ob C' =>  ∏ a b : ob C, a --> b -> F a --> F b)).
Defined.
Definition make_functor_data {C C' : precategory_ob_mor} (F : ob C -> ob C')
           (H : ∏ a b : ob C, a --> b -> F a --> F b) : functor_data C C'.
exact (tpair _ F H).
Defined.
Definition functor_data_constr (C C' : precategory_ob_mor)
           (F : ob C -> ob C') (Fm : ∏ a b : ob C, a --> b -> F a --> F b) :
  functor_data C C'.
exact (tpair _ F Fm).
Defined.
Definition functor_on_objects {C C' : precategory_ob_mor}
     (F : functor_data C C') :  ob C -> ob C'.
exact (pr1 F).
Defined.
Coercion functor_on_objects : functor_data >-> Funclass.
Definition functor_on_morphisms {C C' : precategory_ob_mor} (F : functor_data C C')
  { a b : ob C} :  a --> b -> F a --> F b.
Admitted.

Notation "# F" := (functor_on_morphisms F) (at level 3) : cat.

Definition functor_idax {C C' : precategory_data} (F : functor_data C C') :=
  ∏ a : ob C, #F (identity a) = identity (F a).

Definition functor_compax {C C' : precategory_data} (F : functor_data C C') :=
  ∏ a b c : ob C, ∏ f : a --> b, ∏ g : b --> c, #F (f · g) = #F f · #F g .

Definition is_functor {C C' : precategory_data} (F : functor_data C C') :=
  ( functor_idax F ) × ( functor_compax F ) .
Definition functor (C C' : precategory_data) : UU.
exact (total2 ( λ F : functor_data C C', is_functor F )).
Defined.

Definition make_functor {C C' : precategory_data} (F : functor_data C C') (H : is_functor F) :
  functor C C'.
Proof.
exists F.
exact H.
Defined.
Definition functor_data_from_functor (C C': precategory_data)
     (F : functor C C') : functor_data C C'.
exact (pr1 F).
Defined.
Coercion functor_data_from_functor : functor >-> functor_data.
Definition functor_composite_data {C C' C'' : precategory_ob_mor } (F : functor_data C C')
           (F' : functor_data C' C'') : functor_data C C''.
exact (functor_data_constr C C'' (λ a, F' (F a))  (λ (a b : ob C) f, #F' (#F f))).
Defined.

Lemma is_functor_composite {C C' C'' : precategory_data}
       (F : functor C C') (F' : functor C' C'') :
 is_functor ( functor_composite_data F F' ) .
Admitted.
Definition functor_composite {C C' C'' : precategory_data} (F : functor C C') (F' : functor C' C'') :
  functor C C''.
exact (tpair _ _ (is_functor_composite F F')).
Defined.

Section Constant_Functor.
Variables C D : precategory.
Variable d : D.
Definition constant_functor_data: functor_data C D.
exact (functor_data_constr C D (λ _, d) (λ _ _ _ , identity _)).
Defined.

Lemma is_functor_constant: is_functor constant_functor_data.
Admitted.
Definition constant_functor: functor C D.
exact (tpair _ _ is_functor_constant).
Defined.

End Constant_Functor.

Notation "a ⟶ b" := (functor a b) : cat.

Notation "F ∙ G" := (functor_composite F G) : cat.

Definition graph := ∑ (D : UU), D -> D -> UU.
Definition vertex : graph -> UU.
exact (pr1).
Defined.
Definition edge {g : graph} : vertex g -> vertex g -> UU.
exact (pr2 g).
Defined.
Definition diagram (g : graph) (C : precategory) : UU.
exact (∑ (f : vertex g -> C), ∏ (a b : vertex g), edge a b -> C⟦f a, f b⟧).
Defined.
Definition dob {g : graph} {C : precategory} (d : diagram g C) : vertex g -> C.
exact (pr1 d).
Defined.

Section diagram_from_functor.

Variables (J C : precategory).
Variable (F : functor J C).
Definition graph_from_precategory : graph.
exact ((pr1 (pr1 J))).
Defined.
Definition diagram_from_functor : diagram graph_from_precategory C.
exact (tpair _ _ (pr2 (pr1 F))).
Defined.

End diagram_from_functor.
Definition ColimCocone {C : precategory} {g : graph} (d : diagram g C) : UU.
Admitted.
Definition colim {C : precategory} {g : graph} {d : diagram g C} (CC : ColimCocone d) : C.
Admitted.
Definition colimIn {C : precategory} {g : graph} {d : diagram g C} (CC : ColimCocone d) :
  ∏ (v : vertex g), C⟦dob d v,colim CC⟧.
Admitted.
Definition Colims (C : category) : UU.
Admitted.

Definition colim_mor_eq
           {C : category}
           {G : graph}
           {D : diagram G C}
           (c : ColimCocone D)
           (y : C)
           {f₁ f₂ : colim c --> y}
           (H : ∏ (v : vertex G), colimIn c v · f₁ = colimIn c v · f₂)
  : f₁ = f₂.
Admitted.

Definition precategory_binproduct_mor (C D : precategory_ob_mor) (cd cd' : C × D) := pr1 cd --> pr1 cd' × pr2 cd --> pr2 cd'.
Definition precategory_binproduct_ob_mor (C D : precategory_ob_mor) : precategory_ob_mor.
exact (tpair _ _ (precategory_binproduct_mor C D)).
Defined.

Definition precategory_binproduct_data (C D : precategory_data) : precategory_data.
Proof.
  exists (precategory_binproduct_ob_mor C D).
  split.
  -
 intro cd.
    exact (make_dirprod (identity (pr1 cd)) (identity (pr2 cd))).
  -
 intros cd cd' cd'' fg fg'.
    exact (make_dirprod (pr1 fg · pr1 fg') (pr2 fg · pr2 fg')).
Defined.

Section precategory_binproduct.

Variables C D : precategory.

Lemma is_precategory_precategory_binproduct_data : is_precategory (precategory_binproduct_data C D).
Admitted.
Definition precategory_binproduct : precategory.
exact (tpair _ _ is_precategory_precategory_binproduct_data).
Defined.

Definition has_homsets_precategory_binproduct (hsC : has_homsets C) (hsD : has_homsets D) :
  has_homsets precategory_binproduct.
Admitted.

End precategory_binproduct.
Definition category_binproduct (C D : category) : category.
exact (make_category (precategory_binproduct C D) (has_homsets_precategory_binproduct C D C D)).
Defined.
Local Notation "C × D" := (category_binproduct C D) (at level 75, right associativity).

Definition pr1_functor (A B : category) : (A × B) ⟶ A.
Admitted.

Definition is_pregroupoid (C : category) :=
  ∏ (x y : C) (f : x --> y), is_z_isomorphism f.
Definition pregroupoid : UU.
exact (∑ C : category, is_pregroupoid C).
Defined.
Definition make_pregroupoid (C : category) (is : is_pregroupoid C) : pregroupoid.
exact ((C,, is)).
Defined.
Definition pregroupoid_to_precategory : pregroupoid -> category.
exact (pr1).
Defined.
Definition pregroupoid_is_pregroupoid :
  ∏ gpd : pregroupoid, is_pregroupoid (pr1 gpd).
Admitted.
Coercion pregroupoid_to_precategory : pregroupoid >-> category.
Definition groupoid : UU.
exact (∑ C : category, is_pregroupoid C).
Defined.
Definition make_groupoid (C : category) (is : is_pregroupoid C) : groupoid.
exact ((C,, is)).
Defined.
Definition groupoid_to_category : groupoid -> category.
exact (pr1).
Defined.
Definition groupoid_is_pregroupoid :
  ∏ gpd : groupoid, is_pregroupoid (pr1 gpd).
Admitted.
Coercion groupoid_to_category : groupoid >-> category.
Definition univalent_groupoid : UU.
exact (∑ C : univalent_category, is_pregroupoid C).
Defined.
Definition make_univalent_groupoid (C : univalent_category) (is : is_pregroupoid C) :
  univalent_groupoid.
exact ((C,, is)).
Defined.
Definition univalent_groupoid_to_univalent_category :
  univalent_groupoid -> univalent_category.
exact (pr1).
Defined.
Coercion univalent_groupoid_to_univalent_category :
  univalent_groupoid >-> univalent_category.

Definition path_pregroupoid (X:UU) (iobj : isofhlevel 3 X) : pregroupoid.
  use make_pregroupoid.
  -
 use tpair.
    {
    use make_precategory_one_assoc; use tpair.
    +
 exact (X,, λ x y, x = y).
    +
 use make_dirprod.
      *
 exact (λ _, idpath _).
      *
 intros a b c; exact pathscomp0.
    +
 use make_dirprod.
      *
 reflexivity.
      *
 intros; apply pathscomp0rid.
    +
 intros ? ? ? ? ? ?; apply path_assoc.
    }
    intros ? ? ? ? ? ?.
    apply iobj.
  -
 intros x y path.
    exists (!path).
    split.
    +
 apply pathsinv0r.
    +
 apply pathsinv0l.
Defined.

Definition has_homsets_path_pregroupoid {X : UU} (iobj : isofhlevel 3 X) :
  has_homsets (path_pregroupoid X iobj).
Admitted.

Definition path_groupoid (X : UU) (iobj : isofhlevel 3 X) : groupoid.
Proof.
  use make_groupoid.
  -
 use make_category.
    +
 exact (path_pregroupoid X iobj).
    +
 apply (has_homsets_path_pregroupoid); assumption.
  -
 apply (pregroupoid_is_pregroupoid (path_pregroupoid X iobj)).
Defined.

Lemma is_univalent_path_groupoid (X:UU) (i : isofhlevel 3 X) :
  is_univalent (path_groupoid X i).
Admitted.

Definition path_univalent_groupoid
           {X : UU}
           (i3 : isofhlevel 3 X)
  : univalent_groupoid.
Proof.
  use make_univalent_groupoid.
  -
 exact (make_univalent_category _ (is_univalent_path_groupoid X i3)).
  -
 apply (groupoid_is_pregroupoid _).
Defined.

Definition unit_category : univalent_category.
Proof.
  use path_univalent_groupoid.
  -
 exact unit.
  -
 do 2 (apply hlevelntosn).
apply isapropunit.
Defined.

Definition disp_cat_ob_mor (C : precategory_ob_mor)
  := ∑ (obd : C -> UU), (∏ x y:C, obd x -> obd y -> (x --> y) -> UU).
Definition ob_disp {C: precategory_ob_mor} (D : disp_cat_ob_mor C) : C -> UU.
exact (pr1 D).
Defined.
Coercion ob_disp : disp_cat_ob_mor >-> Funclass.

Definition mor_disp {C: precategory_ob_mor} {D : disp_cat_ob_mor C}
  {x y} xx yy (f : x --> y)
:= pr2 D x y xx yy f : UU.

Local Notation "xx -->[ f ] yy" := (mor_disp xx yy f) (at level 50, left associativity, yy at next level).
Definition disp_cat_id_comp (C : precategory_data)
  (D : disp_cat_ob_mor C)
  : UU.
Admitted.

Definition disp_cat_data C := total2 (disp_cat_id_comp C).
Definition disp_cat_ob_mor_from_disp_cat_data {C: precategory_data}
  (D : disp_cat_data C)
  : disp_cat_ob_mor C.
exact (pr1 D).
Defined.

Coercion disp_cat_ob_mor_from_disp_cat_data :
 disp_cat_data >-> disp_cat_ob_mor.
Definition disp_cat_axioms (C : category) (D : disp_cat_data C)
  : UU.
Admitted.

Definition disp_cat (C : category) := total2 (disp_cat_axioms C).

Definition disp_cat_data_from_disp_cat {C} (D : disp_cat C)
 := pr1 D : disp_cat_data C.
Coercion disp_cat_data_from_disp_cat : disp_cat >-> disp_cat_data.

  Section Total_Category_data.

    Context {C : precategory_data} (D : disp_cat_data C).

    Definition total_category_ob_mor : precategory_ob_mor.
    Proof.
      exists (∑ x:C, D x).
      intros xx yy.

      exact (∑ (f : pr1 xx --> pr1 yy), pr2 xx -->[f] pr2 yy).
    Defined.

    Definition total_category_id_comp : precategory_id_comp (total_category_ob_mor).
Admitted.
Definition total_category_data : precategory_data.
exact ((total_category_ob_mor ,, total_category_id_comp)).
Defined.

  End Total_Category_data.

  Lemma total_category_is_precat {C : category} (D : disp_cat C) :
    is_precategory (total_category_data D).
Admitted.
Definition total_precategory {C : category} (D : disp_cat C) : precategory.
exact ((total_category_data D ,, total_category_is_precat D)).
Defined.

  Lemma total_category_has_homsets {C : category} (D : disp_cat C) :
    has_homsets (total_category_data D).
Admitted.
Definition total_category {C : category} (D : disp_cat C) : category.
exact ((total_precategory D,, total_category_has_homsets D)).
Defined.

  Definition pr1_category_data {C : category} (D : disp_cat C) :
    functor_data (total_category D) C.
  Proof.
    exists pr1.
    intros a b; exact pr1.
  Defined.

  Lemma pr1_category_is_functor {C : category} (D : disp_cat C) :
    is_functor (pr1_category_data D).
Admitted.
Definition pr1_category {C : category} (D : disp_cat C) :
    functor (total_category D) C.
exact (make_functor (pr1_category_data D) (pr1_category_is_functor D)).
Defined.

Section CommaCategory.

  Context {C₁ C₂ C₃ : category}
          (F : C₁ ⟶ C₃)
          (G : C₂ ⟶ C₃).

  Definition comma_disp_cat_ob_mor
    : disp_cat_ob_mor (category_binproduct C₁ C₂).
  Proof.
    use tpair.
    -
 exact (λ x, F (pr1 x) --> G (pr2 x)).
    -
 exact (λ x y i₁ i₂ f, i₁ · #G (pr2 f) = #F (pr1 f) · i₂).
  Defined.

  Definition comma_disp_cat_id_comp
    : disp_cat_id_comp _ comma_disp_cat_ob_mor.
Admitted.
Definition comma_disp_cat_data
    : disp_cat_data (category_binproduct C₁ C₂).
exact (comma_disp_cat_ob_mor,, comma_disp_cat_id_comp).
Defined.

  Definition comma_disp_cat_axioms
    : disp_cat_axioms _ comma_disp_cat_data.
Admitted.

  Definition comma_disp_cat
    : disp_cat (category_binproduct C₁ C₂).
  Proof.
    use tpair.
    -
 exact comma_disp_cat_data.
    -
 exact comma_disp_cat_axioms.
  Defined.
Definition comma
    : category.
exact (total_category comma_disp_cat).
Defined.

  Definition comma_pr1
    : comma ⟶ C₁.
exact (pr1_category comma_disp_cat ∙ pr1_functor C₁ C₂).
Defined.

  End CommaCategory.
  Context {C₁ C₂ D : category}
          (ColimsD : Colims D)
          (P : C₁ ⟶ C₂)
          (F : C₁ ⟶ D).
Definition lan_comma (x : C₂) : category.
exact (comma P (constant_functor unit_category _ x)).
Defined.
Definition lan_pr (x : C₂) : lan_comma x ⟶ D.
exact (comma_pr1 _ _ ∙ F).
Defined.
Definition lan_colim
             (x : C₂)
    : ColimCocone (diagram_from_functor (lan_comma x) D (lan_pr x)).
Admitted.
Definition lan_point
             (x : C₂)
    : D.
exact (colim (lan_colim x)).
Defined.

  Section LanMor.
    Context {x y : C₂}
            (f : x --> y).

    Definition lan_mor
      : D ⟦ lan_point x , lan_point y ⟧.
Admitted.

    Definition lan_mor_colimIn
               (w : C₁)
               (h : P w --> x)
               (a : unit)
      : colimIn (lan_colim x) ((w ,, a) ,, h) · lan_mor
        =
        colimIn (lan_colim y) ((w ,, a) ,, h · f).
Admitted.
  End LanMor.

  Definition lan_data
    : functor_data C₂ D.
  Proof.
    use make_functor_data.
    -
 exact lan_point.
    -
 exact @lan_mor.
  Defined.

  Definition lan_is_functor
    : is_functor lan_data.
  Proof.
    split.
    -
 intros x ; cbn.
      use colim_mor_eq.
      intros v.
      rewrite id_right.
      rewrite lan_mor_colimIn.