Skip to content

Commit 9c1f77d

Browse files
AextraTAextraT
authored
M Types for Set-based Polynomial Functors (UniMath#2056)
This contains the results of my internship under the supervision of Ralph Matthes. Content : - Set truncation as defined by @nmvdw (in a Zulip post), now in MoreFoundations/Sets - "Equivalence" between being a final coalgebra in UU and in HSET in Induction/M/MWithSets. - Proof that polynomial functors in sets are omega-continuous in CategoryTheory/Chains/OmegaContPolynomialFunctors. - Proof that when the polynomial functor is defined with sets, all final coalgebras are sets and construction of such coalgebras using CoAdamek in Induction/M/FinalCoalgebraHSET. - Refinement of ComputationalM in the case of sets in Induction/M/ComputationalMWithSets. - Example of potentially infinite boolean trees labeled with booleans in Induction/M/BinaryBooleanTrees. The files also come with header information.
1 parent d251895 commit 9c1f77d

File tree

10 files changed

+1395
-0
lines changed

10 files changed

+1395
-0
lines changed

‎UniMath/CategoryTheory/.package/files‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -398,6 +398,7 @@ Chains/CoAdamek.v
398398
Chains/OmegaCocontFunctors.v
399399
OppositeCategory/LimitsAsColimits.v
400400
Chains/OmegaContFunctors.v
401+
Chains/OmegaContPolynomialFunctors.v
401402
Chains/All.v
402403
Inductives/Lists.v
403404
Inductives/Trees.v

‎UniMath/CategoryTheory/Chains/OmegaContPolynomialFunctors.v‎

Lines changed: 295 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,295 @@
1+
(** ** Set-Based Polynomial Functors are omega-continuous
2+
3+
Author : Antoine Fisse (@AextraT), 2025
4+
*)
5+
6+
Require Import UniMath.Foundations.PartD.
7+
Require Import UniMath.Foundations.Sets.
8+
Require Import UniMath.MoreFoundations.All.
9+
10+
Require Import UniMath.Induction.FunctorCoalgebras_legacy.
11+
Require Import UniMath.Induction.PolynomialFunctors.
12+
Require Import UniMath.Induction.M.Core.
13+
Require Import UniMath.Induction.M.MWithSets.
14+
15+
Require Import UniMath.CategoryTheory.Categories.Type.Core.
16+
Require Import UniMath.CategoryTheory.Core.Categories.
17+
Require Import UniMath.CategoryTheory.Core.Functors.
18+
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
19+
Require Import UniMath.CategoryTheory.Categories.HSET.All.
20+
Require Import UniMath.CategoryTheory.Chains.CoAdamek.
21+
Require Import UniMath.CategoryTheory.Chains.Chains.
22+
Require Import UniMath.CategoryTheory.Chains.Cochains.
23+
Require Import UniMath.CategoryTheory.Limits.Graphs.Diagrams.
24+
Require Import UniMath.CategoryTheory.Limits.Graphs.Limits.
25+
Require Import UniMath.CategoryTheory.Limits.Terminal.
26+
Require Import UniMath.CategoryTheory.FunctorCoalgebras.
27+
28+
Local Open Scope cat.
29+
Local Open Scope functions.
30+
31+
Section OmegaContinuity.
32+
33+
Context {A : ob HSET} (B : pr1hSet A → ob HSET).
34+
35+
Local Definition F' := MWithSets.F' B.
36+
37+
Lemma comp_right_eq_hset
38+
{X Y Z : UU}
39+
{f g : X -> Y}
40+
(h : Y -> Z)
41+
(p : f = g)
42+
: h ∘ f = h ∘ g.
43+
Proof.
44+
induction p.
45+
apply idpath.
46+
Defined.
47+
48+
Lemma pullback_cone_edge
49+
{X Y0 Y1 Y2: SET}
50+
(x : pr1hSet X)
51+
{f : SET ⟦ Y1, Y2 ⟧}
52+
{g0 : SET ⟦ X, F' Y0 ⟧}
53+
{g1 : SET ⟦ X, F' Y1 ⟧}
54+
{g2 : SET ⟦ X, F' Y2 ⟧}
55+
(p : (#F' f) ∘ g1 = g2)
56+
(q1 : pr1 ∘ g0 = pr1 ∘ g1)
57+
(q2 : pr1 ∘ g0 = pr1 ∘ g2)
58+
: (λ b, f (pr2 (g1 x) (transportf (λ φ, pr1hSet (B (φ x))) q1 b))) = (λ b, pr2 (g2 x) (transportf (λ φ, pr1hSet (B (φ x))) q2 b)).
59+
Proof.
60+
induction p.
61+
cbn.
62+
assert (r : q1 = q2).
63+
{ apply (setproperty (SET ⟦ X, A ⟧,, isaset_forall_hSet (pr1hSet X) (λ _, A)) (pr1 ∘ g0) (pr1 ∘ g1)).
64+
}
65+
induction r.
66+
apply idpath.
67+
Qed.
68+
69+
Lemma pathtozero_cone
70+
{c0 : SET}
71+
{c : cochain SET}
72+
(cc0 : cone (mapdiagram F' c) c0)
73+
(v : nat)
74+
: pr1 ∘ (pr1 cc0 0) = pr1 ∘ (pr1 cc0 v).
75+
Proof.
76+
induction v.
77+
- apply idpath.
78+
- symmetry.
79+
etrans.
80+
+ apply (comp_right_eq_hset (λ x : pr1hSet (F' (dob c v)), pr1 x) (pr2 cc0 (S v) v (idpath (S v)))).
81+
+ symmetry. apply IHv.
82+
Qed.
83+
84+
Lemma pullback_cone
85+
{c0 : SET}
86+
(x : pr1hSet c0)
87+
{c : cochain SET}
88+
(cc0 : cone (mapdiagram F' c) c0)
89+
: cone c (B (pr1 (pr1 cc0 0 x))).
90+
Proof.
91+
unfold cone.
92+
unfold cone in cc0.
93+
unfold forms_cone in cc0.
94+
set (f := λ v : vertex conat_graph, (λ b, pr2 (pr1 cc0 v x) (transportf (λ φ, pr1hSet (B (φ x))) (pathtozero_cone cc0 v) b)) : SET ⟦ B (pr1 (pr1 cc0 0 x)), dob c v ⟧).
95+
assert (p : forms_cone c f).
96+
{
97+
unfold forms_cone.
98+
simpl.
99+
intros u v e.
100+
induction e.
101+
set (p := pullback_cone_edge x (pr2 cc0 (S v) v (idpath (S v))) (pathtozero_cone cc0 (S v)) (pathtozero_cone cc0 v)).
102+
apply p.
103+
}
104+
exact (f,, p).
105+
Defined.
106+
107+
Lemma exists_fun_mapdiagram
108+
{c : cochain SET}
109+
{L : SET}
110+
{cc : cone c L}
111+
(c_limcone : isLimCone c L cc)
112+
(c0 : SET)
113+
(cc0 : cone (mapdiagram F' c) c0)
114+
: SET ⟦ c0, F' L ⟧.
115+
Proof.
116+
intro x.
117+
cbn.
118+
unfold polynomial_functor_obj.
119+
set (a := pr1 (pr1 cc0 0 x) : pr1hSet A).
120+
set (cx := B a).
121+
set (ccx := pullback_cone x cc0).
122+
set (f2x := pr11 (c_limcone cx ccx)).
123+
exact (a,, f2x).
124+
Defined.
125+
126+
Lemma is_mor_mapdiagram2_point
127+
{X Y c : UU}
128+
(x : X)
129+
{φ1 φ2 : X -> pr1hSet A}
130+
{f : pr1hSet (B (φ1 x)) -> c}
131+
{g : c -> Y}
132+
{h : pr1hSet (B (φ2 x)) -> Y}
133+
(q : φ1 = φ2)
134+
(p : g ∘ f = λ b, h (transportf (λ ψ, pr1hSet (B (ψ x))) q b))
135+
: transportf (λ a, pr1hSet (B a) -> Y) (toforallpaths _ _ _ q x) (g ∘ f) = h.
136+
Proof.
137+
induction q.
138+
apply p.
139+
Defined.
140+
141+
Lemma fun_mapdiagram_is_mor
142+
{c : cochain SET}
143+
{L : SET}
144+
{cc : cone c L}
145+
(c_limcone : isLimCone c L cc)
146+
(c0 : SET)
147+
(cc0 : cone (mapdiagram F' c) c0)
148+
(f := exists_fun_mapdiagram c_limcone c0 cc0)
149+
: is_cone_mor cc0 (mapcone F' c cc) f.
150+
Proof.
151+
unfold is_cone_mor.
152+
intro v.
153+
apply funextfun.
154+
intro x.
155+
use total2_paths_f.
156+
- unfold coneOut.
157+
unfold mapcone.
158+
cbn.
159+
apply (toforallpaths _ _ _ (pathtozero_cone cc0 v) x).
160+
- cbn.
161+
unfold coneOut.
162+
set (a := pr1 (pr1 cc0 0 x) : pr1hSet A).
163+
set (cx := B a).
164+
set (ccx := pullback_cone x cc0).
165+
set (p := pr2 (pr1 (c_limcone cx ccx)) v).
166+
cbn in p.
167+
unfold coneOut in p.
168+
apply (is_mor_mapdiagram2_point x (pathtozero_cone cc0 v) p).
169+
Qed.
170+
171+
Lemma exists_mor_mapdiagram
172+
{c : cochain SET}
173+
{L : SET}
174+
{cc : cone c L}
175+
(c_limcone : isLimCone c L cc)
176+
(c0 : SET)
177+
(cc0 : cone (mapdiagram F' c) c0)
178+
: ∑ f : SET ⟦ c0, F' L ⟧, is_cone_mor cc0 (mapcone F' c cc) f.
179+
Proof.
180+
set (f := exists_fun_mapdiagram c_limcone c0 cc0).
181+
set (p := fun_mapdiagram_is_mor c_limcone c0 cc0).
182+
exact (f,, p).
183+
Defined.
184+
185+
Lemma move_proof
186+
{X Y Z : SET}
187+
{x : pr1hSet X}
188+
(h1 h2 : SET⟦ X, A ⟧)
189+
(f : SET ⟦ B (h2 x), Y ⟧)
190+
(g : SET ⟦ Y, Z ⟧ )
191+
(q : h1 = h2)
192+
: g ∘ (transportf (λ a, SET ⟦ B a, Y ⟧) (pathsinv0 (toforallpaths _ _ _ q x)) f) = λ b, g (f (transportf (λ φ, pr1hSet (B (φ x))) q b)).
193+
Proof.
194+
induction q.
195+
cbn.
196+
apply idpath.
197+
Qed.
198+
199+
Lemma proj_is_cone_mor_point
200+
{X Y Z0 Z : SET}
201+
(x : pr1hSet X)
202+
{f : SET ⟦ X, F' Y ⟧}
203+
{g : SET⟦ Y, Z ⟧}
204+
(h0 : SET⟦ X, F' Z0 ⟧)
205+
(h1 : SET⟦ X, F' Z ⟧)
206+
(p : #F' g ∘ f = h1)
207+
(q : pr1 (f x) = pr1 (h0 x))
208+
(q' : pr1 ∘ h0 = pr1 ∘ h1)
209+
: g ∘ (transportf _ q (pr2 (f x))) = λ b, (pr2 (h1 x)) (transportf (λ φ, pr1hSet (B (φ x))) q' b).
210+
Proof.
211+
induction p.
212+
cbn.
213+
set (q'x := toforallpaths _ _ _ q' x).
214+
cbn in q'x.
215+
set (q'x' := pathsinv0 q'x).
216+
assert (r : q'x' = q) by apply (setproperty A).
217+
induction r.
218+
apply (move_proof (pr1 ∘ h0) (pr1 ∘ # F' g ∘ f) (pr2 (f x)) g q').
219+
Qed.
220+
221+
Lemma proj_is_cone_mor
222+
{c : cochain SET}
223+
{c0 L : SET}
224+
{x : pr1hSet c0}
225+
{cc : cone c L}
226+
{cc0 : cone (mapdiagram F' c) c0}
227+
(f : SET ⟦ c0, F' L ⟧)
228+
{p : pr1 (f x) = pr1 (pr1 cc0 0 x)}
229+
(pf : is_cone_mor cc0 (mapcone F' c cc) f)
230+
: is_cone_mor (pullback_cone x cc0) cc (transportf _ p (pr2 (f x))).
231+
Proof.
232+
set (ccx := pullback_cone x cc0).
233+
cbn.
234+
unfold is_cone_mor.
235+
intro v.
236+
unfold is_cone_mor in pf.
237+
unfold coneOut in pf.
238+
apply (proj_is_cone_mor_point x (pr1 cc0 0) (pr1 cc0 v) (pf v) p (pathtozero_cone cc0 v)).
239+
Qed.
240+
241+
Lemma morph_unicity_pushout
242+
{c : cochain SET}
243+
{c0 L : SET}
244+
{cc : cone c L}
245+
(c_limcone : isLimCone c L cc)
246+
(cc0 : cone (mapdiagram F' c) c0)
247+
{f' : SET⟦ c0, F' L ⟧}
248+
(pf' : is_cone_mor cc0 (mapcone F' c cc) f')
249+
: f' = pr1 (exists_mor_mapdiagram c_limcone c0 cc0).
250+
Proof.
251+
set (f_pf := exists_mor_mapdiagram c_limcone c0 cc0).
252+
set (f := pr1 f_pf).
253+
set (pf := pr2 f_pf).
254+
apply funextfun.
255+
intro x.
256+
set (p := maponpaths (λ z, pr1 z) (toforallpaths _ _ _ (pf' 0) x)).
257+
use total2_paths_f.
258+
- unfold is_cone_mor in pf'.
259+
unfold mapcone in pf'.
260+
unfold coneOut in pf'.
261+
cbn in pf'.
262+
apply p.
263+
- cbn.
264+
set (a := pr1 (pr1 cc0 0 x) : pr1hSet A).
265+
set (cx := B a).
266+
set (ccx := pullback_cone x cc0).
267+
set (f'2 := transportf _ p (pr2 (f' x)) : SET ⟦ cx, L ⟧).
268+
set (f'2_cone_mor := proj_is_cone_mor f' pf' : is_cone_mor ccx cc f'2).
269+
apply (maponpaths (λ z, pr1 z) (pr2 (c_limcone cx ccx) (f'2,, f'2_cone_mor))).
270+
Qed.
271+
272+
Lemma PolyFunctor_omega_cont : is_omega_cont F'.
273+
Proof.
274+
unfold is_omega_cont.
275+
unfold preserves_limit.
276+
unfold isLimCone.
277+
intros c L cc c_limcone c0 cc0.
278+
use tpair.
279+
- exact (exists_mor_mapdiagram c_limcone c0 cc0).
280+
- set (f_pf := exists_mor_mapdiagram c_limcone c0 cc0).
281+
set (f := pr1 f_pf).
282+
set (pf := pr2 f_pf).
283+
intro t.
284+
destruct t as [f' pf'].
285+
use total2_paths_f.
286+
+ apply (morph_unicity_pushout c_limcone cc0 pf').
287+
+ set (p1 := morph_unicity_pushout c_limcone cc0 pf').
288+
set (tpf' := transportf (is_cone_mor cc0 (mapcone F' c cc)) p1 pf').
289+
unfold is_cone_mor in pf.
290+
use funextsec.
291+
intro v.
292+
apply (isaset_forall_hSet (pr1hSet c0) (λ _, F' (dob c v))).
293+
Defined.
294+
295+
End OmegaContinuity.

‎UniMath/Induction/.package/files‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,11 @@
11
FunctorAlgebras_legacy.v
22
FunctorCoalgebras_legacy.v
3+
FunctorCoalgebras_legacy_alt_UU.v
34

45
PolynomialFunctors.v
56
PolynomialAlgebras2Cells.v
67
ImpredicativeInductiveSets.v
8+
SetBasedPolynomialFunctors.v
79
M/Core.v
810
M/Limits.v
911
M/Uniqueness.v
@@ -15,3 +17,7 @@ W/Naturals.v
1517
W/Uniqueness.v
1618
M/Chains.v
1719
M/ComputationalM.v
20+
M/MWithSets.v
21+
M/FinalCoalgebraHSET.v
22+
M/ComputationalMWithSets.v
23+
M/BinaryBooleanMTrees.v

0 commit comments

Comments
 (0)