SkySkimmer/foo.v

## foo.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 *)
(* 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 (155688103c43f578a8aef464bf0cb9a76acd269e)
   Expected coqc runtime on this file: 10.088 sec *)
Require UniMath.CategoryTheory.limits.graphs.colimits.


Import UniMath.Foundations.All.
Import UniMath.CategoryTheory.Core.Categories.
Import UniMath.CategoryTheory.Core.Functors.
Local Open Scope cat.

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.
Import UniMath.CategoryTheory.Core.Isos.
Import UniMath.CategoryTheory.Core.Univalence.

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.
Import UniMath.CategoryTheory.limits.graphs.colimits.
  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.
	(* -- 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 *)
	(* 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 (155688103c43f578a8aef464bf0cb9a76acd269e)
	Expected coqc runtime on this file: 10.088 sec *)
	Require UniMath.CategoryTheory.limits.graphs.colimits.



	Import UniMath.Foundations.All.
	Import UniMath.CategoryTheory.Core.Categories.
	Import UniMath.CategoryTheory.Core.Functors.
	Local Open Scope cat.

	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.
	Import UniMath.CategoryTheory.Core.Isos.
	Import UniMath.CategoryTheory.Core.Univalence.

	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.
	Import UniMath.CategoryTheory.limits.graphs.colimits.
	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.