Skip to content

Commit 35416c5

Browse files
mikeshulmanmikeshulman
committed
fibrancy of W-types
1 parent 25cbaea commit 35416c5

File tree

2 files changed

+419
-23
lines changed

2 files changed

+419
-23
lines changed

‎test/black/hct-hott.t/fibrant_types.ny‎

Lines changed: 356 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -259,6 +259,362 @@ def 𝕗ℕ : isFibrant ℕ ≔ [
259259
| .id.e ↦ n0 n1 ↦
260260
𝕗eqv (ℕ_code n0 n1) (Id ℕ n0 n1) (id_ℕ_iso n0 n1) (𝕗_ℕ_code n0 n1)]
261261

262+
{` W-types `}
263+
264+
{` To prove that general W-types are fibrant, we need function extensionality, since W-types involve functions as inputs. `}
265+
266+
axiom funext (A : Type) (B : A → Type) (f0 f1 : (x : A) → B x)
267+
(f2 : (x : A) → eq (B x) (f0 x) (f1 x))
268+
: eq ((x : A) → B x) f0 f1
269+
270+
{` We also need a version of funext for bridges in function types. We could probably derive this from the ordinary one, using the definitional isomorphism behavior of Id-Π. `}
271+
272+
axiom funext_refl (A0 A1 : Type) (A2 : Id Type A0 A1) (B0 : A0 → Type)
273+
(B1 : A1 → Type) (B2 : refl ((X ↦ X → Type) : Type → Type) A2 B0 B1)
274+
(f0 : Π A0 B0) (f1 : Π A1 B1) (f20 f21 : refl Π A2 B2 f0 f1)
275+
(f22 : (a0 : A0) (a1 : A1) (a2 : A2 a0 a1)
276+
→ eq.eq (B2 a2 (f0 a0) (f1 a1)) (f20 a2) (f21 a2))
277+
: eq (refl Π A2 B2 f0 f1) f20 f21
278+
279+
{` Now, there are two ways to characterize the Id types of a W-type. The firts is that the Id-types of an (indexed) W-type are an indexed W-type, which is properly indexed even if the original W-type was not. This is not helpful for us, since indexed inductive types in general are *not* fibrant until we fibrantly replace them. However, we include the encode-decode argument here anyway. `}
280+
281+
section Indexed_𝕎 ≔
282+
283+
def 𝕎spec : Type ≔ sig (
284+
I : Type,
285+
A : Type,
286+
B : A → Type,
287+
j : (a : A) → B a → I,
288+
k : A → I )
289+
290+
def 𝕎 (s : 𝕎spec) : s .I → Type ≔ data [
291+
| sup. (a : s .A) (f : (b : s .B a) → 𝕎 s (s .j a b)) : 𝕎 s (s .k a) ]
292+
293+
def code_spec (s : 𝕎spec) : 𝕎spec ≔ (
294+
I ≔ sig (
295+
i0 : s .I,
296+
i1 : s .I,
297+
i2 : Id (s .I) i0 i1,
298+
x0 : 𝕎 s i0,
299+
x1 : 𝕎 s i1 ),
300+
A ≔ sig (
301+
a0 : s .A,
302+
a1 : s .A,
303+
a2 : Id (s .A) a0 a1,
304+
f0 : (b0 : s .B a0) → 𝕎 s (s .j a0 b0),
305+
f1 : (b1 : s .B a1) → 𝕎 s (s .j a1 b1) ),
306+
B ≔ x ↦ sig (
307+
b0 : s .B (x .a0),
308+
b1 : s .B (x .a1),
309+
b2 : refl (s .B) (x .a2) b0 b1 ),
310+
j ≔ a b ↦ (
311+
s .j (a .a0) (b .b0),
312+
s .j (a .a1) (b .b1),
313+
refl (s .j) (a .a2) (b .b2),
314+
a .f0 (b .b0),
315+
a .f1 (b .b1)),
316+
k ≔ a ↦ (
317+
s .k (a .a0),
318+
s .k (a .a1),
319+
refl (s .k) (a .a2),
320+
sup. (a .a0) (a .f0),
321+
sup. (a .a1) (a .f1)))
322+
323+
def 𝕎_encode (s : 𝕎spec) (i0 i1 : s .I) (i2 : Id (s .I) i0 i1)
324+
(x0 : 𝕎 s i0) (x1 : 𝕎 s i1) (x2 : refl (𝕎 s) i2 x0 x1)
325+
: 𝕎 (code_spec s) (i0, i1, i2, x0, x1)
326+
≔ match x2 [
327+
| sup. a f ↦
328+
sup. (a.0, a.1, a.2, f.0, f.1)
329+
(b ↦
330+
𝕎_encode s (s .j a.0 (b .b0)) (s .j a.1 (b .b1))
331+
(refl (s .j) a.2 (b .b2)) (f.0 (b .b0)) (f.1 (b .b1))
332+
(f.2 (b .b2)))]
333+
334+
def 𝕎_decode (s : 𝕎spec) (y : code_spec s .I) (y2 : 𝕎 (code_spec s) y)
335+
: refl (𝕎 s) (y .i2) (y .x0) (y .x1)
336+
≔ match y2 [
337+
| sup. a f ↦
338+
sup. (a .a2)
339+
(b ⤇
340+
𝕎_decode s
341+
(s .j (a .a0) b.0,
342+
s .j (a .a1) b.1,
343+
refl s .j (a .a2) b.2,
344+
a .f0 b.0,
345+
a .f1 b.1) (f (b.0, b.1, b.2)))]
346+
347+
def 𝕎_decode_encode (s : 𝕎spec) (i0 i1 : s .I) (i2 : Id (s .I) i0 i1)
348+
(x0 : 𝕎 s i0) (x1 : 𝕎 s i1) (x2 : refl (𝕎 s) i2 x0 x1)
349+
: eq (refl (𝕎 s) i2 x0 x1)
350+
(𝕎_decode s (i0, i1, i2, x0, x1) (𝕎_encode s i0 i1 i2 x0 x1 x2)) x2
351+
≔ match x2 [
352+
| sup. a f ↦
353+
eq.ap
354+
(refl Π (refl s .B a.2) {b ↦ 𝕎 s (s .j a.0 b)} {b ↦ 𝕎 s (s .j a.1 b)}
355+
(b ⤇ refl 𝕎 (refl s) (refl s .j a.2 b.2)) f.0 f.1)
356+
(refl 𝕎 (refl s) (refl s .k a.2) (sup. a.0 f.0) (sup. a.1 f.1))
357+
(H ↦ sup. a.2 H)
358+
(b ⤇
359+
𝕎_decode s
360+
(s .j a.0 b.0, s .j a.1 b.1, refl s .j a.2 b.2, f.0 b.0, f.1 b.1)
361+
(𝕎_encode s (s .j a.0 b.0) (s .j a.1 b.1) (refl s .j a.2 b.2)
362+
(f.0 b.0) (f.1 b.1) (f.2 b.2))) f.2
363+
(funext_refl (s .B a.0) (s .B a.1) (refl s .B a.2)
364+
(x ↦ 𝕎 s (s .j a.0 x)) (x ↦ 𝕎 s (s .j a.1 x))
365+
(x ⤇ refl 𝕎 (refl s) (refl s .j a.2 x.2)) f.0 f.1
366+
(b ⤇
367+
𝕎_decode s
368+
(s .j a.0 b.0,
369+
s .j a.1 b.1,
370+
refl s .j a.2 b.2,
371+
f.0 b.0,
372+
f.1 b.1)
373+
(𝕎_encode s (s .j a.0 b.0) (s .j a.1 b.1) (refl s .j a.2 b.2)
374+
(f.0 b.0) (f.1 b.1) (f.2 b.2))) f.2
375+
(a0 a1 a2 ↦
376+
𝕎_decode_encode s (s .j a.0 a0) (s .j a.1 a1) (refl s .j a.2 a2)
377+
(f.0 a0) (f.1 a1) (f.2 a2)))]
378+
379+
def 𝕎_encode_decode (s : 𝕎spec) (y : code_spec s .I)
380+
(y2 : 𝕎 (code_spec s) y)
381+
: eq (𝕎 (code_spec s) y)
382+
(𝕎_encode s (y .i0) (y .i1) (y .i2) (y .x0) (y .x1) (𝕎_decode s y y2))
383+
y2
384+
≔ match y2 [
385+
| sup. a f ↦
386+
eq.ap ((b : code_spec s .B a) → 𝕎 (code_spec s) (code_spec s .j a b))
387+
(𝕎 (code_spec s) (code_spec s .k a)) (g ↦ sup. a g)
388+
(b ↦
389+
𝕎_encode s (s .j (a .a0) (b .b0)) (s .j (a .a1) (b .b1))
390+
(refl s .j (a .a2) (b .b2)) (a .f0 (b .b0)) (a .f1 (b .b1))
391+
(𝕎_decode s
392+
(s .j (a .a0) (b .b0),
393+
s .j (a .a1) (b .b1),
394+
refl s .j (a .a2) (b .b2),
395+
a .f0 (b .b0),
396+
a .f1 (b .b1)) (f (b .b0, b .b1, b .b2)))) f
397+
(funext (code_spec s .B a) (b ↦ 𝕎 (code_spec s) (code_spec s .j a b))
398+
(b ↦
399+
𝕎_encode s (s .j (a .a0) (b .b0)) (s .j (a .a1) (b .b1))
400+
(refl s .j (a .a2) (b .b2)) (a .f0 (b .b0)) (a .f1 (b .b1))
401+
(𝕎_decode s
402+
(s .j (a .a0) (b .b0),
403+
s .j (a .a1) (b .b1),
404+
refl s .j (a .a2) (b .b2),
405+
a .f0 (b .b0),
406+
a .f1 (b .b1)) (f (b .b0, b .b1, b .b2)))) f
407+
(x ↦ 𝕎_encode_decode s (code_spec s .j a x) (f x)))]
408+
409+
def id_𝕎_iso (s : 𝕎spec) (i0 i1 : s .I) (i2 : Id (s .I) i0 i1)
410+
(x0 : 𝕎 s i0) (x1 : 𝕎 s i1)
411+
: refl (𝕎 s) i2 x0 x1 ≅ 𝕎 (code_spec s) (i0, i1, i2, x0, x1)
412+
≔ adjointify (refl (𝕎 s) i2 x0 x1) (𝕎 (code_spec s) (i0, i1, i2, x0, x1))
413+
(𝕎_encode s i0 i1 i2 x0 x1) (𝕎_decode s (i0, i1, i2, x0, x1))
414+
(x2 ↦ 𝕎_decode_encode s i0 i1 i2 x0 x1 x2)
415+
(y2 ↦ 𝕎_encode_decode s (i0, i1, i2, x0, x1) y2)
416+
417+
end
418+
419+
{` The characterization of Id-types of W-types that is useful to us is recursive, analogous to that for the Id-types of ℕ above. `}
420+
421+
def 𝕎 (A : Type) (B : A → Type) : Type ≔ data [
422+
| sup. (a : A) (f : B a → 𝕎 A B) ]
423+
424+
{` We need to characterize the *dependent* Id-types over bridges of A and B. `}
425+
426+
def 𝕎_code (A0 A1 : Type) (A2 : Id Type A0 A1) (B0 : A0 → Type)
427+
(B1 : A1 → Type) (B2 : refl ((X ↦ X → Type) : Type → Type) A2 B0 B1)
428+
(x0 : 𝕎 A0 B0) (x1 : 𝕎 A1 B1)
429+
: Type
430+
≔ match x0, x1 [
431+
| sup. a0 f0, sup. a1 f1 ↦
432+
Σ (A2 a0 a1)
433+
(a2 ↦
434+
(b0 : B0 a0) (b1 : B1 a1) (b2 : B2 a2 b0 b1)
435+
→ 𝕎_code A0 A1 A2 B0 B1 B2 (f0 b0) (f1 b1))]
436+
437+
{` The encode-decode argument is straightforward, and only long because of the multiple applications of funext and because we lack implicit arguments. `}
438+
439+
def 𝕎_encode (A0 A1 : Type) (A2 : Id Type A0 A1) (B0 : A0 → Type)
440+
(B1 : A1 → Type) (B2 : refl ((X ↦ X → Type) : Type → Type) A2 B0 B1)
441+
(x0 : 𝕎 A0 B0) (x1 : 𝕎 A1 B1) (x2 : refl 𝕎 A2 B2 x0 x1)
442+
: 𝕎_code A0 A1 A2 B0 B1 B2 x0 x1
443+
≔ match x2 [
444+
| sup. a f ↦ (
445+
fst ≔ a.2,
446+
snd ≔ b0 b1 b2 ↦ 𝕎_encode A0 A1 A2 B0 B1 B2 (f.0 b0) (f.1 b1) (f.2 b2))]
447+
448+
def 𝕎_decode (A0 A1 : Type) (A2 : Id Type A0 A1) (B0 : A0 → Type)
449+
(B1 : A1 → Type) (B2 : refl ((X ↦ X → Type) : Type → Type) A2 B0 B1)
450+
(x0 : 𝕎 A0 B0) (x1 : 𝕎 A1 B1) (y2 : 𝕎_code A0 A1 A2 B0 B1 B2 x0 x1)
451+
: refl 𝕎 A2 B2 x0 x1
452+
≔ match x0, x1 [
453+
| sup. a0 f0, sup. a1 f1 ↦
454+
sup. (y2 .fst)
455+
(b ⤇ 𝕎_decode A0 A1 A2 B0 B1 B2 (f0 b.0) (f1 b.1) (y2 .snd b.0 b.1 b.2))]
456+
457+
def 𝕎_decode_encode (A0 A1 : Type) (A2 : Id Type A0 A1) (B0 : A0 → Type)
458+
(B1 : A1 → Type) (B2 : refl ((X ↦ X → Type) : Type → Type) A2 B0 B1)
459+
(x0 : 𝕎 A0 B0) (x1 : 𝕎 A1 B1) (x2 : refl 𝕎 A2 B2 x0 x1)
460+
: eq (refl 𝕎 A2 B2 x0 x1)
461+
(𝕎_decode A0 A1 A2 B0 B1 B2 x0 x1 (𝕎_encode A0 A1 A2 B0 B1 B2 x0 x1 x2))
462+
x2
463+
≔ match x2 [
464+
| sup. a f ↦
465+
eq.ap
466+
(refl Π (B2 a.2) {_ ↦ 𝕎 A0 B0} {_ ↦ 𝕎 A1 B1} (_ ⤇ refl 𝕎 A2 B2) f.0 f.1)
467+
(refl 𝕎 A2 B2 (sup. a.0 f.0) (sup. a.1 f.1)) (g ↦ sup. a.2 g)
468+
(b ⤇
469+
𝕎_decode A0 A1 A2 B0 B1 B2 (f.0 b.0) (f.1 b.1)
470+
(𝕎_encode A0 A1 A2 B0 B1 B2 (f.0 b.0) (f.1 b.1) (f.2 b.2))) f.2
471+
(funext_refl (B0 a.0) (B1 a.1) (B2 a.2) (_ ↦ 𝕎 A0 B0) (_ ↦ 𝕎 A1 B1)
472+
(_ ⤇ refl 𝕎 A2 B2) f.0 f.1
473+
(b ⤇
474+
𝕎_decode A0 A1 A2 B0 B1 B2 (f.0 b.0) (f.1 b.1)
475+
(𝕎_encode A0 A1 A2 B0 B1 B2 (f.0 b.0) (f.1 b.1) (f.2 b.2))) f.2
476+
(a0 a1 a2 ↦
477+
𝕎_decode_encode A0 A1 A2 B0 B1 B2 (f.0 a0) (f.1 a1) (f.2 a2)))]
478+
479+
def 𝕎_encode_decode (A0 A1 : Type) (A2 : Id Type A0 A1) (B0 : A0 → Type)
480+
(B1 : A1 → Type) (B2 : refl ((X ↦ X → Type) : Type → Type) A2 B0 B1)
481+
(x0 : 𝕎 A0 B0) (x1 : 𝕎 A1 B1) (y2 : 𝕎_code A0 A1 A2 B0 B1 B2 x0 x1)
482+
: eq (𝕎_code A0 A1 A2 B0 B1 B2 x0 x1)
483+
(𝕎_encode A0 A1 A2 B0 B1 B2 x0 x1 (𝕎_decode A0 A1 A2 B0 B1 B2 x0 x1 y2))
484+
y2
485+
≔ match x0, x1 [
486+
| sup. a0 f0, sup. a1 f1 ↦
487+
eq.ap
488+
((b0 : B0 a0) (b1 : B1 a1) (b2 : B2 (y2 .fst) b0 b1)
489+
→ 𝕎_code A0 A1 A2 B0 B1 B2 (f0 b0) (f1 b1))
490+
(Σ (A2 a0 a1)
491+
(a2 ↦
492+
(b0 : B0 a0) (b1 : B1 a1) (b2 : B2 a2 b0 b1)
493+
→ 𝕎_code A0 A1 A2 B0 B1 B2 (f0 b0) (f1 b1))) (f2 ↦ (y2 .fst, f2))
494+
((𝕎_encode A0 A1 A2 B0 B1 B2 (sup. a0 f0) (sup. a1 f1)
495+
(sup. (y2 .fst)
496+
(b ⤇
497+
𝕎_decode A0 A1 A2 B0 B1 B2 (f0 b.0) (f1 b.1)
498+
(y2 .snd b.0 b.1 b.2)))) .snd) (y2 .snd)
499+
(funext (B0 a0)
500+
(b0 ↦
501+
(b1 : B1 a1) (b2 : B2 (y2 .fst) b0 b1)
502+
→ 𝕎_code A0 A1 A2 B0 B1 B2 (f0 b0) (f1 b1))
503+
(𝕎_encode A0 A1 A2 B0 B1 B2 (sup. a0 f0) (sup. a1 f1)
504+
(sup. (y2 .fst)
505+
(b ⤇
506+
𝕎_decode A0 A1 A2 B0 B1 B2 (f0 b.0) (f1 b.1)
507+
(y2 .snd b.0 b.1 b.2))) .snd) (y2 .snd)
508+
(b0 ↦
509+
funext (B1 a1)
510+
(b1 ↦
511+
(b2 : B2 (y2 .fst) b0 b1)
512+
→ 𝕎_code A0 A1 A2 B0 B1 B2 (f0 b0) (f1 b1))
513+
(𝕎_encode A0 A1 A2 B0 B1 B2 (sup. a0 f0) (sup. a1 f1)
514+
(sup. (y2 .fst)
515+
(b ⤇
516+
𝕎_decode A0 A1 A2 B0 B1 B2 (f0 b.0) (f1 b.1)
517+
(y2 .snd b.0 b.1 b.2)))
518+
.snd b0) (y2 .snd b0)
519+
(b1 ↦
520+
funext (B2 (y2 .fst) b0 b1)
521+
(_ ↦ 𝕎_code A0 A1 A2 B0 B1 B2 (f0 b0) (f1 b1))
522+
(𝕎_encode A0 A1 A2 B0 B1 B2 (sup. a0 f0) (sup. a1 f1)
523+
(sup. (y2 .fst)
524+
(b ⤇
525+
𝕎_decode A0 A1 A2 B0 B1 B2 (f0 b.0) (f1 b.1)
526+
(y2 .snd b.0 b.1 b.2)))
527+
.snd b0 b1) (y2 .snd b0 b1)
528+
(b2 ↦
529+
𝕎_encode_decode A0 A1 A2 B0 B1 B2 (f0 b0) (f1 b1)
530+
(y2 .snd b0 b1 b2)))))]
531+
532+
def Id_𝕎_iso (A0 A1 : Type) (A2 : Id Type A0 A1) (B0 : A0 → Type)
533+
(B1 : A1 → Type) (B2 : refl ((X ↦ X → Type) : Type → Type) A2 B0 B1)
534+
(x0 : 𝕎 A0 B0) (x1 : 𝕎 A1 B1)
535+
: 𝕎_code A0 A1 A2 B0 B1 B2 x0 x1 ≅ refl 𝕎 A2 B2 x0 x1
536+
≔ adjointify (𝕎_code A0 A1 A2 B0 B1 B2 x0 x1) (refl 𝕎 A2 B2 x0 x1)
537+
(𝕎_decode A0 A1 A2 B0 B1 B2 x0 x1) (𝕎_encode A0 A1 A2 B0 B1 B2 x0 x1)
538+
(𝕎_encode_decode A0 A1 A2 B0 B1 B2 x0 x1)
539+
(𝕎_decode_encode A0 A1 A2 B0 B1 B2 x0 x1)
540+
541+
{` Next we prove that the codes are fibrant if the inputs are. This is just putting together 𝕗Σ and 𝕗Π. `}
542+
543+
def 𝕗_𝕎_code (A0 A1 : Type) (A2 : Id Type A0 A1) (B0 : A0 → Type)
544+
(B1 : A1 → Type) (B2 : refl ((X ↦ X → Type) : Type → Type) A2 B0 B1)
545+
(𝕗A0 : isFibrant A0) (𝕗A1 : isFibrant A1) (𝕗A2 : refl isFibrant A2 𝕗A0 𝕗A1)
546+
(𝕗B0 : (a0 : A0) → isFibrant (B0 a0)) (𝕗B1 : (a1 : A1) → isFibrant (B1 a1))
547+
(𝕗B2 : refl Π A2 {x ↦ isFibrant (B0 x)} {x ↦ isFibrant (B1 x)}
548+
(x ⤇ refl isFibrant (B2 x.2)) 𝕗B0 𝕗B1) (x0 : 𝕎 A0 B0)
549+
(x1 : 𝕎 A1 B1)
550+
: isFibrant (𝕎_code A0 A1 A2 B0 B1 B2 x0 x1)
551+
≔ match x0, x1 [
552+
| sup. a0 f0, sup. a1 f1 ↦
553+
𝕗Σ (A2 a0 a1)
554+
(a2 ↦
555+
(b0 : B0 a0) (b1 : B1 a1) (b2 : B2 a2 b0 b1)
556+
→ 𝕎_code A0 A1 A2 B0 B1 B2 (f0 b0) (f1 b1)) (𝕗A2 .id.1 a0 a1)
557+
(a2 ↦
558+
𝕗Π (B0 a0)
559+
(b0 ↦
560+
(b1 : B1 a1) (b2 : B2 a2 b0 b1)
561+
→ 𝕎_code A0 A1 A2 B0 B1 B2 (f0 b0) (f1 b1)) (𝕗B0 a0)
562+
(b0 ↦
563+
𝕗Π (B1 a1)
564+
(b1 ↦
565+
(b2 : B2 a2 b0 b1) → 𝕎_code A0 A1 A2 B0 B1 B2 (f0 b0) (f1 b1))
566+
(𝕗B1 a1)
567+
(b1 ↦
568+
𝕗Π (B2 a2 b0 b1) (_ ↦ 𝕎_code A0 A1 A2 B0 B1 B2 (f0 b0) (f1 b1))
569+
(𝕗B2 a2 .id.1 b0 b1)
570+
(b2 ↦
571+
𝕗_𝕎_code A0 A1 A2 B0 B1 B2 𝕗A0 𝕗A1 𝕗A2 𝕗B0 𝕗B1 𝕗B2 (f0 b0)
572+
(f1 b1)))))]
573+
574+
{` Finally, we can prove that W-types are fibrant. Note that there are "recursive calls" to 𝕗𝕎 in *all* the clauses. I'm not exactly sure how they are justified in the cases of tr and lift, but note that they are inside matches as well. `}
575+
576+
def 𝕗𝕎 (A : Type) (B : A → Type) (𝕗A : isFibrant A)
577+
(𝕗B : (x : A) → isFibrant (B x))
578+
: isFibrant (𝕎 A B)
579+
≔ [
580+
| .trr.e ↦ [
581+
| sup. a0 f0 ↦
582+
sup. (𝕗A.2 .trr.1 a0)
583+
(refl 𝕗Π (B.2 (𝕗A.2 .liftr.1 a0)) {_ ⤇ 𝕎 A.0 B.0} {_ ⤇ 𝕎 A.1 B.1}
584+
(_ ⤇ refl 𝕎 A.2 B.2) (𝕗B.2 (𝕗A.2 .liftr.1 a0))
585+
{_ ⤇ 𝕗𝕎 A.0 B.0 𝕗A.0 𝕗B.0} {_ ⤇ 𝕗𝕎 A.1 B.1 𝕗A.1 𝕗B.1}
586+
(_ ⤇ refl 𝕗𝕎 A.2 B.2 𝕗A.2 𝕗B.2)
587+
.trr.1 f0)]
588+
| .trl.e ↦ [
589+
| sup. a1 f1 ↦
590+
sup. (𝕗A.2 .trl.1 a1)
591+
(refl 𝕗Π (B.2 (𝕗A.2 .liftl.1 a1)) {_ ⤇ 𝕎 A.0 B.0} {_ ⤇ 𝕎 A.1 B.1}
592+
(_ ⤇ refl 𝕎 A.2 B.2) (𝕗B.2 (𝕗A.2 .liftl.1 a1))
593+
{_ ⤇ 𝕗𝕎 A.0 B.0 𝕗A.0 𝕗B.0} {_ ⤇ 𝕗𝕎 A.1 B.1 𝕗A.1 𝕗B.1}
594+
(_ ⤇ refl 𝕗𝕎 A.2 B.2 𝕗A.2 𝕗B.2)
595+
.trl.1 f1)]
596+
{` Just transport/lift in a Π `}
597+
| .liftr.e ↦ [
598+
| sup. a0 f0 ↦
599+
sup. (𝕗A.2 .liftr.1 a0)
600+
(refl 𝕗Π (B.2 (𝕗A.2 .liftr.1 a0)) {_ ⤇ 𝕎 A.0 B.0} {_ ⤇ 𝕎 A.1 B.1}
601+
(_ ⤇ refl 𝕎 A.2 B.2) (𝕗B.2 (𝕗A.2 .liftr.1 a0))
602+
{_ ⤇ 𝕗𝕎 A.0 B.0 𝕗A.0 𝕗B.0} {_ ⤇ 𝕗𝕎 A.1 B.1 𝕗A.1 𝕗B.1}
603+
(_ ⤇ refl 𝕗𝕎 A.2 B.2 𝕗A.2 𝕗B.2)
604+
.liftr.1 f0)]
605+
| .liftl.e ↦ [
606+
| sup. a1 f1 ↦
607+
sup. (𝕗A.2 .liftl.1 a1)
608+
(refl 𝕗Π (B.2 (𝕗A.2 .liftl.1 a1)) {_ ⤇ 𝕎 A.0 B.0} {_ ⤇ 𝕎 A.1 B.1}
609+
(_ ⤇ refl 𝕎 A.2 B.2) (𝕗B.2 (𝕗A.2 .liftl.1 a1))
610+
{_ ⤇ 𝕗𝕎 A.0 B.0 𝕗A.0 𝕗B.0} {_ ⤇ 𝕗𝕎 A.1 B.1 𝕗A.1 𝕗B.1}
611+
(_ ⤇ refl 𝕗𝕎 A.2 B.2 𝕗A.2 𝕗B.2)
612+
.liftl.1 f1)]
613+
| .id.e ↦ x0 x1 ↦
614+
𝕗eqv (𝕎_code A.0 A.1 A.2 B.0 B.1 B.2 x0 x1) (refl 𝕎 A.2 B.2 x0 x1)
615+
(Id_𝕎_iso A.0 A.1 A.2 B.0 B.1 B.2 x0 x1)
616+
(𝕗_𝕎_code A.0 A.1 A.2 B.0 B.1 B.2 𝕗A.0 𝕗A.1 𝕗A.2 𝕗B.0 𝕗B.1 𝕗B.2 x0 x1)]
617+
262618
{` Gel types `}
263619

264620
def Gel (A B : Type) (R : A → B → Type) : Id Type A B ≔ sig a b ↦ (
@@ -277,26 +633,3 @@ def 𝕗Gel (A B : Type) (R : A → B → Type)
277633
(𝕗R : (a : A) (b : B) → isFibrant (R a b)) (a : A) (b : B)
278634
: isFibrant (Gel A B R a b)
279635
≔ 𝕗eqv (R a b) (Gel A B R a b) (Gel_iso A B R a b) (𝕗R a b)
280-
281-
{` The universe `}
282-
283-
{`
284-
def over_and_back (B0 B1 : Fib) (B2 : Id Fib B0 B1) (b0 : B0 .t)
285-
: Id B0 .t (B2 .f .trl.1 (B2 .f .trr.1 b0)) b0
286-
≔ B2⁽ᵉ¹⁾
287-
.f
288-
.id.1 (B2 .f .liftl.1 (B2 .f .trr.1 b0)) (B2 .f .liftr.1 b0)
289-
.trl.1 (refl (B2 .f .trr.1 b0))
290-
291-
def 𝕗Fib : isFibrant Fib ≔ [
292-
| .trr.e ↦ X ↦ X
293-
| .trl.e ↦ X ↦ X
294-
| .liftr.e ↦ X ↦ refl X
295-
| .liftl.e ↦ X ↦ refl X
296-
| .id.e ↦ A B ↦ [
297-
| .trr.e ↦ C0 ↦ ?
298-
| .trl.e ↦ C1 ↦ ?
299-
| .liftr.e ↦ C0 ↦ ?
300-
| .liftl.e ↦ C1 ↦ ?
301-
| .id.e ↦ C0 C1 ↦ ?]]
302-
`}

0 commit comments

Comments
 (0)