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, then from 995 lines to 513 lines, then from 526 lines to 881 lines, then from 885 lines to 589 lines, then from 602 lines to 692 lines, then from 697 lines to 590 lines, then from 603 lines to 644 lines, then from 649 lines to 589 lines, then from 602 lines to 1996 lines, then from 1900 lines to 1183 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: 8.636 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.

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 Export UniMath_DOT_Foundations_DOT_PartB_WRAPPED.
Module Export PartB.


Export UniMath.Foundations.PartA.


Fixpoint isofhlevel (n : nat) (X : UU) : UU
  := match n with
     | O => iscontr X
     | S m => ∏ x : X, ∏ x' : X, (isofhlevel m (x = x'))
     end.


Theorem hlevelretract (n : nat) {X Y : UU} (p : X -> Y) (s : Y -> X)
        (eps : ∏ y : Y , paths (p (s y)) y) : isofhlevel n X -> isofhlevel n Y.
Admitted.

Corollary isofhlevelweqf (n : nat) {X Y : UU} (f : X ≃ Y) :
  isofhlevel n X -> isofhlevel n Y.
Admitted.

Corollary isofhlevelweqb (n : nat) {X Y : UU} (f : X ≃ Y) :
  isofhlevel n Y -> isofhlevel n X.
Admitted.

Lemma isofhlevelsn (n : nat) {X : UU} (f : X -> isofhlevel (S n) X) :
  isofhlevel (S n) X.
Admitted.

Lemma isofhlevelssn (n : nat) {X : UU}
      (is : ∏ x : X, isofhlevel (S n) (x = x)) : isofhlevel (S (S n)) X.
Admitted.
Definition isofhlevelf (n : nat) {X Y : UU} (f : X -> Y) : UU. exact (∏ y : Y, isofhlevel n (hfiber f y)). Defined.

Theorem isofhlevelfhomot (n : nat) {X Y : UU} (f f' : X -> Y)
        (h : ∏ x : X, paths (f x) (f' x)) :
  isofhlevelf n f -> isofhlevelf n f'.
Admitted.

Theorem isofhlevelfpmap (n : nat) {X Y : UU} (f : X -> Y) (Q : Y -> UU) :
  isofhlevelf n f -> isofhlevelf n (fpmap f Q).
Admitted.

Theorem isofhlevelfffromZ (n : nat) {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (z : Z)
        (fs : fibseqstr f g z) (isz : isofhlevel (S n) Z) : isofhlevelf n f.
Admitted.

Theorem isofhlevelXfromg (n : nat) {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (z : Z)
        (fs : fibseqstr f g z) : isofhlevelf n g -> isofhlevel n X.
Admitted.

Theorem isofhlevelffromXY (n : nat) {X Y : UU} (f : X -> Y) :
  isofhlevel n X -> isofhlevel (S n) Y -> isofhlevelf n f.
Admitted.

Theorem isofhlevelXfromfY (n : nat) {X Y : UU} (f : X -> Y) :
  isofhlevelf n f -> isofhlevel n Y -> isofhlevel n X.
Admitted.

Theorem  isofhlevelffib (n : nat) {X : UU} (P : X -> UU) (x : X)
         (is : ∏ x' : X, isofhlevel n (x' = x)) : isofhlevelf n (tpair P x).
Admitted.

Theorem isofhlevelfhfiberpr1y (n : nat) {X Y : UU} (f : X -> Y) (y : Y)
        (is : ∏ y' : Y, isofhlevel n (y' = y)) :
  isofhlevelf n (hfiberpr1 f y).
Admitted.

Theorem isofhlevelfsnfib (n : nat) {X : UU} (P : X -> UU) (x : X)
        (is : isofhlevel (S n) (x = x)) : isofhlevelf (S n) (tpair P x).
Admitted.

Theorem isofhlevelfsnhfiberpr1 (n : nat) {X Y : UU} (f : X -> Y) (y : Y)
        (is : isofhlevel (S n) (y = y)) : isofhlevelf (S n) (hfiberpr1 f y).
Admitted.

Corollary isofhlevelfhfiberpr1 (n : nat) {X Y : UU} (f : X -> Y) (y : Y)
          (is : isofhlevel (S n) Y) : isofhlevelf n (hfiberpr1 f y).
Admitted.

Theorem isofhlevelff (n : nat) {X Y Z : UU} (f : X -> Y) (g : Y -> Z) :
  isofhlevelf n (λ x : X, g (f x)) -> isofhlevelf (S n)  g -> isofhlevelf n f.
Admitted.

Theorem isofhlevelfgf (n : nat) {X Y Z : UU} (f : X -> Y) (g : Y -> Z) :
  isofhlevelf n f -> isofhlevelf n g -> isofhlevelf n (λ x : X, g (f x)).
Admitted.

Theorem isofhlevelfgwtog (n : nat) {X Y Z : UU} (w : X ≃ Y) (g : Y -> Z)
        (is : isofhlevelf n (λ x : X, g (w x))) : isofhlevelf n g.
Admitted.

Theorem isofhlevelfgtogw (n : nat) {X Y Z : UU} (w : X ≃ Y) (g : Y -> Z)
        (is : isofhlevelf n g) : isofhlevelf n (λ x : X, g (w x)).
Admitted.

Corollary isofhlevelfhomot2 (n : nat) {X X' Y : UU} (f : X -> Y) (f' : X' -> Y)
          (w : X ≃ X') (h : ∏ x : X, paths (f x) (f' (w x))) :
  isofhlevelf n f -> isofhlevelf n f'.
Admitted.

Theorem isofhlevelfonpaths (n : nat) {X Y : UU} (f : X -> Y) (x x' : X) :
  isofhlevelf (S n) f -> isofhlevelf n (@maponpaths _ _ f x x').
Admitted.

Theorem isofhlevelfsn (n : nat) {X Y : UU} (f : X -> Y) :
  (∏ x x' : X, isofhlevelf n (@maponpaths _ _ f x x')) -> isofhlevelf (S n) f.
Admitted.

Theorem isofhlevelfssn (n : nat) {X Y : UU} (f : X -> Y) :
  (∏ x : X, isofhlevelf (S n) (@maponpaths _ _ f x x))
  -> isofhlevelf (S (S n)) f.
Admitted.


Theorem isofhlevelfpr1 (n : nat) {X : UU} (P : X -> UU)
        (is : ∏ x : X, isofhlevel n (P x)) : isofhlevelf n (@pr1 X P).
Admitted.

Lemma isweqpr1 {Z : UU} (P : Z -> UU) (is1 : ∏ z : Z, iscontr (P z)) :
  isweq (@pr1 Z P).
Admitted.
Definition weqpr1 {Z : UU} (P : Z -> UU) (is : ∏ z : Z , iscontr (P z)) :
  weq (total2 P) Z. exact (make_weq _ (isweqpr1 P is)). Defined.


Theorem isofhleveltotal2 (n : nat) {X : UU} (P : X -> UU) (is1 : isofhlevel n X)
        (is2 : ∏ x : X, isofhlevel n (P x)) : isofhlevel n (total2 P).
Admitted.

Corollary isofhleveldirprod (n : nat) (X Y : UU) (is1 : isofhlevel n X)
          (is2 : isofhlevel n Y) : isofhlevel n (X × Y).
Admitted.


Definition isaprop := isofhlevel 1.

Definition isPredicate {X : UU} (Y : X -> UU) := ∏ x : X, isaprop (Y x).
Definition isapropunit : isaprop unit. exact (iscontrpathsinunit). Defined.
Definition isapropdirprod (X Y : UU) : isaprop X -> isaprop Y -> isaprop (X × Y). exact (isofhleveldirprod 1 X Y). Defined.

Lemma isapropifcontr {X : UU} (is : iscontr X) : isaprop X.
Admitted.

Theorem hlevelntosn (n : nat) (T : UU) (is : isofhlevel n T) : isofhlevel (S n) T.
Admitted.

Corollary isofhlevelcontr (n : nat) {X : UU} (is : iscontr X) : isofhlevel n X.
Admitted.

Lemma isofhlevelfweq (n : nat) {X Y : UU} (f : X ≃ Y) : isofhlevelf n f.
Admitted.

Corollary isweqfinfibseq {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (z : Z)
          (fs : fibseqstr f g z) (isz : iscontr Z) : isweq f.
Admitted.

Corollary weqhfibertocontr {X Y : UU} (f : X -> Y) (y : Y) (is : iscontr Y) :
  weq (hfiber f y) X.
Admitted.

Corollary weqhfibertounit (X : UU) : (hfiber (λ x : X, tt) tt) ≃ X.
Admitted.

Corollary isofhleveltofun (n : nat) (X : UU) :
  isofhlevel n X -> isofhlevelf n (λ x : X, tt).
Admitted.

Corollary isofhlevelfromfun (n : nat) (X : UU) :
  isofhlevelf n (λ x : X, tt) -> isofhlevel n X.
Admitted.

Definition weqhfiberunit {X Z : UU} (i : X -> Z) (z : Z) :
  (∑ x, hfiber (λ _ : unit, z) (i x)) ≃ hfiber i z.
Admitted.

Lemma isofhlevelsnprop (n : nat) {X : UU} (is : isaprop X) : isofhlevel (S n) X.
Admitted.


Lemma iscontraprop1 {X : UU} (is : isaprop X) (x : X) : iscontr X.
Admitted.

Lemma iscontraprop1inv {X : UU} (f : X -> iscontr X) : isaprop X.
Admitted.

Definition isProofIrrelevant (X:UU) := ∏ x y:X, x = y.

Lemma proofirrelevance (X : UU) : isaprop X -> isProofIrrelevant X.
Admitted.

Lemma invproofirrelevance (X : UU) : isProofIrrelevant X -> isaprop X.
Admitted.

Lemma isProofIrrelevant_paths {X} (irr:isProofIrrelevant X) {x y:X} : isProofIrrelevant (x=y).
Admitted.

Lemma isapropcoprod (P Q : UU) :
  isaprop P -> isaprop Q -> (P -> Q -> ∅) -> isaprop (P ⨿ Q).
Admitted.

Lemma isweqimplimpl {X Y : UU} (f : X -> Y) (g : Y -> X) (isx : isaprop X)
      (isy : isaprop Y) : isweq f.
Admitted.

Definition weqimplimpl {X Y : UU} (f : X -> Y) (g : Y -> X) (isx : isaprop X)
           (isy : isaprop Y) := make_weq _ (isweqimplimpl f g isx isy).
Definition weqiff {X Y : UU} : (X <-> Y) -> isaprop X -> isaprop Y -> X ≃ Y. exact (λ f i j, make_weq _ (isweqimplimpl (pr1 f) (pr2 f) i j)). Defined.
Definition weq_to_iff {X Y : UU} : X ≃ Y -> (X <-> Y). exact (λ f, (pr1weq f ,, invmap f)). Defined.

Theorem isapropempty: isaprop empty.
Admitted.

Theorem isapropifnegtrue {X : UU} (a : X -> empty) : isaprop X.
Admitted.

Lemma isapropretract {P Q : UU} (i : isaprop Q) (f : P -> Q) (g : Q -> P)
      (h : g ∘ f ~ idfun _) : isaprop P.
Admitted.

Lemma isapropcomponent1 (P Q : UU) : isaprop (P ⨿ Q) -> isaprop P.
Admitted.

Lemma isapropcomponent2 (P Q : UU) : isaprop (P ⨿ Q) -> isaprop Q.
Admitted.


Definition isincl {X Y : UU} (f : X -> Y) := isofhlevelf 1 f.

Definition incl (X Y : UU) := total2 (fun f : X -> Y => isincl f).
Definition make_incl {X Y : UU} (f : X -> Y) (is : isincl f) :
  incl X Y. exact (tpair _ f is). Defined.
Definition pr1incl (X Y : UU) : incl X Y -> (X -> Y). exact (@pr1 _ _). Defined.
Coercion pr1incl : incl >-> Funclass.

Lemma isinclweq (X Y : UU) (f : X -> Y) : isweq f -> isincl f.
Admitted.
Coercion isinclweq : isweq >-> isincl.

Lemma isofhlevelfsnincl (n : nat) {X Y : UU} (f : X -> Y) (is : isincl f) :
  isofhlevelf (S n) f.
Admitted.
Definition weqtoincl {X Y : UU} : X ≃ Y -> incl X Y. exact (λ w, make_incl (pr1weq w) (pr2 w)). Defined.

Lemma isinclcomp {X Y Z : UU} (f : incl X Y) (g : incl Y Z) :
  isincl (funcomp (pr1 f) (pr1 g)).
Admitted.
Definition inclcomp {X Y Z : UU} (f : incl X Y) (g : incl Y Z) :
  incl X Z. exact (make_incl (funcomp (pr1 f) (pr1 g)) (isinclcomp f g)). Defined.

Lemma isincltwooutof3a {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (isg : isincl g)
      (isgf : isincl (funcomp f g)) : isincl f.
Admitted.

Lemma isinclgwtog {X Y Z : UU} (w : X ≃ Y) (g : Y -> Z)
      (is : isincl (funcomp w g)) : isincl g.
Admitted.

Lemma isinclgtogw {X Y Z : UU}  (w : X ≃ Y) (g : Y -> Z) (is : isincl g) :
  isincl (funcomp w g).
Admitted.

Lemma isinclhomot {X Y : UU} (f g : X -> Y) (h : homot f g) (isf : isincl f) :
  isincl g.
Admitted.
Definition isofhlevelsninclb (n : nat) {X Y : UU} (f : X -> Y) (is : isincl f) :
  isofhlevel (S n) Y -> isofhlevel (S n) X. exact (isofhlevelXfromfY (S n) f (isofhlevelfsnincl n f is)). Defined.
Definition isapropinclb {X Y : UU} (f : X -> Y) (isf : isincl f) :
  isaprop Y -> isaprop X. exact (isofhlevelXfromfY 1 _ isf). Defined.

Lemma iscontrhfiberofincl {X Y : UU} (f : X -> Y) :
  isincl f -> (∏ x : X, iscontr (hfiber f (f x))).
Admitted.


Definition isInjective {X Y : UU} (f : X -> Y)
  := ∏ (x x' : X), isweq (maponpaths f : x = x' -> f x = f x').

Definition Injectivity {X Y : UU} (f : X -> Y) :
  isInjective f -> ∏ (x x' : X), x = x'  ≃  f x = f x'.
Admitted.

Lemma isweqonpathsincl {X Y : UU} (f : X -> Y) : isincl f -> isInjective f.
Admitted.

Definition weqonpathsincl {X Y : UU} (f : X -> Y) (is : isincl f) (x x' : X)
  := make_weq _ (isweqonpathsincl f is x x').

Definition invmaponpathsincl {X Y : UU} (f : X -> Y) :
  isincl f -> ∏ x x', f x = f x' -> x = x'.
Admitted.

Lemma isinclweqonpaths {X Y : UU} (f : X -> Y) : isInjective f -> isincl f.
Admitted.
Definition isinclpr1 {X : UU} (P : X -> UU) (is : ∏ x : X, isaprop (P x)) :
  isincl (@pr1 X P). exact (isofhlevelfpr1 (S O) P is). Defined.

Theorem subtypeInjectivity {A : UU} (B : A -> UU) :
  isPredicate B -> ∏ (x y : total2 B), (x = y) ≃ (pr1 x = pr1 y).
Admitted.

Corollary subtypePath {A : UU} {B : A -> UU} (is : isPredicate B)
   {s s' : total2 (λ x, B x)} : pr1 s = pr1 s' -> s = s'.
Admitted.

Corollary subtypePath' {A : UU} {B : A -> UU}
   {s s' : total2 (λ x, B x)} : pr1 s = pr1 s' -> isaprop (B (pr1 s')) -> s = s'.
Admitted.


Corollary unique_exists {A : UU} {B : A -> UU} (x : A) (b : B x)
          (h : ∏ y, isaprop (B y)) (H : ∏ y, B y -> y = x) :
  iscontr (total2 (λ t : A, B t)).
Admitted.

Definition subtypePairEquality {X : UU} {P : X -> UU} (is : isPredicate P)
           {x y : X} {p : P x} {q : P y} :
  x = y -> (x,,p) = (y,,q).
Admitted.

Definition subtypePairEquality' {X : UU} {P : X -> UU}
           {x y : X} {p : P x} {q : P y} :
  x = y -> isaprop(P y) -> (x,,p) = (y,,q).
Admitted.

Theorem samehfibers {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (is1 : isincl g)
        (y : Y) :  hfiber f y ≃ hfiber (g ∘ f) (g y).
Admitted.
Definition isaset (X : UU) : UU. exact (∏ x x' : X, isaprop (x = x')). Defined.


Notation isasetdirprod := (isofhleveldirprod 2).

Lemma isasetunit : isaset unit.
Admitted.

Lemma isasetempty : isaset empty.
Admitted.

Lemma isasetifcontr {X : UU} (is : iscontr X) : isaset X.
Admitted.

Lemma isasetaprop {X : UU} (is : isaprop X) : isaset X.
Admitted.

Corollary isaset_total2 {X : UU} (P : X->UU) :
  isaset X -> (∏ x, isaset (P x)) -> isaset (∑ x, P x).
Admitted.

Corollary isaset_dirprod {X Y : UU} : isaset X -> isaset Y -> isaset (X × Y).
Admitted.

Corollary isaset_hfiber {X Y : UU} (f : X -> Y) (y : Y) : isaset X -> isaset Y -> isaset (hfiber f y).
Admitted.


Lemma uip {X : UU} (is : isaset X) {x x' : X} (e e' : x = x') : e = e'.
Admitted.


Lemma isofhlevelssnset (n : nat) (X : UU) (is : isaset X) :
  isofhlevel (S (S n)) X.
Admitted.

Lemma isasetifiscontrloops (X : UU) : (∏ x : X, iscontr (x = x)) -> isaset X.
Admitted.

Lemma iscontrloopsifisaset (X : UU) :
  (isaset X) -> (∏ x : X, iscontr (x = x)).
Admitted.


Theorem isasetsubset {X Y : UU} (f : X -> Y) (is1 : isaset Y) (is2 : isincl f) :
  isaset X.
Admitted.


Theorem isinclfromhfiber {X Y : UU} (f: X -> Y) (is : isaset Y) (y : Y) :
  @isincl (hfiber f y) X (@pr1 _ _).
Admitted.


Theorem isinclbetweensets {X Y : UU} (f : X -> Y)
        (isx : isaset X) (isy : isaset Y)
        (inj : ∏ x x' : X , (paths (f x) (f x') -> x = x')) : isincl f.
Admitted.


Theorem isinclfromunit {X : UU} (f : unit -> X) (is : isaset X) : isincl f.
Admitted.

Corollary set_bijection_to_weq {X Y : UU} (f : X -> Y) :
  UniqueConstruction f -> isaset Y -> isweq f.
Admitted.


Definition complementary P Q := (P -> Q -> ∅) × (P ⨿ Q).

Definition complementary_to_neg_iff {P Q} : complementary P Q -> ¬P <-> Q.
Admitted.

Definition decidable (X:UU) := X ⨿ ¬X.

Definition decidable_to_complementary {X} : decidable X -> complementary X (¬X).
Admitted.

Definition decidable_dirprod (X Y : UU) :
  decidable X -> decidable Y -> decidable (X × Y).
Admitted.


Definition isdecprop (P:UU) := (P ⨿ ¬P) × isaprop P.
Definition isdecproptoisaprop ( X : UU ) ( is : isdecprop X ) : isaprop X. exact (pr2 is). Defined.
Coercion isdecproptoisaprop : isdecprop >-> isaprop .

Lemma isdecpropif ( X : UU ) : isaprop X -> X ⨿ ¬ X -> isdecprop X.
Admitted.

Lemma isdecpropfromiscontr {P} : iscontr P -> isdecprop P.
Admitted.

Lemma isdecpropempty : isdecprop ∅.
Admitted.

Lemma isdecpropweqf {X Y} : X≃Y -> isdecprop X -> isdecprop Y.
Admitted.

Lemma isdecpropweqb {X Y} : X≃Y -> isdecprop Y -> isdecprop X.
Admitted.

Lemma isdecproplogeqf {X Y : UU} (isx : isdecprop X) (isy : isaprop Y)
      (lg : X <-> Y) : isdecprop Y.
Admitted.

Lemma isdecproplogeqb {X Y : UU} (isx : isaprop X) (isy : isdecprop Y)
      (lg : X <-> Y) : isdecprop X.
Admitted.

Lemma isdecpropfromneg {P : UU} : ¬P -> isdecprop P.
Admitted.
Definition isdeceq (X:UU) : UU. exact (∏ (x x':X), decidable (x=x')). Defined.

Lemma isdeceqweqf {X Y : UU} (w : X ≃ Y) (is : isdeceq X) : isdeceq Y.
Admitted.

Lemma isdeceqweqb {X Y : UU} (w : X ≃ Y) (is : isdeceq Y) : isdeceq X.
Admitted.

Theorem isdeceqinclb {X Y : UU} (f : X -> Y) (is : isdeceq Y) (is' : isincl f) :
  isdeceq X.
Admitted.

Lemma isdeceqifisaprop (X : UU) : isaprop X -> isdeceq X.
Admitted.

Definition booleq {X : UU} (is : isdeceq X) (x x' : X) : bool.
Admitted.

Lemma eqfromdnegeq (X : UU) (is : isdeceq X) (x x' : X) :
  dneg (x = x') -> x = x'.
Admitted.

Lemma isdecequnit : isdeceq unit.
Admitted.

Theorem isdeceqbool: isdeceq bool.
Admitted.

Lemma isdeceqcoprod {A B : UU} (h1 : isdeceq A) (h2 : isdeceq B) :
  isdeceq (A ⨿ B).
Admitted.


Definition isisolated (X:UU) (x:X) := ∏ x':X, (x = x') ⨿ (x != x').

Definition isolated ( T : UU ) := ∑ t:T, isisolated _ t.
Definition make_isolated ( T : UU ) (t:T) (i:isisolated _ t) : isolated T. exact ((t,,i)). Defined.
Definition pr1isolated ( T : UU ) (x:isolated T) : T. exact (pr1 x). Defined.

Theorem isaproppathsfromisolated (X : UU) (x : X) (is : isisolated X x) :
  ∏ x', isaprop(x = x').
Admitted.

Local Open Scope transport.

Theorem isaproppathstoisolated (X : UU) (x : X) (is : isisolated X x) :
  ∏ x' : X, isaprop (x' = x).
Admitted.

Lemma isisolatedweqf { X Y : UU } (f : X ≃ Y) (x:X) : isisolated X x -> isisolated Y (f x).
Admitted.

Theorem isisolatedinclb {X Y : UU} (f : X -> Y) (is : isincl f) (x : X)
        (is0 : isisolated _ (f x)) : isisolated _ x.
Admitted.

Lemma disjointl1 (X : UU) : isisolated (coprod X unit) (ii2 tt).
Admitted.


Theorem isasetifdeceq (X : UU) : isdeceq X -> isaset X.
Admitted.


Lemma isdeceq_total2 {X : UU} {P : X -> UU}
  : isdeceq X -> (∏ x : X, isdeceq (P x)) → isdeceq (∑ x : X, P x).
Admitted.


Definition isolfun1 {X Y:UU} (x1:X) (i1 : isisolated _ x1) (y1 y':Y) : X → Y.
Admitted.

Definition decfun1 {X Y:UU} (i : isdeceq X) (x1:X) : ∏ (y1 y':Y), X → Y.
Admitted.

Definition isolfun2 {X Y:UU} (x1 x2:X) (i1 : isisolated _ x1) (i2 : isisolated _ x2) (y1 y2 y':Y) : X → Y.
Admitted.

Definition decfun2 {X Y:UU} (i : isdeceq X) (x1 x2:X) (y1 y2 y':Y) : X → Y.
Admitted.

Definition isolfun3 {X Y:UU} (x1 x2 x3:X) (i1 : isisolated _ x1) (i2 : isisolated _ x2) (i3 : isisolated _ x3) (y1 y2 y3 y':Y) : X → Y.
Admitted.

Definition decfun3 {X Y:UU} (i : isdeceq X) (x1 x2 x3:X) (y1 y2 y3 y':Y) : X → Y.
Admitted.


Theorem isasetbool: isaset bool.
Admitted.


Definition subsetsplit {X : UU} (f : X -> bool) (x : X) :
  (hfiber f true) ⨿ (hfiber f false).
Admitted.
Definition subsetsplitinv {X : UU} (f : X -> bool)
           (ab : (hfiber f true) ⨿ (hfiber f false)) : X. exact (match ab with ii1 xt => pr1 xt | ii2 xf => pr1 xf end). Defined.

Theorem weqsubsetsplit {X : UU} (f : X -> bool) :
  weq X ((hfiber f true) ⨿ (hfiber f false)).
Admitted.


End PartB.

End UniMath_DOT_Foundations_DOT_PartB_WRAPPED.
Definition precategory_ob_mor : UU.
exact (∑ ob : UU, ob -> ob -> UU).
Defined.
Definition ob (C : precategory_ob_mor) : UU.
exact (@pr1 _ _ C).
Defined.
Coercion ob : precategory_ob_mor >-> UU.
Definition precategory_morphisms { C : precategory_ob_mor } :
       C ->  C -> UU.
exact (pr2 C).
Defined.

Declare Scope cat.

Local Open Scope cat.

Notation "a --> b" := (precategory_morphisms a b) : cat.

Notation "C ⟦ a , b ⟧" := (precategory_morphisms (C:=C) a b) : cat.
Definition precategory_id_comp (C : precategory_ob_mor) : UU.
exact ((∏ c : C, c --> c)
      ×
    (∏ a b c : C, a --> b -> b --> c -> a --> c)).
Defined.
Definition precategory_data : UU.
exact (∑ C : precategory_ob_mor, precategory_id_comp C).
Defined.
Definition precategory_ob_mor_from_precategory_data (C : precategory_data) :
     precategory_ob_mor.
exact (pr1 C).
Defined.
Coercion precategory_ob_mor_from_precategory_data :
  precategory_data >-> precategory_ob_mor.
Definition identity {C : precategory_data}
  : ∏ c : C, c --> c.
exact (pr1 (pr2 C)).
Defined.
Definition compose {C : precategory_data} { a b c : C }
  : a --> b -> b --> c -> a --> c.
exact (pr2 (pr2 C) a b c).
Defined.

Notation "f · g" := (compose f g) : cat.
Definition is_precategory (C : precategory_data) : UU.
Admitted.
Definition is_precategory_one_assoc (C : precategory_data) : UU.
exact (((∏ (a b : C) (f : a --> b), identity a · f = f)
     ×
     (∏ (a b : C) (f : a --> b), f · identity b = f))
    ×
    (∏ (a b c d : C) (f : a --> b) (g : b --> c) (h : c --> d), f · (g · h) = (f · g) · h)).
Defined.
Definition is_precategory_one_assoc_to_two (C : precategory_data) :
  is_precategory_one_assoc C -> is_precategory C.
Admitted.

Definition precategory := total2 is_precategory.
Definition make_precategory_one_assoc (C : precategory_data) (H : is_precategory_one_assoc C)
  : precategory.
exact (tpair _ C (is_precategory_one_assoc_to_two C H)).
Defined.
Definition precategory_data_from_precategory (C : precategory) :
       precategory_data.
exact (pr1 C).
Defined.
Coercion precategory_data_from_precategory : precategory >-> precategory_data.
Definition has_homsets (C : precategory_ob_mor) : UU.
exact (∏ a b : C, isaset (a --> b)).
Defined.

Definition category := ∑ C:precategory, has_homsets C.
Definition make_category C h : category := C,,h.
Definition category_to_precategory : category -> precategory.
exact (pr1).
Defined.
Coercion category_to_precategory : category >-> precategory.
Coercion homset_property (C : category) : has_homsets C.
Admitted.
Definition id_right (C : precategory) :
   ∏ (a b : C) (f : a --> b),
           f · identity b = f.
Admitted.

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_z_isomorphism {C : precategory_data} {a b : ob C}
           (f : a --> b) := ∑ g, is_inverse_in_precat f g.

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

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