split

meta-introspector · Feb 1, 2024 · a564677 · a564677
1 parent 6bc8bdc
commit a564677
Show file tree

Hide file tree

Showing 134 changed files with 392,636 additions and 0 deletions.
diff --git a/2024/02/01/TASK5aa b/2024/02/01/TASK5aa
diff --git a/2024/02/01/TASK5ab b/2024/02/01/TASK5ab
diff --git a/2024/02/01/TASK5ac b/2024/02/01/TASK5ac
diff --git a/2024/02/01/TASK5ad b/2024/02/01/TASK5ad
diff --git a/2024/02/01/TASK5ae b/2024/02/01/TASK5ae
diff --git a/2024/02/01/TASK5af b/2024/02/01/TASK5af
diff --git a/2024/02/01/TASK5ag b/2024/02/01/TASK5ag
diff --git a/2024/02/01/TASK5ah b/2024/02/01/TASK5ah
diff --git a/2024/02/01/TASK5ai b/2024/02/01/TASK5ai
diff --git a/2024/02/01/TASK5aj b/2024/02/01/TASK5aj
diff --git a/2024/02/01/TASK5ak b/2024/02/01/TASK5ak
diff --git a/2024/02/01/TASK5al b/2024/02/01/TASK5al
diff --git a/2024/02/01/TASK5am b/2024/02/01/TASK5am
diff --git a/2024/02/01/TASK5an b/2024/02/01/TASK5an
diff --git a/2024/02/01/TASK5ao b/2024/02/01/TASK5ao
diff --git a/2024/02/01/TASK5ap b/2024/02/01/TASK5ap
diff --git a/2024/02/01/TASK5aq b/2024/02/01/TASK5aq
diff --git a/2024/02/01/TASK5ar b/2024/02/01/TASK5ar
diff --git a/2024/02/01/TASK5as b/2024/02/01/TASK5as
diff --git a/2024/02/01/TASK5at b/2024/02/01/TASK5at
diff --git a/2024/02/01/TASK5au b/2024/02/01/TASK5au
diff --git a/2024/02/01/TASK5av b/2024/02/01/TASK5av
diff --git a/2024/02/01/TASK5aw b/2024/02/01/TASK5aw
diff --git a/2024/02/01/TASK5ax b/2024/02/01/TASK5ax
diff --git a/2024/02/01/TASK5ay b/2024/02/01/TASK5ay
diff --git a/2024/02/01/TASK5az b/2024/02/01/TASK5az
diff --git a/2024/02/01/TASK5ba b/2024/02/01/TASK5ba
diff --git a/2024/02/01/TASK5bb b/2024/02/01/TASK5bb
diff --git a/2024/02/01/TASK5bc b/2024/02/01/TASK5bc
diff --git a/2024/02/01/TASK5bd b/2024/02/01/TASK5bd
diff --git a/2024/02/01/TASK5be b/2024/02/01/TASK5be
diff --git a/2024/02/01/TASK5bf b/2024/02/01/TASK5bf
diff --git a/2024/02/01/TASK5bg b/2024/02/01/TASK5bg
diff --git a/2024/02/01/TASK5bh b/2024/02/01/TASK5bh
diff --git a/2024/02/01/TASK5bi b/2024/02/01/TASK5bi
diff --git a/2024/02/01/TASK5bj b/2024/02/01/TASK5bj
diff --git a/2024/02/01/TASK5bk b/2024/02/01/TASK5bk
diff --git a/2024/02/01/TASK5bl b/2024/02/01/TASK5bl
diff --git a/2024/02/01/TASK5bm b/2024/02/01/TASK5bm
diff --git a/2024/02/01/TASK5bn b/2024/02/01/TASK5bn
diff --git a/2024/02/01/TASK5bo b/2024/02/01/TASK5bo
diff --git a/2024/02/01/TASK5bp b/2024/02/01/TASK5bp
diff --git a/2024/02/01/TASK5bq b/2024/02/01/TASK5bq
diff --git a/2024/02/01/TASK5br b/2024/02/01/TASK5br
diff --git a/2024/02/01/TASK5bs b/2024/02/01/TASK5bs
diff --git a/2024/02/01/TASK5bt b/2024/02/01/TASK5bt
diff --git a/2024/02/01/TASK5bu b/2024/02/01/TASK5bu
diff --git a/2024/02/01/TASK5bv b/2024/02/01/TASK5bv
diff --git a/2024/02/01/TASK5bw b/2024/02/01/TASK5bw
diff --git a/2024/02/01/TASK5bx b/2024/02/01/TASK5bx
diff --git a/2024/02/01/TASK5by b/2024/02/01/TASK5by
diff --git a/2024/02/01/TASK5bz b/2024/02/01/TASK5bz
diff --git a/2024/02/01/TASK5ca b/2024/02/01/TASK5ca
diff --git a/2024/02/01/TASK5cb b/2024/02/01/TASK5cb
diff --git a/2024/02/01/TASK5cc b/2024/02/01/TASK5cc
diff --git a/2024/02/01/TASK5cd b/2024/02/01/TASK5cd
diff --git a/2024/02/01/TASK5ce b/2024/02/01/TASK5ce
diff --git a/2024/02/01/TASK5cf b/2024/02/01/TASK5cf
diff --git a/2024/02/01/TASK5cg b/2024/02/01/TASK5cg
diff --git a/2024/02/01/TASK5ch b/2024/02/01/TASK5ch
diff --git a/2024/02/01/TASK5ci b/2024/02/01/TASK5ci
diff --git a/2024/02/01/TASK5cj b/2024/02/01/TASK5cj
diff --git a/2024/02/01/TASK5ck b/2024/02/01/TASK5ck
diff --git a/2024/02/01/TASK5cl b/2024/02/01/TASK5cl
diff --git a/2024/02/01/TASK5cm b/2024/02/01/TASK5cm
diff --git a/2024/02/01/TASK5cn b/2024/02/01/TASK5cn
diff --git a/2024/02/01/TASK5co b/2024/02/01/TASK5co
diff --git a/2024/02/01/TASK5cp b/2024/02/01/TASK5cp
diff --git a/2024/02/01/TASK5cq b/2024/02/01/TASK5cq
diff --git a/2024/02/01/TASK5cr b/2024/02/01/TASK5cr
diff --git a/2024/02/01/TASK5cs b/2024/02/01/TASK5cs
diff --git a/2024/02/01/TASK5ct b/2024/02/01/TASK5ct
diff --git a/2024/02/01/TASK5cu b/2024/02/01/TASK5cu
diff --git a/2024/02/01/TASK5cv b/2024/02/01/TASK5cv
diff --git a/2024/02/01/TASK5cw b/2024/02/01/TASK5cw
diff --git a/2024/02/01/TASK5cx b/2024/02/01/TASK5cx
diff --git a/2024/02/01/TASK5cy b/2024/02/01/TASK5cy
diff --git a/2024/02/01/TASK5cz b/2024/02/01/TASK5cz
diff --git a/2024/02/01/TASK5da b/2024/02/01/TASK5da
diff --git a/2024/02/01/TASK5db b/2024/02/01/TASK5db
diff --git a/2024/02/01/TASK5dc b/2024/02/01/TASK5dc
diff --git a/2024/02/01/TASK5dd b/2024/02/01/TASK5dd
diff --git a/2024/02/01/TASK5de b/2024/02/01/TASK5de
diff --git a/2024/02/01/TASK5df b/2024/02/01/TASK5df
diff --git a/2024/02/01/TASK5dg b/2024/02/01/TASK5dg
diff --git a/2024/02/01/TASK5dh b/2024/02/01/TASK5dh
diff --git a/2024/02/01/TASK5di b/2024/02/01/TASK5di
diff --git a/2024/02/01/TASK5dj b/2024/02/01/TASK5dj
diff --git a/2024/02/01/TASK5dk b/2024/02/01/TASK5dk
diff --git a/2024/02/01/TASK5dl b/2024/02/01/TASK5dl
diff --git a/2024/02/01/TASK5dm b/2024/02/01/TASK5dm
diff --git a/2024/02/01/TASK5dn b/2024/02/01/TASK5dn
diff --git a/2024/02/01/TASK5do b/2024/02/01/TASK5do
diff --git a/2024/02/01/TASK5dp b/2024/02/01/TASK5dp
diff --git a/2024/02/01/TASK5dq b/2024/02/01/TASK5dq
diff --git a/2024/02/01/TASK5dr b/2024/02/01/TASK5dr
diff --git a/2024/02/01/TASK5ds b/2024/02/01/TASK5ds
diff --git a/2024/02/01/TASK5dt b/2024/02/01/TASK5dt
diff --git a/2024/02/01/TASK5du b/2024/02/01/TASK5du
diff --git a/2024/02/01/TASK5dv b/2024/02/01/TASK5dv
diff --git a/2024/02/01/TASK5dw b/2024/02/01/TASK5dw
diff --git a/2024/02/01/TASK5dx b/2024/02/01/TASK5dx
diff --git a/2024/02/01/TASK5dy b/2024/02/01/TASK5dy
diff --git a/2024/02/01/TASK5dz b/2024/02/01/TASK5dz
diff --git a/2024/02/01/TASK5ea b/2024/02/01/TASK5ea
diff --git a/2024/02/01/TASK5eb b/2024/02/01/TASK5eb
diff --git a/2024/02/01/TASK5ec b/2024/02/01/TASK5ec
diff --git a/2024/02/01/TASK5ed b/2024/02/01/TASK5ed
diff --git a/2024/02/01/TASK5ee b/2024/02/01/TASK5ee
diff --git a/2024/02/01/TASK5ef b/2024/02/01/TASK5ef
diff --git a/2024/02/01/TASK5eg b/2024/02/01/TASK5eg
diff --git a/2024/02/01/TASK5eh b/2024/02/01/TASK5eh
diff --git a/2024/02/01/TASK5ei b/2024/02/01/TASK5ei
diff --git a/2024/02/01/TASK5ej b/2024/02/01/TASK5ej
diff --git a/2024/02/01/TASK5ek b/2024/02/01/TASK5ek
diff --git a/2024/02/01/TASK5el b/2024/02/01/TASK5el
diff --git a/2024/02/01/TASK5em b/2024/02/01/TASK5em
diff --git a/2024/02/01/TASK5en b/2024/02/01/TASK5en
diff --git a/2024/02/01/TASK5eo b/2024/02/01/TASK5eo
diff --git a/2024/02/01/TASK5ep b/2024/02/01/TASK5ep
diff --git a/2024/02/01/TASK5eq b/2024/02/01/TASK5eq
diff --git a/2024/02/01/TASK5er b/2024/02/01/TASK5er
diff --git a/2024/02/01/TASK5es b/2024/02/01/TASK5es
diff --git a/2024/02/01/TASK5et b/2024/02/01/TASK5et
diff --git a/2024/02/01/TASK5eu b/2024/02/01/TASK5eu
diff --git a/2024/02/01/TASK5ev b/2024/02/01/TASK5ev
diff --git a/2024/02/01/TASK5ew b/2024/02/01/TASK5ew
diff --git a/2024/02/01/TASK5ex b/2024/02/01/TASK5ex
diff --git a/2024/02/01/TASK5ey b/2024/02/01/TASK5ey
diff --git a/2024/02/01/TASK5ez b/2024/02/01/TASK5ez
diff --git a/2024/02/01/TASK5fa b/2024/02/01/TASK5fa
@@ -0,0 +1,399 @@
+E' := make_enrichment_over_struct P C E
+ : enrichment C (sym_mon_closed_cat_of_hset_struct P)
+J : UU
+HP : hset_struct_type_prod P J
+EBC : structure_enrichment_coprod
+ys : J → C
+The term "make_is_coprod_enriched ?E ?D" has type
+ "∏ (a : enriched_coprod_cocone ?E ?D)
+  (sum : ∏ (w : ?C) (v : ?V),
+         (∏ j : ?J, ?V ⟦ v, ?E ⦃ ?D j, w ⦄ ⟧) → ?V ⟦ v, ?E ⦃ a, w ⦄ ⟧),
+  (∏ (w : ?C) (v : ?V) (f : ∏ j : ?J, ?V ⟦ v, ?E ⦃ ?D j, w ⦄ ⟧) 
+   (j : ?J),
+   sum w v f · precomp_arr ?E w (enriched_coprod_cocone_in ?E ?D a j) = f j)
+  → (∏ (w : ?C) (v : ?V) (φ₁ φ₂ : ?V ⟦ v, ?E ⦃ a, w ⦄ ⟧),
+     (∏ j : ?J,
+      φ₁ · precomp_arr ?E w (enriched_coprod_cocone_in ?E ?D a j) =
+      φ₂ · precomp_arr ?E w (enriched_coprod_cocone_in ?E ?D a j)) → 
+     φ₁ = φ₂) → is_coprod_enriched ?E ?D a" while it is expected to have type
+ "is_coprod_enriched E' ys make_structure_enriched_coprod_cocone".
+Level 0: In environment
+P : hset_cartesian_closed_struct
+C : category
+E : struct_enrichment P C
+E' := make_enrichment_over_struct P C E
+ : enrichment C (sym_mon_closed_cat_of_hset_struct P)
+J : UU
+HP : hset_struct_type_prod P J
+EBC : structure_enrichment_coprod
+ys : J → C
+The term "make_is_coprod_enriched ?E ?D" has type
+ "∏ (a : enriched_coprod_cocone ?E ?D)
+  (sum : ∏ (w : ?C) (v : ?V),
+         (∏ j : ?J, ?V ⟦ v, ?E ⦃ ?D j, w ⦄ ⟧) → ?V ⟦ v, ?E ⦃ a, w ⦄ ⟧),
+  (∏ (w : ?C) (v : ?V) (f : ∏ j : ?J, ?V ⟦ v, ?E ⦃ ?D j, w ⦄ ⟧) 
+   (j : ?J),
+   sum w v f · precomp_arr ?E w (enriched_coprod_cocone_in ?E ?D a j) = f j)
+  → (∏ (w : ?C) (v : ?V) (φ₁ φ₂ : ?V ⟦ v, ?E ⦃ a, w ⦄ ⟧),
+     (∏ j : ?J,
+      φ₁ · precomp_arr ?E w (enriched_coprod_cocone_in ?E ?D a j) =
+      φ₂ · precomp_arr ?E w (enriched_coprod_cocone_in ?E ?D a j)) → 
+     φ₁ = φ₂) → is_coprod_enriched ?E ?D a" while it is expected to have type
+ "is_coprod_enriched E' ys make_structure_enriched_coprod_cocone".
+
+TcDebug (0) > 
+Goal:
+
+  P : hset_cartesian_closed_struct
+  C : category
+  E : struct_enrichment P C
+  E' := make_enrichment_over_struct P C E
+     : enrichment C (sym_mon_closed_cat_of_hset_struct P)
+  J : UU
+  HP : hset_struct_type_prod P J
+  EBC : structure_enrichment_coprod
+  ys : J → C
+  ============================
+   (is_coprod_enriched E' ys make_structure_enriched_coprod_cocone)
+
+
+Going to execute:
+simple refine (p _ _ _ _)
+
+TcDebug (0) > 
+Goal:
+
+  P : hset_cartesian_closed_struct
+  C : category
+  E : struct_enrichment P C
+  E' := make_enrichment_over_struct P C E
+     : enrichment C (sym_mon_closed_cat_of_hset_struct P)
+  J : UU
+  HP : hset_struct_type_prod P J
+  EBC : structure_enrichment_coprod
+  ys : J → C
+  ============================
+   (is_coprod_enriched E' ys make_structure_enriched_coprod_cocone)
+
+
+Going to execute:
+<coq-core.plugins.ltac::simple_refine@0> $1
+
+TcDebug (0) > 
+Goal:
+
+  P : hset_cartesian_closed_struct
+  C : category
+  E : struct_enrichment P C
+  E' := make_enrichment_over_struct P C E
+     : enrichment C (sym_mon_closed_cat_of_hset_struct P)
+  J : UU
+  HP : hset_struct_type_prod P J
+  EBC : structure_enrichment_coprod
+  ys : J → C
+  ============================
+   (is_coprod_enriched E' ys make_structure_enriched_coprod_cocone)
+
+
+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 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)
+Level 0: In environment
+P : hset_cartesian_closed_struct
+C : category
+E : struct_enrichment P C
+E' := make_enrichment_over_struct P C E
+ : enrichment C (sym_mon_closed_cat_of_hset_struct P)
+J : UU
+HP : hset_struct_type_prod P J
+EBC : structure_enrichment_coprod
+ys : J → C
+The term "make_is_coprod_enriched ?E ?D ?a" has type
+ "∏
+  sum : ∏ (w : ?C) (v : ?V),
+        (∏ j : ?J, ?V ⟦ v, ?E ⦃ ?D j, w ⦄ ⟧) → ?V ⟦ v, ?E ⦃ ?a, w ⦄ ⟧,
+  (∏ (w : ?C) (v : ?V) (f : ∏ j : ?J, ?V ⟦ v, ?E ⦃ ?D j, w ⦄ ⟧) 
+   (j : ?J),
+   sum w v f · precomp_arr ?E w (enriched_coprod_cocone_in ?E ?D ?a j) = f j)
+  → (∏ (w : ?C) (v : ?V) (φ₁ φ₂ : ?V ⟦ v, ?E ⦃ ?a, w ⦄ ⟧),
+     (∏ j : ?J,
+      φ₁ · precomp_arr ?E w (enriched_coprod_cocone_in ?E ?D ?a j) =
+      φ₂ · precomp_arr ?E w (enriched_coprod_cocone_in ?E ?D ?a j)) → 
+     φ₁ = φ₂) → is_coprod_enriched ?E ?D ?a"
+while it is expected to have type
+ "is_coprod_enriched E' ys make_structure_enriched_coprod_cocone".
+Level 0: In environment
+P : hset_cartesian_closed_struct
+C : category
+E : struct_enrichment P C
+E' := make_enrichment_over_struct P C E
+ : enrichment C (sym_mon_closed_cat_of_hset_struct P)
+J : UU
+HP : hset_struct_type_prod P J
+EBC : structure_enrichment_coprod
+ys : J → C
+The term "make_is_coprod_enriched ?E ?D ?a" has type
+ "∏
+  sum : ∏ (w : ?C) (v : ?V),
+        (∏ j : ?J, ?V ⟦ v, ?E ⦃ ?D j, w ⦄ ⟧) → ?V ⟦ v, ?E ⦃ ?a, w ⦄ ⟧,
+  (∏ (w : ?C) (v : ?V) (f : ∏ j : ?J, ?V ⟦ v, ?E ⦃ ?D j, w ⦄ ⟧) 
+   (j : ?J),
+   sum w v f · precomp_arr ?E w (enriched_coprod_cocone_in ?E ?D ?a j) = f j)
+  → (∏ (w : ?C) (v : ?V) (φ₁ φ₂ : ?V ⟦ v, ?E ⦃ ?a, w ⦄ ⟧),
+     (∏ j : ?J,
+      φ₁ · precomp_arr ?E w (enriched_coprod_cocone_in ?E ?D ?a j) =
+      φ₂ · precomp_arr ?E w (enriched_coprod_cocone_in ?E ?D ?a j)) → 
+     φ₁ = φ₂) → is_coprod_enriched ?E ?D ?a"
+while it is expected to have type
+ "is_coprod_enriched E' ys make_structure_enriched_coprod_cocone".
+
+TcDebug (0) > 
+Goal:
+
+  P : hset_cartesian_closed_struct
+  C : category
+  E : struct_enrichment P C
+  E' := make_enrichment_over_struct P C E
+     : enrichment C (sym_mon_closed_cat_of_hset_struct P)
+  J : UU
+  HP : hset_struct_type_prod P J
+  EBC : structure_enrichment_coprod
+  ys : J → C
+  ============================
+   (is_coprod_enriched E' ys make_structure_enriched_coprod_cocone)
+
+
+Going to execute:
+simple refine (p _ _ _ _ _)
+
+TcDebug (0) > 
+Goal:
+
+  P : hset_cartesian_closed_struct
+  C : category
+  E : struct_enrichment P C
+  E' := make_enrichment_over_struct P C E
+     : enrichment C (sym_mon_closed_cat_of_hset_struct P)
+  J : UU
+  HP : hset_struct_type_prod P J
+  EBC : structure_enrichment_coprod
+  ys : J → C
+  ============================
+   (is_coprod_enriched E' ys make_structure_enriched_coprod_cocone)
+
+
+Going to execute:
+<coq-core.plugins.ltac::simple_refine@0> $1
+
+TcDebug (0) > 
+Goal:
+
+  P : hset_cartesian_closed_struct
+  C : category
+  E : struct_enrichment P C
+  E' := make_enrichment_over_struct P C E
+     : enrichment C (sym_mon_closed_cat_of_hset_struct P)
+  J : UU
+  HP : hset_struct_type_prod P J
+  EBC : structure_enrichment_coprod
+  ys : J → C
+  ============================
+   (is_coprod_enriched E' ys make_structure_enriched_coprod_cocone)
+
+
+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 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)
+Level 0: In environment
+P : hset_cartesian_closed_struct
+C : category
+E : struct_enrichment P C
+E' := make_enrichment_over_struct P C E
+ : enrichment C (sym_mon_closed_cat_of_hset_struct P)
+J : UU
+HP : hset_struct_type_prod P J
+EBC : structure_enrichment_coprod
+ys : J → C
+The term "make_is_coprod_enriched ?E ?D ?a ?sum" has type
+ "(∏ (w : ?C) (v : ?V) (f : ∏ j : ?J, ?V ⟦ v, ?E ⦃ ?D j, w ⦄ ⟧) 
+   (j : ?J),
+   ?sum w v f · precomp_arr ?E w (enriched_coprod_cocone_in ?E ?D ?a j) = f j)
+  → (∏ (w : ?C) (v : ?V) (φ₁ φ₂ : ?V ⟦ v, ?E ⦃ ?a, w ⦄ ⟧),
+     (∏ j : ?J,
+      φ₁ · precomp_arr ?E w (enriched_coprod_cocone_in ?E ?D ?a j) =
+      φ₂ · precomp_arr ?E w (enriched_coprod_cocone_in ?E ?D ?a j)) → 
+     φ₁ = φ₂) → is_coprod_enriched ?E ?D ?a"
+while it is expected to have type
+ "is_coprod_enriched E' ys make_structure_enriched_coprod_cocone".
+Level 0: In environment
+P : hset_cartesian_closed_struct
+C : category
+E : struct_enrichment P C
+E' := make_enrichment_over_struct P C E
+ : enrichment C (sym_mon_closed_cat_of_hset_struct P)
+J : UU
+HP : hset_struct_type_prod P J
+EBC : structure_enrichment_coprod
+ys : J → C
+The term "make_is_coprod_enriched ?E ?D ?a ?sum" has type
+ "(∏ (w : ?C) (v : ?V) (f : ∏ j : ?J, ?V ⟦ v, ?E ⦃ ?D j, w ⦄ ⟧) 
+   (j : ?J),
+   ?sum w v f · precomp_arr ?E w (enriched_coprod_cocone_in ?E ?D ?a j) = f j)
+  → (∏ (w : ?C) (v : ?V) (φ₁ φ₂ : ?V ⟦ v, ?E ⦃ ?a, w ⦄ ⟧),
+     (∏ j : ?J,
+      φ₁ · precomp_arr ?E w (enriched_coprod_cocone_in ?E ?D ?a j) =
+      φ₂ · precomp_arr ?E w (enriched_coprod_cocone_in ?E ?D ?a j)) → 
+     φ₁ = φ₂) → is_coprod_enriched ?E ?D ?a"
+while it is expected to have type
+ "is_coprod_enriched E' ys make_structure_enriched_coprod_cocone".
+
+TcDebug (0) > 
+Goal:
+
+  P : hset_cartesian_closed_struct
+  C : category
+  E : struct_enrichment P C
+  E' := make_enrichment_over_struct P C E
+     : enrichment C (sym_mon_closed_cat_of_hset_struct P)
+  J : UU
+  HP : hset_struct_type_prod P J
+  EBC : structure_enrichment_coprod
+  ys : J → C
+  ============================
+   (is_coprod_enriched E' ys make_structure_enriched_coprod_cocone)
+
+
+Going to execute:
+simple refine (p _ _ _ _ _ _)
+
+TcDebug (0) > 
+Goal:
+
+  P : hset_cartesian_closed_struct
+  C : category
+  E : struct_enrichment P C
+  E' := make_enrichment_over_struct P C E
+     : enrichment C (sym_mon_closed_cat_of_hset_struct P)
+  J : UU
+  HP : hset_struct_type_prod P J
+  EBC : structure_enrichment_coprod
+  ys : J → C
+  ============================
+   (is_coprod_enriched E' ys make_structure_enriched_coprod_cocone)
+
+
+Going to execute:
+<coq-core.plugins.ltac::simple_refine@0> $1
+
+TcDebug (0) > 
+Goal:
+
+  P : hset_cartesian_closed_struct
+  C : category
+  E : struct_enrichment P C
+  E' := make_enrichment_over_struct P C E
+     : enrichment C (sym_mon_closed_cat_of_hset_struct P)
+  J : UU
+  HP : hset_struct_type_prod P J
+  EBC : structure_enrichment_coprod
+  ys : J → C
+  ============================
+   (is_coprod_enriched E' ys make_structure_enriched_coprod_cocone)
+
+
+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 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)
+Level 0: In environment
+P : hset_cartesian_closed_struct
+C : category
+E : struct_enrichment P C
+E' := make_enrichment_over_struct P C E
+ : enrichment C (sym_mon_closed_cat_of_hset_struct P)
+J : UU
+HP : hset_struct_type_prod P J
+EBC : structure_enrichment_coprod
+ys : J → C
+The term "make_is_coprod_enriched ?E ?D ?a ?sum ?in_sum" has type
+ "(∏ (w : ?C) (v : ?V) (φ₁ φ₂ : ?V ⟦ v, ?E ⦃ ?a, w ⦄ ⟧),
+   (∏ j : ?J,
+    φ₁ · precomp_arr ?E w (enriched_coprod_cocone_in ?E ?D ?a j) =
+    φ₂ · precomp_arr ?E w (enriched_coprod_cocone_in ?E ?D ?a j)) → 
+   φ₁ = φ₂) → is_coprod_enriched ?E ?D ?a" while it is expected to have type
+ "is_coprod_enriched E' ys make_structure_enriched_coprod_cocone".
+Level 0: In environment
+P : hset_cartesian_closed_struct
+C : category
+E : struct_enrichment P C
+E' := make_enrichment_over_struct P C E
+ : enrichment C (sym_mon_closed_cat_of_hset_struct P)
+J : UU
+HP : hset_struct_type_prod P J
+EBC : structure_enrichment_coprod
+ys : J → C
+The term "make_is_coprod_enriched ?E ?D ?a ?sum ?in_sum" has type
+ "(∏ (w : ?C) (v : ?V) (φ₁ φ₂ : ?V ⟦ v, ?E ⦃ ?a, w ⦄ ⟧),
+   (∏ j : ?J,
+    φ₁ · precomp_arr ?E w (enriched_coprod_cocone_in ?E ?D ?a j) =
+    φ₂ · precomp_arr ?E w (enriched_coprod_cocone_in ?E ?D ?a j)) → 
+   φ₁ = φ₂) → is_coprod_enriched ?E ?D ?a" while it is expected to have type
+ "is_coprod_enriched E' ys make_structure_enriched_coprod_cocone".
+
+TcDebug (0) > 
+Goal:
+
+  P : hset_cartesian_closed_struct
+  C : category
+  E : struct_enrichment P C
+  E' := make_enrichment_over_struct P C E
+     : enrichment C (sym_mon_closed_cat_of_hset_struct P)
+  J : UU
+  HP : hset_struct_type_prod P J
+  EBC : structure_enrichment_coprod
+  ys : J → C
+  ============================
+   (is_coprod_enriched E' ys make_structure_enriched_coprod_cocone)
+
+
+Going to execute:
+simple refine (p _ _ _ _ _ _ _)
+
+TcDebug (0) > 
+Goal:
+
+  P : hset_cartesian_closed_struct
+  C : category
+  E : struct_enrichment P C
+  E' := make_enrichment_over_struct P C E
+     : enrichment C (sym_mon_closed_cat_of_hset_struct P)
+  J : UU
+  HP : hset_struct_type_prod P J
+  EBC : structure_enrichment_coprod
+  ys : J → C
+  ============================
+   (is_coprod_enriched E' ys make_structure_enriched_coprod_cocone)
+