  P : ob poset_sym_mon_closed_cat
  h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧
  q : h · precomp_arr E' w f = h · precomp_arr E' w g
  ============================
   ((λ (w : C) (P : poset_sym_mon_closed_cat)
     (h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧)
     (q : h · precomp_arr E' w f = h · precomp_arr E' w g),
     ((λ z : pr1 P, pr1 h z,, eqtohomot (maponpaths pr1 q) z),,
      make_poset_enrichment_coequalizer_is_coequalizer_subproof0 w P h q)
     · poset_enrichment_coequalizer_to_equalizer EEC f g) w P h q
    · precomp_arr E' w
        (enriched_coequalizer_cocone_in E' f g
           make_poset_enrichment_coequalizer_cocone) = h)


Going to execute:
simple refine (p _) ||
  simple refine (p _ _) ||
    simple refine (p _ _ _) ||
      simple refine (p _ _ _ _) ||
        simple refine (p _ _ _ _ _) ||
          simple refine (p _ _ _ _ _ _) ||
            simple refine (p _ _ _ _ _ _ _) ||
              simple refine (p _ _ _ _ _ _ _ _) ||
                simple refine (p _ _ _ _ _ _ _ _ _) ||
                  simple refine (p _ _ _ _ _ _ _ _ _ _) ||
                    simple refine (p _ _ _ _ _ _ _ _ _ _ _) ||
                      simple refine (p _ _ _ _ _ _ _ _ _ _ _ _) ||
                        simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
                          simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
                            simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)
Level 0: In environment
C : category
E : poset_enrichment C
E' := make_enrichment_over_poset C E : enrichment C poset_sym_mon_closed_cat
EEC : poset_enrichment_coequalizers
x, y : C
f, g : C ⟦ x, y ⟧
w : C
P : poset_sym_mon_closed_cat
h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧
q : h · precomp_arr E' w f = h · precomp_arr E' w g
The term "eq_monotone_function" has type
 "∏ f0 g0 : monotone_function ?R₁ ?R₂, (∏ x0 : ?X₁, f0 x0 = g0 x0) → f0 = g0"
while it is expected to have type
 "((λ z : pr1 P, pr1 h z,, eqtohomot (maponpaths pr1 q) z),,
   make_poset_enrichment_coequalizer_is_coequalizer_subproof0 w P h q)
  · poset_enrichment_coequalizer_to_equalizer EEC f g
  · precomp_arr E' w
      (enriched_coequalizer_cocone_in E' f g
         make_poset_enrichment_coequalizer_cocone) = h".
Level 0: In environment
C : category
E : poset_enrichment C
E' := make_enrichment_over_poset C E : enrichment C poset_sym_mon_closed_cat
EEC : poset_enrichment_coequalizers
x, y : C
f, g : C ⟦ x, y ⟧
w : C
P : poset_sym_mon_closed_cat
h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧
q : h · precomp_arr E' w f = h · precomp_arr E' w g
The term "eq_monotone_function" has type
 "∏ f0 g0 : monotone_function ?R₁ ?R₂, (∏ x0 : ?X₁, f0 x0 = g0 x0) → f0 = g0"
while it is expected to have type
 "((λ z : pr1 P, pr1 h z,, eqtohomot (maponpaths pr1 q) z),,
   make_poset_enrichment_coequalizer_is_coequalizer_subproof0 w P h q)
  · poset_enrichment_coequalizer_to_equalizer EEC f g
  · precomp_arr E' w
      (enriched_coequalizer_cocone_in E' f g
         make_poset_enrichment_coequalizer_cocone) = h".

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧
  q : h · precomp_arr E' w f = h · precomp_arr E' w g
  ============================
   ((λ (w : C) (P : poset_sym_mon_closed_cat)
     (h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧)
     (q : h · precomp_arr E' w f = h · precomp_arr E' w g),
     ((λ z : pr1 P, pr1 h z,, eqtohomot (maponpaths pr1 q) z),,
      make_poset_enrichment_coequalizer_is_coequalizer_subproof0 w P h q)
     · poset_enrichment_coequalizer_to_equalizer EEC f g) w P h q
    · precomp_arr E' w
        (enriched_coequalizer_cocone_in E' f g
           make_poset_enrichment_coequalizer_cocone) = h)


Going to execute:
simple refine (p _)

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧
  q : h · precomp_arr E' w f = h · precomp_arr E' w g
  ============================
   ((λ (w : C) (P : poset_sym_mon_closed_cat)
     (h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧)
     (q : h · precomp_arr E' w f = h · precomp_arr E' w g),
     ((λ z : pr1 P, pr1 h z,, eqtohomot (maponpaths pr1 q) z),,
      make_poset_enrichment_coequalizer_is_coequalizer_subproof0 w P h q)
     · poset_enrichment_coequalizer_to_equalizer EEC f g) w P h q
    · precomp_arr E' w
        (enriched_coequalizer_cocone_in E' f g
           make_poset_enrichment_coequalizer_cocone) = h)


Going to execute:
<coq-core.plugins.ltac::simple_refine@0> $1

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧
  q : h · precomp_arr E' w f = h · precomp_arr E' w g
  ============================
   ((λ (w : C) (P : poset_sym_mon_closed_cat)
     (h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧)
     (q : h · precomp_arr E' w f = h · precomp_arr E' w g),
     ((λ z : pr1 P, pr1 h z,, eqtohomot (maponpaths pr1 q) z),,
      make_poset_enrichment_coequalizer_is_coequalizer_subproof0 w P h q)
     · poset_enrichment_coequalizer_to_equalizer EEC f g) w P h q
    · precomp_arr E' w
        (enriched_coequalizer_cocone_in E' f g
           make_poset_enrichment_coequalizer_cocone) = h)


Going to execute:
simple refine (p _ _) ||
  simple refine (p _ _ _) ||
    simple refine (p _ _ _ _) ||
      simple refine (p _ _ _ _ _) ||
        simple refine (p _ _ _ _ _ _) ||
          simple refine (p _ _ _ _ _ _ _) ||
            simple refine (p _ _ _ _ _ _ _ _) ||
              simple refine (p _ _ _ _ _ _ _ _ _) ||
                simple refine (p _ _ _ _ _ _ _ _ _ _) ||
                  simple refine (p _ _ _ _ _ _ _ _ _ _ _) ||
                    simple refine (p _ _ _ _ _ _ _ _ _ _ _ _) ||
                      simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
                        simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
                          simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)
Level 0: In environment
C : category
E : poset_enrichment C
E' := make_enrichment_over_poset C E : enrichment C poset_sym_mon_closed_cat
EEC : poset_enrichment_coequalizers
x, y : C
f, g : C ⟦ x, y ⟧
w : C
P : poset_sym_mon_closed_cat
h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧
q : h · precomp_arr E' w f = h · precomp_arr E' w g
The term "eq_monotone_function ?f" has type
 "∏ g0 : monotone_function ?R₁ ?R₂, (∏ x0 : ?X₁, ?f x0 = g0 x0) → ?f = g0"
while it is expected to have type
 "((λ z : pr1 P, pr1 h z,, eqtohomot (maponpaths pr1 q) z),,
   make_poset_enrichment_coequalizer_is_coequalizer_subproof0 w P h q)
  · poset_enrichment_coequalizer_to_equalizer EEC f g
  · precomp_arr E' w
      (enriched_coequalizer_cocone_in E' f g
         make_poset_enrichment_coequalizer_cocone) = h".
Level 0: In environment
C : category
E : poset_enrichment C
E' := make_enrichment_over_poset C E : enrichment C poset_sym_mon_closed_cat
EEC : poset_enrichment_coequalizers
x, y : C
f, g : C ⟦ x, y ⟧
w : C
P : poset_sym_mon_closed_cat
h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧
q : h · precomp_arr E' w f = h · precomp_arr E' w g
The term "eq_monotone_function ?f" has type
 "∏ g0 : monotone_function ?R₁ ?R₂, (∏ x0 : ?X₁, ?f x0 = g0 x0) → ?f = g0"
while it is expected to have type
 "((λ z : pr1 P, pr1 h z,, eqtohomot (maponpaths pr1 q) z),,
   make_poset_enrichment_coequalizer_is_coequalizer_subproof0 w P h q)
  · poset_enrichment_coequalizer_to_equalizer EEC f g
  · precomp_arr E' w
      (enriched_coequalizer_cocone_in E' f g
         make_poset_enrichment_coequalizer_cocone) = h".

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧
  q : h · precomp_arr E' w f = h · precomp_arr E' w g
  ============================
   ((λ (w : C) (P : poset_sym_mon_closed_cat)
     (h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧)
     (q : h · precomp_arr E' w f = h · precomp_arr E' w g),
     ((λ z : pr1 P, pr1 h z,, eqtohomot (maponpaths pr1 q) z),,
      make_poset_enrichment_coequalizer_is_coequalizer_subproof0 w P h q)
     · poset_enrichment_coequalizer_to_equalizer EEC f g) w P h q
    · precomp_arr E' w
        (enriched_coequalizer_cocone_in E' f g
           make_poset_enrichment_coequalizer_cocone) = h)


Going to execute:
simple refine (p _ _)

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧
  q : h · precomp_arr E' w f = h · precomp_arr E' w g
  ============================
   ((λ (w : C) (P : poset_sym_mon_closed_cat)
     (h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧)
     (q : h · precomp_arr E' w f = h · precomp_arr E' w g),
     ((λ z : pr1 P, pr1 h z,, eqtohomot (maponpaths pr1 q) z),,
      make_poset_enrichment_coequalizer_is_coequalizer_subproof0 w P h q)
     · poset_enrichment_coequalizer_to_equalizer EEC f g) w P h q
    · precomp_arr E' w
        (enriched_coequalizer_cocone_in E' f g
           make_poset_enrichment_coequalizer_cocone) = h)


Going to execute:
<coq-core.plugins.ltac::simple_refine@0> $1

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧
  q : h · precomp_arr E' w f = h · precomp_arr E' w g
  ============================
   ((λ (w : C) (P : poset_sym_mon_closed_cat)
     (h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧)
     (q : h · precomp_arr E' w f = h · precomp_arr E' w g),
     ((λ z : pr1 P, pr1 h z,, eqtohomot (maponpaths pr1 q) z),,
      make_poset_enrichment_coequalizer_is_coequalizer_subproof0 w P h q)
     · poset_enrichment_coequalizer_to_equalizer EEC f g) w P h q
    · precomp_arr E' w
        (enriched_coequalizer_cocone_in E' f g
           make_poset_enrichment_coequalizer_cocone) = h)


Going to execute:
simple refine (p _ _ _) ||
  simple refine (p _ _ _ _) ||
    simple refine (p _ _ _ _ _) ||
      simple refine (p _ _ _ _ _ _) ||
        simple refine (p _ _ _ _ _ _ _) ||
          simple refine (p _ _ _ _ _ _ _ _) ||
            simple refine (p _ _ _ _ _ _ _ _ _) ||
              simple refine (p _ _ _ _ _ _ _ _ _ _) ||
                simple refine (p _ _ _ _ _ _ _ _ _ _ _) ||
                  simple refine (p _ _ _ _ _ _ _ _ _ _ _ _) ||
                    simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
                      simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) || simple
                       refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)
Level 0: In environment
C : category
E : poset_enrichment C
E' := make_enrichment_over_poset C E : enrichment C poset_sym_mon_closed_cat
EEC : poset_enrichment_coequalizers
x, y : C
f, g : C ⟦ x, y ⟧
w : C
P : poset_sym_mon_closed_cat
h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧
q : h · precomp_arr E' w f = h · precomp_arr E' w g
The term "eq_monotone_function ?f ?g" has type
 "(∏ x0 : ?X₁, ?f x0 = ?g x0) → ?f = ?g" while it is expected to have type
 "((λ z : pr1 P, pr1 h z,, eqtohomot (maponpaths pr1 q) z),,
   make_poset_enrichment_coequalizer_is_coequalizer_subproof0 w P h q)
  · poset_enrichment_coequalizer_to_equalizer EEC f g
  · precomp_arr E' w
      (enriched_coequalizer_cocone_in E' f g
         make_poset_enrichment_coequalizer_cocone) = h".
Level 0: In environment
C : category
E : poset_enrichment C
E' := make_enrichment_over_poset C E : enrichment C poset_sym_mon_closed_cat
EEC : poset_enrichment_coequalizers
x, y : C
f, g : C ⟦ x, y ⟧
w : C
P : poset_sym_mon_closed_cat
h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧
q : h · precomp_arr E' w f = h · precomp_arr E' w g
The term "eq_monotone_function ?f ?g" has type
 "(∏ x0 : ?X₁, ?f x0 = ?g x0) → ?f = ?g" while it is expected to have type
 "((λ z : pr1 P, pr1 h z,, eqtohomot (maponpaths pr1 q) z),,
   make_poset_enrichment_coequalizer_is_coequalizer_subproof0 w P h q)
  · poset_enrichment_coequalizer_to_equalizer EEC f g
  · precomp_arr E' w
      (enriched_coequalizer_cocone_in E' f g
         make_poset_enrichment_coequalizer_cocone) = h".

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧
  q : h · precomp_arr E' w f = h · precomp_arr E' w g
  ============================
   ((λ (w : C) (P : poset_sym_mon_closed_cat)
     (h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧)
     (q : h · precomp_arr E' w f = h · precomp_arr E' w g),
     ((λ z : pr1 P, pr1 h z,, eqtohomot (maponpaths pr1 q) z),,
      make_poset_enrichment_coequalizer_is_coequalizer_subproof0 w P h q)
     · poset_enrichment_coequalizer_to_equalizer EEC f g) w P h q
    · precomp_arr E' w
        (enriched_coequalizer_cocone_in E' f g
           make_poset_enrichment_coequalizer_cocone) = h)


Going to execute:
simple refine (p _ _ _)

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧
  q : h · precomp_arr E' w f = h · precomp_arr E' w g
  ============================
   ((λ (w : C) (P : poset_sym_mon_closed_cat)
     (h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧)
     (q : h · precomp_arr E' w f = h · precomp_arr E' w g),
     ((λ z : pr1 P, pr1 h z,, eqtohomot (maponpaths pr1 q) z),,
      make_poset_enrichment_coequalizer_is_coequalizer_subproof0 w P h q)
     · poset_enrichment_coequalizer_to_equalizer EEC f g) w P h q
    · precomp_arr E' w
        (enriched_coequalizer_cocone_in E' f g
           make_poset_enrichment_coequalizer_cocone) = h)


Going to execute:
<coq-core.plugins.ltac::simple_refine@0> $1

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧
  q : h · precomp_arr E' w f = h · precomp_arr E' w g
  ============================
   (∏ x0 : pr1 P,
    ((λ (w : C) (P : poset_sym_mon_closed_cat)
      (h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧)
      (q : h · precomp_arr E' w f = h · precomp_arr E' w g),
      ((λ z : pr1 P, pr1 h z,, eqtohomot (maponpaths pr1 q) z),,
       make_poset_enrichment_coequalizer_is_coequalizer_subproof0 w P h q)
      · poset_enrichment_coequalizer_to_equalizer EEC f g) w P h q
     · precomp_arr E' w
         (enriched_coequalizer_cocone_in E' f g
            make_poset_enrichment_coequalizer_cocone)) x0 = 
    h x0)


Going to execute:
intros z

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧
  q : h · precomp_arr E' w f = h · precomp_arr E' w g
  z : pr1hSet
        ?X633@{__:=?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0; __:=?M0; __:=?M0; __:=?M0}
  ============================
   (((λ (w : C) (P : poset_sym_mon_closed_cat)
      (h : poset_sym_mon_closed_cat ⟦ P, E' ⦃ y, w ⦄ ⟧)
      (q : h · precomp_arr E' w f = h · precomp_arr E' w g),
      ((λ z : pr1 P, pr1 h z,, eqtohomot (maponpaths pr1 q) z),,
       make_poset_enrichment_coequalizer_is_coequalizer_subproof0 w P h q)
      · poset_enrichment_coequalizer_to_equalizer EEC f g) w P h q
     · precomp_arr E' w
         (enriched_coequalizer_cocone_in E' f g
            make_poset_enrichment_coequalizer_cocone)) z = 
    h z)


Going to execute:
apply poset_enrichment_obj_from_coequalizer_in

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  ============================
   (∑ a : enriched_coequalizer_cocone E' f g,
    is_coequalizer_enriched E' f g a)


Going to execute:
<coq-core.plugins.ltac::simple_refine@0> $1
Evaluated term: poset_enrichment_obj_from_coequalizer_in

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  ============================
   (enriched_coequalizer_cocone E' f g)


Going to execute:
<coq-core.plugins.ltac::exact@0> $1

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  ============================
   ((λ a : enriched_coequalizer_cocone E' f g,
     is_coequalizer_enriched E' f g a)
      (make_poset_enrichment_coequalizer_cocone EEC f g))


Going to execute:
<coq-core.plugins.ltac::exact@0> $1

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : enrichment_coequalizers E'
  x : ob C
  y : ob C
  z : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  Eq := Equalizers_category_of_posets (E' ⦃ y, z ⦄) 
          (E' ⦃ x, z ⦄) (precomp_arr E' z f) (precomp_arr E' z g)
     : Equalizer (precomp_arr E' z f) (precomp_arr E' z g)
  Eq_pr := EqualizerArrow Eq : category_of_posets ⟦ Eq, E' ⦃ y, z ⦄ ⟧
  Eq_path := EqualizerEqAr Eq
          : Eq_pr · precomp_arr E' z f = Eq_pr · precomp_arr E' z g
  h : C ⟦ y, z ⟧
  q : f · h = g · h
  ============================
   (enriched_coequalizer_cocone_in E' f g (pr1 (EEC x y f g))
    · poset_to_underlying_coequalizer_map h q = h)


Going to execute:
<coq-core.plugins.ltac::exact@0> $1

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : enrichment_coequalizers E'
  x : ob C
  y : ob C
  z : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  Eq := Equalizers_category_of_posets (E' ⦃ y, z ⦄) 
          (E' ⦃ x, z ⦄) (precomp_arr E' z f) (precomp_arr E' z g)
     : Equalizer (precomp_arr E' z f) (precomp_arr E' z g)
  Eq_pr := EqualizerArrow Eq : category_of_posets ⟦ Eq, E' ⦃ y, z ⦄ ⟧
  Eq_path := EqualizerEqAr Eq
          : Eq_pr · precomp_arr E' z f = Eq_pr · precomp_arr E' z g
  h : C ⟦ y, z ⟧
  q : f · h = g · h
  ============================
   (CoequalizerOut (underlying_Coequalizer E' f g (pr2 (EEC x y f g))) z h q =
    poset_to_underlying_coequalizer_map h q)


Going to execute:
simple_rapply p
Evaluated term: (pr2
                   (EqualizerIn
                      (is_coequalizer_enriched_to_Equalizer E' f g
                         (pr2 (EEC x y f g)) z) Eq Eq_pr Eq_path) 
                   (h₁,, q₁) (h₂,, q₂) ph)

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : enrichment_coequalizers E'
  x : ob C
  y : ob C
  z : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  Eq := Equalizers_category_of_posets (E' ⦃ y, z ⦄) 
          (E' ⦃ x, z ⦄) (precomp_arr E' z f) (precomp_arr E' z g)
     : Equalizer (precomp_arr E' z f) (precomp_arr E' z g)
  Eq_pr := EqualizerArrow Eq : category_of_posets ⟦ Eq, E' ⦃ y, z ⦄ ⟧
  Eq_path := EqualizerEqAr Eq
          : Eq_pr · precomp_arr E' z f = Eq_pr · precomp_arr E' z g
  h : C ⟦ y, z ⟧
  q : f · h = g · h
  ============================
   (CoequalizerOut (underlying_Coequalizer E' f g (pr2 (EEC x y f g))) z h q =
    poset_to_underlying_coequalizer_map h q)


Going to execute:
fun p =>
  simple refine p ||
    simple refine (p _) ||
      simple refine (p _ _) ||
...                              simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _)
                               || simple refine
                               (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)

TcDebug (1) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : enrichment_coequalizers E'
  x : ob C
  y : ob C
  z : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  Eq := Equalizers_category_of_posets (E' ⦃ y, z ⦄) 
          (E' ⦃ x, z ⦄) (precomp_arr E' z f) (precomp_arr E' z g)
     : Equalizer (precomp_arr E' z f) (precomp_arr E' z g)
  Eq_pr := EqualizerArrow Eq : category_of_posets ⟦ Eq, E' ⦃ y, z ⦄ ⟧
  Eq_path := EqualizerEqAr Eq
          : Eq_pr · precomp_arr E' z f = Eq_pr · precomp_arr E' z g
  h : C ⟦ y, z ⟧
  q : f · h = g · h
  ============================
   (CoequalizerOut (underlying_Coequalizer E' f g (pr2 (EEC x y f g))) z h q =
    poset_to_underlying_coequalizer_map h q)


Going to execute:
simple refine p ||
  simple refine (p _) ||
    simple refine (p _ _) ||
      simple refine (p _ _ _) ||
        simple refine (p _ _ _ _) ||
          simple refine (p _ _ _ _ _) ||
            simple refine (p _ _ _ _ _ _) ||
              simple refine (p _ _ _ _ _ _ _) ||
                simple refine (p _ _ _ _ _ _ _ _) ||
                  simple refine (p _ _ _ _ _ _ _ _ _) ||
                    simple refine (p _ _ _ _ _ _ _ _ _ _) ||
                      simple refine (p _ _ _ _ _ _ _ _ _ _ _) ||
                        simple refine (p _ _ _ _ _ _ _ _ _ _ _ _) ||
                          simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
                            simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
                              simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)

TcDebug (1) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : enrichment_coequalizers E'
  x : ob C
  y : ob C
  z : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  Eq := Equalizers_category_of_posets (E' ⦃ y, z ⦄) 
          (E' ⦃ x, z ⦄) (precomp_arr E' z f) (precomp_arr E' z g)
     : Equalizer (precomp_arr E' z f) (precomp_arr E' z g)
  Eq_pr := EqualizerArrow Eq : category_of_posets ⟦ Eq, E' ⦃ y, z ⦄ ⟧
  Eq_path := EqualizerEqAr Eq
          : Eq_pr · precomp_arr E' z f = Eq_pr · precomp_arr E' z g
  h : C ⟦ y, z ⟧
  q : f · h = g · h
  ============================
   (CoequalizerOut (underlying_Coequalizer E' f g (pr2 (EEC x y f g))) z h q =
    poset_to_underlying_coequalizer_map h q)


Going to execute:
simple refine p
Level 1: evaluation returns
simple refine p ||
  simple refine (p _) ||
    simple refine (p _ _) ||
      simple refine (p _ _ _) ||
        simple refine (p _ _ _ _) ||
          simple refine (p _ _ _ _ _) ||
            simple refine (p _ _ _ _ _ _) ||
              simple refine (p _ _ _ _ _ _ _) ||
                simple refine (p _ _ _ _ _ _ _ _) ||
                  simple refine (p _ _ _ _ _ _ _ _ _) ||
                    simple refine (p _ _ _ _ _ _ _ _ _ _) ||
                      simple refine (p _ _ _ _ _ _ _ _ _ _ _) ||
                        simple refine (p _ _ _ _ _ _ _ _ _ _ _ _) ||
                          simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
                            simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
                              simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)
where
p := underlying_Coequalizer_arr_eq
of type
uconstr of type tacvalue


TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : enrichment_coequalizers E'
  x : ob C
  y : ob C
  z : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  Eq := Equalizers_category_of_posets (E' ⦃ y, z ⦄) 
          (E' ⦃ x, z ⦄) (precomp_arr E' z f) (precomp_arr E' z g)
     : Equalizer (precomp_arr E' z f) (precomp_arr E' z g)
  Eq_pr := EqualizerArrow Eq : category_of_posets ⟦ Eq, E' ⦃ y, z ⦄ ⟧
  Eq_path := EqualizerEqAr Eq
          : Eq_pr · precomp_arr E' z f = Eq_pr · precomp_arr E' z g
  h : C ⟦ y, z ⟧
  q : f · h = g · h
  ============================
   (CoequalizerOut (underlying_Coequalizer E' f g (pr2 (EEC x y f g))) z h q =
    poset_to_underlying_coequalizer_map h q)


Going to execute:
<coq-core.plugins.ltac::simple_refine@0> $1

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : enrichment_coequalizers E'
  x : ob C
  y : ob C
  z : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  Eq := Equalizers_category_of_posets (E' ⦃ y, z ⦄) 
          (E' ⦃ x, z ⦄) (precomp_arr E' z f) (precomp_arr E' z g)
     : Equalizer (precomp_arr E' z f) (precomp_arr E' z g)
  Eq_pr := EqualizerArrow Eq : category_of_posets ⟦ Eq, E' ⦃ y, z ⦄ ⟧
  Eq_path := EqualizerEqAr Eq
          : Eq_pr · precomp_arr E' z f = Eq_pr · precomp_arr E' z g
  h : C ⟦ y, z ⟧
  q : f · h = g · h
  ============================
   (CoequalizerOut (underlying_Coequalizer E' f g (pr2 (EEC x y f g))) z h q =
    poset_to_underlying_coequalizer_map h q)


Going to execute:
simple refine (p _) ||
  simple refine (p _ _) ||
    simple refine (p _ _ _) ||
      simple refine (p _ _ _ _) ||
        simple refine (p _ _ _ _ _) ||
          simple refine (p _ _ _ _ _ _) ||
            simple refine (p _ _ _ _ _ _ _) ||
              simple refine (p _ _ _ _ _ _ _ _) ||
                simple refine (p _ _ _ _ _ _ _ _ _) ||
                  simple refine (p _ _ _ _ _ _ _ _ _ _) ||
                    simple refine (p _ _ _ _ _ _ _ _ _ _ _) ||
                      simple refine (p _ _ _ _ _ _ _ _ _ _ _ _) ||
                        simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
                          simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
                            simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)
Level 0: In environment
C : category
E : poset_enrichment C
E' := make_enrichment_over_poset C E : enrichment C poset_sym_mon_closed_cat
EEC : enrichment_coequalizers E'
x, y, z : C
f, g : C ⟦ x, y ⟧
Eq := Equalizers_category_of_posets (E' ⦃ y, z ⦄) 
        (E' ⦃ x, z ⦄) (precomp_arr E' z f) (precomp_arr E' z g)
 : Equalizer (precomp_arr E' z f) (precomp_arr E' z g)
Eq_pr := EqualizerArrow Eq : category_of_posets ⟦ Eq, E' ⦃ y, z ⦄ ⟧
Eq_path := EqualizerEqAr Eq
 : Eq_pr · precomp_arr E' z f = Eq_pr · precomp_arr E' z g
h : C ⟦ y, z ⟧
q : f · h = g · h
The term "underlying_Coequalizer_arr_eq" has type
 "∏ (E0 : enrichment ?C ?V) (x0 y0 : ?C) (f0 g0 : ?C ⟦ x0, y0 ⟧)
  (a : enriched_coequalizer_cocone E0 f0 g0),
  is_coequalizer_enriched E0 f0 g0 a
  → ∏ (w : ?C) (h₁ h₂ : ?C ⟦ a, w ⟧),
    enriched_coequalizer_cocone_in E0 f0 g0 a · h₁ =
    enriched_coequalizer_cocone_in E0 f0 g0 a · h₂ → 
    h₁ = h₂" while it is expected to have type
 "CoequalizerOut (underlying_Coequalizer E' f g (pr2 (EEC x y f g))) z h q =
  poset_to_underlying_coequalizer_map h q".
Level 0: In environment
C : category
E : poset_enrichment C
E' := make_enrichment_over_poset C E : enrichment C poset_sym_mon_closed_cat
EEC : enrichment_coequalizers E'
x, y, z : C
f, g : C ⟦ x, y ⟧
Eq := Equalizers_category_of_posets (E' ⦃ y, z ⦄) 
        (E' ⦃ x, z ⦄) (precomp_arr E' z f) (precomp_arr E' z g)
 : Equalizer (precomp_arr E' z f) (precomp_arr E' z g)
Eq_pr := EqualizerArrow Eq : category_of_posets ⟦ Eq, E' ⦃ y, z ⦄ ⟧
Eq_path := EqualizerEqAr Eq
 : Eq_pr · precomp_arr E' z f = Eq_pr · precomp_arr E' z g
h : C ⟦ y, z ⟧
q : f · h = g · h
The term "underlying_Coequalizer_arr_eq" has type
 "∏ (E0 : enrichment ?C ?V) (x0 y0 : ?C) (f0 g0 : ?C ⟦ x0, y0 ⟧)
  (a : enriched_coequalizer_cocone E0 f0 g0),
  is_coequalizer_enriched E0 f0 g0 a
  → ∏ (w : ?C) (h₁ h₂ : ?C ⟦ a, w ⟧),
    enriched_coequalizer_cocone_in E0 f0 g0 a · h₁ =
    enriched_coequalizer_cocone_in E0 f0 g0 a · h₂ → 
    h₁ = h₂" while it is expected to have type
 "CoequalizerOut (underlying_Coequalizer E' f g (pr2 (EEC x y f g))) z h q =
  poset_to_underlying_coequalizer_map h q".

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : enrichment_coequalizers E'
  x : ob C
  y : ob C
  z : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  Eq := Equalizers_category_of_posets (E' ⦃ y, z ⦄) 
          (E' ⦃ x, z ⦄) (precomp_arr E' z f) (precomp_arr E' z g)
     : Equalizer (precomp_arr E' z f) (precomp_arr E' z g)
  Eq_pr := EqualizerArrow Eq : category_of_posets ⟦ Eq, E' ⦃ y, z ⦄ ⟧
  Eq_path := EqualizerEqAr Eq
          : Eq_pr · precomp_arr E' z f = Eq_pr · precomp_arr E' z g
  h : C ⟦ y, z ⟧
  q : f · h = g · h
  ============================
   (CoequalizerOut (underlying_Coequalizer E' f g (pr2 (EEC x y f g))) z h q =
    poset_to_underlying_coequalizer_map h q)


Going to execute:
simple refine (p _)

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : enrichment_coequalizers E'
  x : ob C
  y : ob C
  z : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  Eq := Equalizers_category_of_posets (E' ⦃ y, z ⦄) 
          (E' ⦃ x, z ⦄) (precomp_arr E' z f) (precomp_arr E' z g)
     : Equalizer (precomp_arr E' z f) (precomp_arr E' z g)
  Eq_pr := EqualizerArrow Eq : category_of_posets ⟦ Eq, E' ⦃ y, z ⦄ ⟧
  Eq_path := EqualizerEqAr Eq
          : Eq_pr · precomp_arr E' z f = Eq_pr · precomp_arr E' z g
  h : C ⟦ y, z ⟧
  q : f · h = g · h
  ============================
   (CoequalizerOut (underlying_Coequalizer E' f g (pr2 (EEC x y f g))) z h q =
    poset_to_underlying_coequalizer_map h q)


Going to execute:
<coq-core.plugins.ltac::simple_refine@0> $1

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : enrichment_coequalizers E'
  x : ob C
  y : ob C
  z : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  Eq := Equalizers_category_of_posets (E' ⦃ y, z ⦄) 
          (E' ⦃ x, z ⦄) (precomp_arr E' z f) (precomp_arr E' z g)
     : Equalizer (precomp_arr E' z f) (precomp_arr E' z g)
  Eq_pr := EqualizerArrow Eq : category_of_posets ⟦ Eq, E' ⦃ y, z ⦄ ⟧
  Eq_path := EqualizerEqAr Eq
          : Eq_pr · precomp_arr E' z f = Eq_pr · precomp_arr E' z g
  h : C ⟦ y, z ⟧
  q : f · h = g · h
  ============================
   (CoequalizerOut (underlying_Coequalizer E' f g (pr2 (EEC x y f g))) z h q =
    poset_to_underlying_coequalizer_map h q)


Going to execute:
simple refine (p _ _) ||
  simple refine (p _ _ _) ||
    simple refine (p _ _ _ _) ||
      simple refine (p _ _ _ _ _) ||
        simple refine (p _ _ _ _ _ _) ||
          simple refine (p _ _ _ _ _ _ _) ||
            simple refine (p _ _ _ _ _ _ _ _) ||
              simple refine (p _ _ _ _ _ _ _ _ _) ||
                simple refine (p _ _ _ _ _ _ _ _ _ _) ||
                  simple refine (p _ _ _ _ _ _ _ _ _ _ _) ||
                    simple refine (p _ _ _ _ _ _ _ _ _ _ _ _) ||
                      simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
                        simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
                          simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)
Level 0: In environment
C : category
E : poset_enrichment C
E' := make_enrichment_over_poset C E : enrichment C poset_sym_mon_closed_cat
EEC : enrichment_coequalizers E'
x, y, z : C
f, g : C ⟦ x, y ⟧
Eq := Equalizers_category_of_posets (E' ⦃ y, z ⦄) 
        (E' ⦃ x, z ⦄) (precomp_arr E' z f) (precomp_arr E' z g)
 : Equalizer (precomp_arr E' z f) (precomp_arr E' z g)
Eq_pr := EqualizerArrow Eq : category_of_posets ⟦ Eq, E' ⦃ y, z ⦄ ⟧
Eq_path := EqualizerEqAr Eq
 : Eq_pr · precomp_arr E' z f = Eq_pr · precomp_arr E' z g
h : C ⟦ y, z ⟧
q : f · h = g · h
The term "@underlying_Coequalizer_arr_eq ?V ?C ?E" has type
 "∏ (x0 y0 : ?C) (f0 g0 : ?C ⟦ x0, y0 ⟧)
  (a : enriched_coequalizer_cocone ?E f0 g0),
  is_coequalizer_enriched ?E f0 g0 a
  → ∏ (w : ?C) (h₁ h₂ : ?C ⟦ a, w ⟧),
    enriched_coequalizer_cocone_in ?E f0 g0 a · h₁ =
    enriched_coequalizer_cocone_in ?E f0 g0 a · h₂ → 
    h₁ = h₂" while it is expected to have type
 "CoequalizerOut (underlying_Coequalizer E' f g (pr2 (EEC x y f g))) z h q =
  poset_to_underlying_coequalizer_map h q".
Level 0: In environment
C : category
E : poset_enrichment C
E' := make_enrichment_over_poset C E : enrichment C poset_sym_mon_closed_cat
EEC : enrichment_coequalizers E'
x, y, z : C
f, g : C ⟦ x, y ⟧
Eq := Equalizers_category_of_posets (E' ⦃ y, z ⦄) 
