oxilean_std/parametricity/functions.rs
1//! Auto-generated module
2//!
3//! ๐ค Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use oxilean_kernel::{BinderInfo, Declaration, Environment, Expr, Level, Name};
6
7use super::types::LogicalRelation;
8
9pub fn app(f: Expr, a: Expr) -> Expr {
10 Expr::App(Box::new(f), Box::new(a))
11}
12pub fn app2(f: Expr, a: Expr, b: Expr) -> Expr {
13 app(app(f, a), b)
14}
15pub fn app3(f: Expr, a: Expr, b: Expr, c: Expr) -> Expr {
16 app(app2(f, a, b), c)
17}
18pub fn app4(f: Expr, a: Expr, b: Expr, c: Expr, d: Expr) -> Expr {
19 app(app3(f, a, b, c), d)
20}
21pub fn cst(s: &str) -> Expr {
22 Expr::Const(Name::str(s), vec![])
23}
24pub fn prop() -> Expr {
25 Expr::Sort(Level::zero())
26}
27pub fn type0() -> Expr {
28 Expr::Sort(Level::succ(Level::zero()))
29}
30pub fn type1() -> Expr {
31 Expr::Sort(Level::succ(Level::succ(Level::zero())))
32}
33pub fn pi(bi: BinderInfo, name: &str, dom: Expr, body: Expr) -> Expr {
34 Expr::Pi(bi, Name::str(name), Box::new(dom), Box::new(body))
35}
36pub(super) fn arrow(a: Expr, b: Expr) -> Expr {
37 pi(BinderInfo::Default, "_", a, b)
38}
39pub fn impl_pi(name: &str, dom: Expr, body: Expr) -> Expr {
40 pi(BinderInfo::Implicit, name, dom, body)
41}
42pub fn bvar(n: u32) -> Expr {
43 Expr::BVar(n)
44}
45pub fn nat_ty() -> Expr {
46 cst("Nat")
47}
48/// `Rel : Type โ Type โ Type`
49///
50/// The type of binary relations between two types.
51/// `Rel A B = A โ B โ Prop`.
52pub fn rel_ty() -> Expr {
53 arrow(type0(), arrow(type0(), type0()))
54}
55/// `RelId : โ (A : Type), Rel A A`
56///
57/// The identity relation on A: `RelId A a a' โ a = a'`.
58pub fn rel_id_ty() -> Expr {
59 pi(
60 BinderInfo::Default,
61 "A",
62 type0(),
63 app2(cst("Rel"), bvar(0), bvar(0)),
64 )
65}
66/// `RelComp : โ {A B C : Type}, Rel A B โ Rel B C โ Rel A C`
67///
68/// Relational composition: (R โ S)(a, c) โ โ b, R(a,b) โง S(b,c).
69pub fn rel_comp_ty() -> Expr {
70 impl_pi(
71 "A",
72 type0(),
73 impl_pi(
74 "B",
75 type0(),
76 impl_pi(
77 "C",
78 type0(),
79 arrow(
80 app2(cst("Rel"), bvar(2), bvar(1)),
81 arrow(
82 app2(cst("Rel"), bvar(2), bvar(1)),
83 app2(cst("Rel"), bvar(4), bvar(2)),
84 ),
85 ),
86 ),
87 ),
88 )
89}
90/// `RelConverse : โ {A B : Type}, Rel A B โ Rel B A`
91///
92/// The converse relation: R^op(b, a) โ R(a, b).
93pub fn rel_converse_ty() -> Expr {
94 impl_pi(
95 "A",
96 type0(),
97 impl_pi(
98 "B",
99 type0(),
100 arrow(
101 app2(cst("Rel"), bvar(1), bvar(0)),
102 app2(cst("Rel"), bvar(1), bvar(2)),
103 ),
104 ),
105 )
106}
107/// `RelFun : โ {A B C D : Type}, Rel A B โ Rel C D โ Rel (A โ C) (B โ D)`
108///
109/// Lifting of relations to function types: the "function relation" between AโC and BโD
110/// induced by relations R : Rel A B and S : Rel C D.
111/// `RelFun R S f g โ โ a b, R a b โ S (f a) (g b)`.
112pub fn rel_fun_ty() -> Expr {
113 impl_pi(
114 "A",
115 type0(),
116 impl_pi(
117 "B",
118 type0(),
119 impl_pi(
120 "C",
121 type0(),
122 impl_pi(
123 "D",
124 type0(),
125 arrow(
126 app2(cst("Rel"), bvar(3), bvar(2)),
127 arrow(
128 app2(cst("Rel"), bvar(3), bvar(2)),
129 app2(cst("Rel"), arrow(bvar(5), bvar(3)), arrow(bvar(5), bvar(3))),
130 ),
131 ),
132 ),
133 ),
134 ),
135 )
136}
137/// `ReynoldsParametricity : Prop`
138///
139/// The fundamental parametricity theorem (Reynolds 1983):
140/// Every polymorphic term f : โ ฮฑ. F(ฮฑ) satisfies the relation F(R) for every
141/// relation R between types A and B.
142/// Stated as an axiom at the metatheory level.
143pub fn reynolds_parametricity_ty() -> Expr {
144 prop()
145}
146/// `ParametricFunction : โ {F : Type โ Type}, (โ ฮฑ, F ฮฑ) โ Prop`
147///
148/// Predicate: a polymorphic function is parametric if it preserves all relations.
149/// `ParametricFunction f โ โ A B (R : Rel A B), Lift_F R (f A) (f B)`.
150pub fn parametric_function_ty() -> Expr {
151 impl_pi(
152 "F",
153 arrow(type0(), type0()),
154 arrow(
155 pi(BinderInfo::Default, "ฮฑ", type0(), app(bvar(1), bvar(0))),
156 prop(),
157 ),
158 )
159}
160/// `ParametricityCondition : โ {A B : Type} (R : Rel A B) {F : Type โ Type},
161/// (โ ฮฑ, F ฮฑ) โ Prop`
162///
163/// The parametricity condition for a specific relation R and functor F:
164/// the polymorphic function maps R-related inputs to F(R)-related outputs.
165pub fn parametricity_condition_ty() -> Expr {
166 impl_pi(
167 "A",
168 type0(),
169 impl_pi(
170 "B",
171 type0(),
172 pi(
173 BinderInfo::Default,
174 "R",
175 app2(cst("Rel"), bvar(1), bvar(0)),
176 impl_pi(
177 "F",
178 arrow(type0(), type0()),
179 arrow(
180 pi(BinderInfo::Default, "ฮฑ", type0(), app(bvar(1), bvar(0))),
181 prop(),
182 ),
183 ),
184 ),
185 ),
186 )
187}
188/// `RelTypeConstructor : (Type โ Type) โ (Type โ Type โ Type)`
189///
190/// Lifting of type constructors to relational type constructors.
191/// `RelTypeConstructor F A B = Rel (F A) (F B)`.
192pub fn rel_type_constructor_ty() -> Expr {
193 arrow(
194 arrow(type0(), type0()),
195 arrow(type0(), arrow(type0(), type0())),
196 )
197}
198/// `FreeTheorem : โ (ฯ : Type), Prop`
199///
200/// The free theorem associated to a polymorphic type ฯ.
201/// By Wadler's theorem-for-free, every inhabitant of โ ฮฑ. ฯ(ฮฑ) satisfies a
202/// non-trivial equational property determined by ฯ.
203pub fn free_theorem_ty() -> Expr {
204 arrow(type0(), prop())
205}
206/// `FreeTheoremId : โ {A B : Type} (f : โ ฮฑ, ฮฑ โ ฮฑ),
207/// โ (x : A), f A x = x`
208///
209/// Free theorem for the identity type โ ฮฑ, ฮฑ โ ฮฑ:
210/// Any parametric function of this type must be the identity.
211pub fn free_theorem_id_ty() -> Expr {
212 impl_pi(
213 "A",
214 type0(),
215 impl_pi(
216 "B",
217 type0(),
218 pi(
219 BinderInfo::Default,
220 "f",
221 pi(BinderInfo::Default, "ฮฑ", type0(), arrow(bvar(0), bvar(0))),
222 pi(
223 BinderInfo::Default,
224 "x",
225 bvar(2),
226 app3(cst("Eq"), bvar(3), app(bvar(1), bvar(3)), bvar(0)),
227 ),
228 ),
229 ),
230 )
231}
232/// `FreeTheoremList : โ {A B : Type} (f : โ ฮฑ, List ฮฑ โ List ฮฑ) (g : A โ B),
233/// map g (f A xs) = f B (map g xs)`
234///
235/// Free theorem for โ ฮฑ, List ฮฑ โ List ฮฑ:
236/// Every parametric such function commutes with map.
237pub fn free_theorem_list_ty() -> Expr {
238 impl_pi(
239 "A",
240 type0(),
241 impl_pi(
242 "B",
243 type0(),
244 pi(
245 BinderInfo::Default,
246 "f",
247 pi(
248 BinderInfo::Default,
249 "ฮฑ",
250 type0(),
251 arrow(app(cst("List"), bvar(0)), app(cst("List"), bvar(0))),
252 ),
253 pi(BinderInfo::Default, "g", arrow(bvar(2), bvar(1)), prop()),
254 ),
255 ),
256 )
257}
258/// `FreeTheoremFold : โ {A B : Type}
259/// (f : โ ฮฑ ฮฒ, (ฮฑ โ ฮฒ โ ฮฒ) โ ฮฒ โ List ฮฑ โ ฮฒ),
260/// โ (h : A โ B) (op : A โ A โ A) (z : A),
261/// h (f A A op z xs) = f B B (fun a b -> h (op a ...)) (h z) (map h xs)`
262///
263/// A free theorem for fold-like polymorphic functions.
264pub fn free_theorem_fold_ty() -> Expr {
265 impl_pi(
266 "A",
267 type0(),
268 impl_pi(
269 "B",
270 type0(),
271 pi(
272 BinderInfo::Default,
273 "f",
274 pi(
275 BinderInfo::Default,
276 "ฮฑ",
277 type0(),
278 pi(
279 BinderInfo::Default,
280 "ฮฒ",
281 type0(),
282 arrow(
283 arrow(bvar(1), arrow(bvar(0), bvar(0))),
284 arrow(bvar(1), arrow(app(cst("List"), bvar(2)), bvar(2))),
285 ),
286 ),
287 ),
288 prop(),
289 ),
290 ),
291 )
292}
293/// `Naturality : โ {F G : Type โ Type} (ฮท : โ ฮฑ, F ฮฑ โ G ฮฑ),
294/// โ {A B : Type} (f : A โ B), G f โ ฮท A = ฮท B โ F f`
295///
296/// A parametric polymorphic function ฮท is a natural transformation.
297pub fn naturality_ty() -> Expr {
298 impl_pi(
299 "F",
300 arrow(type0(), type0()),
301 impl_pi(
302 "G",
303 arrow(type0(), type0()),
304 pi(
305 BinderInfo::Default,
306 "ฮท",
307 pi(
308 BinderInfo::Default,
309 "ฮฑ",
310 type0(),
311 arrow(app(bvar(2), bvar(0)), app(bvar(2), bvar(0))),
312 ),
313 impl_pi(
314 "A",
315 type0(),
316 impl_pi("B", type0(), arrow(arrow(bvar(1), bvar(0)), prop())),
317 ),
318 ),
319 ),
320 )
321}
322/// `DiNaturality : โ {F : Type โ Type โ Type} (ฮฑ : โ A, F A A),
323/// โ {A B : Type} (f : A โ B), ...`
324///
325/// Dinaturality: a parametric function of mixed-variance type is a dinatural
326/// transformation, meaning it satisfies a hexagon identity.
327pub fn dinaturality_ty() -> Expr {
328 impl_pi(
329 "F",
330 arrow(type0(), arrow(type0(), type0())),
331 pi(
332 BinderInfo::Default,
333 "ฮฑ",
334 pi(
335 BinderInfo::Default,
336 "A",
337 type0(),
338 app2(bvar(1), bvar(0), bvar(0)),
339 ),
340 impl_pi(
341 "A",
342 type0(),
343 impl_pi("B", type0(), arrow(arrow(bvar(1), bvar(0)), prop())),
344 ),
345 ),
346 )
347}
348/// `NaturalTransformation : (Type โ Type) โ (Type โ Type) โ Type`
349///
350/// The type of natural transformations between two functors F and G.
351/// `NaturalTransformation F G = { ฮท : โ ฮฑ, F ฮฑ โ G ฮฑ | Naturality ฮท }`.
352pub fn natural_transformation_ty() -> Expr {
353 arrow(
354 arrow(type0(), type0()),
355 arrow(arrow(type0(), type0()), type0()),
356 )
357}
358/// `NaturalIso : (Type โ Type) โ (Type โ Type) โ Type`
359///
360/// A natural isomorphism between functors.
361pub fn natural_iso_ty() -> Expr {
362 arrow(
363 arrow(type0(), type0()),
364 arrow(arrow(type0(), type0()), type0()),
365 )
366}
367/// `AbstractType : Type`
368///
369/// An abstract type is an existential package: `โ (ฮฑ : Type), Interface ฮฑ`.
370/// This models information hiding and encapsulation.
371pub fn abstract_type_ty() -> Expr {
372 type0()
373}
374/// `AbstractPackage : โ (Interface : Type โ Prop), Type`
375///
376/// A package hiding the concrete representation type:
377/// `AbstractPackage I = โ (ฮฑ : Type), I ฮฑ ร ฮฑ`.
378pub fn abstract_package_ty() -> Expr {
379 arrow(arrow(type0(), prop()), type0())
380}
381/// `RepresentationIndependence : โ {I : Type โ Prop}
382/// (pkg1 pkg2 : AbstractPackage I), Prop`
383///
384/// Two abstract packages with the same interface are observationally equivalent:
385/// no client program can distinguish them.
386pub fn representation_independence_ty() -> Expr {
387 impl_pi(
388 "I",
389 arrow(type0(), prop()),
390 arrow(
391 app(cst("AbstractPackage"), bvar(0)),
392 arrow(app(cst("AbstractPackage"), bvar(1)), prop()),
393 ),
394 )
395}
396/// `AbstractionTheorem : โ {I : Type โ Prop}
397/// (pkg1 pkg2 : AbstractPackage I),
398/// RepresentationIndependence pkg1 pkg2`
399///
400/// Reynolds' abstraction theorem: any two implementations of an interface
401/// are representationally independent.
402pub fn abstraction_theorem_ty() -> Expr {
403 impl_pi(
404 "I",
405 arrow(type0(), prop()),
406 pi(
407 BinderInfo::Default,
408 "pkg1",
409 app(cst("AbstractPackage"), bvar(0)),
410 pi(
411 BinderInfo::Default,
412 "pkg2",
413 app(cst("AbstractPackage"), bvar(1)),
414 app2(cst("RepresentationIndependence"), bvar(1), bvar(0)),
415 ),
416 ),
417 )
418}
419/// `ExistentialType : (Type โ Type) โ Type`
420///
421/// Existential quantification over types: `โ ฮฑ. F ฮฑ`.
422/// Models abstract data types in System F.
423pub fn existential_type_ty() -> Expr {
424 arrow(arrow(type0(), type0()), type0())
425}
426/// `Pack : โ {F : Type โ Type} (A : Type), F A โ ExistentialType F`
427///
428/// Packing a concrete implementation into an abstract package.
429pub fn pack_ty() -> Expr {
430 impl_pi(
431 "F",
432 arrow(type0(), type0()),
433 pi(
434 BinderInfo::Default,
435 "A",
436 type0(),
437 arrow(app(bvar(1), bvar(0)), app(cst("ExistentialType"), bvar(2))),
438 ),
439 )
440}
441/// `Unpack : โ {F : Type โ Type} {R : Prop},
442/// ExistentialType F โ (โ A, F A โ R) โ R`
443///
444/// Unpacking (elimination) for existential types.
445pub fn unpack_ty() -> Expr {
446 impl_pi(
447 "F",
448 arrow(type0(), type0()),
449 impl_pi(
450 "R",
451 prop(),
452 arrow(
453 app(cst("ExistentialType"), bvar(1)),
454 arrow(
455 pi(
456 BinderInfo::Default,
457 "A",
458 type0(),
459 arrow(app(bvar(3), bvar(0)), bvar(2)),
460 ),
461 bvar(1),
462 ),
463 ),
464 ),
465 )
466}
467/// `LogicalRelation : โ (F : Type โ Type), Type`
468///
469/// A logical relation over a type constructor F:
470/// `LogicalRelation F = โ A B, Rel A B โ Rel (F A) (F B)`.
471/// This is the relational interpretation of F in a parametric model.
472pub fn logical_relation_ty() -> Expr {
473 pi(
474 BinderInfo::Default,
475 "F",
476 arrow(type0(), type0()),
477 pi(
478 BinderInfo::Default,
479 "A",
480 type0(),
481 pi(
482 BinderInfo::Default,
483 "B",
484 type0(),
485 arrow(
486 app2(cst("Rel"), bvar(1), bvar(0)),
487 app2(cst("Rel"), app(bvar(3), bvar(2)), app(bvar(3), bvar(1))),
488 ),
489 ),
490 ),
491 )
492}
493/// `FundamentalLemma : โ (ฯ : Type) (f : ฯ),
494/// LogicalRelation_at ฯ (f, f)`
495///
496/// The fundamental lemma of logical relations: every typeable term is related
497/// to itself by the logical relation of its type.
498pub fn fundamental_lemma_ty() -> Expr {
499 pi(BinderInfo::Default, "ฯ", type0(), arrow(bvar(0), prop()))
500}
501/// `ClosedRelation : โ {F : Type โ Type}, LogicalRelation F โ Prop`
502///
503/// A logical relation is closed (a.k.a. admissible) if it is preserved by
504/// least fixed points (needed for recursive types).
505pub fn closed_relation_ty() -> Expr {
506 impl_pi(
507 "F",
508 arrow(type0(), type0()),
509 arrow(app(cst("LogicalRelation"), bvar(0)), prop()),
510 )
511}
512/// `RelationalModel : Type`
513///
514/// A relational model of System F: assigns to each type a carrier set and
515/// a logical relation, satisfying the parametricity condition for all terms.
516pub fn relational_model_ty() -> Expr {
517 type0()
518}
519/// `ParametricModel : RelationalModel โ Prop`
520///
521/// A relational model is parametric if every definable function in System F
522/// is interpreted by a parametric element (one that lives in all logical relations
523/// connecting related inputs).
524pub fn parametric_model_ty() -> Expr {
525 arrow(cst("RelationalModel"), prop())
526}
527/// `SystemFType : Type`
528///
529/// Types of System F (second-order polymorphic lambda calculus):
530/// โ ฮฑ. ฯ, ฯโ โ ฯโ, base types.
531pub fn system_f_type_ty() -> Expr {
532 type0()
533}
534/// `SystemFTerm : SystemFType โ Type`
535///
536/// Terms of System F of a given type.
537pub fn system_f_term_ty() -> Expr {
538 arrow(cst("SystemFType"), type0())
539}
540/// `PolymorphicId : โ (ฮฑ : Type), ฮฑ โ ฮฑ`
541///
542/// The polymorphic identity function: the unique inhabitant of โ ฮฑ, ฮฑ โ ฮฑ
543/// (up to parametricity).
544pub fn polymorphic_id_ty() -> Expr {
545 pi(BinderInfo::Default, "ฮฑ", type0(), arrow(bvar(0), bvar(0)))
546}
547/// `PolymorphicConst : โ (ฮฑ ฮฒ : Type), ฮฑ โ ฮฒ โ ฮฑ`
548///
549/// The polymorphic constant (K combinator): the unique inhabitant of โ ฮฑ ฮฒ, ฮฑ โ ฮฒ โ ฮฑ.
550pub fn polymorphic_const_ty() -> Expr {
551 pi(
552 BinderInfo::Default,
553 "ฮฑ",
554 type0(),
555 pi(
556 BinderInfo::Default,
557 "ฮฒ",
558 type0(),
559 arrow(bvar(1), arrow(bvar(1), bvar(2))),
560 ),
561 )
562}
563/// `PolymorphicFlip : โ (ฮฑ ฮฒ ฮณ : Type), (ฮฑ โ ฮฒ โ ฮณ) โ ฮฒ โ ฮฑ โ ฮณ`
564///
565/// The flip combinator.
566pub fn polymorphic_flip_ty() -> Expr {
567 pi(
568 BinderInfo::Default,
569 "ฮฑ",
570 type0(),
571 pi(
572 BinderInfo::Default,
573 "ฮฒ",
574 type0(),
575 pi(
576 BinderInfo::Default,
577 "ฮณ",
578 type0(),
579 arrow(
580 arrow(bvar(2), arrow(bvar(1), bvar(0))),
581 arrow(bvar(2), arrow(bvar(3), bvar(3))),
582 ),
583 ),
584 ),
585 )
586}
587/// `ChurchNumeral : (โ ฮฑ, (ฮฑ โ ฮฑ) โ ฮฑ โ ฮฑ) โ Nat`
588///
589/// Church numerals in System F: โ ฮฑ. (ฮฑ โ ฮฑ) โ ฮฑ โ ฮฑ.
590/// Parametricity implies these are exactly the natural numbers.
591pub fn church_numeral_ty() -> Expr {
592 pi(
593 BinderInfo::Default,
594 "ฮฑ",
595 type0(),
596 arrow(arrow(bvar(0), bvar(0)), arrow(bvar(1), bvar(1))),
597 )
598}
599/// `ChurchBool : (โ ฮฑ, ฮฑ โ ฮฑ โ ฮฑ) โ Bool`
600///
601/// Church booleans in System F: โ ฮฑ. ฮฑ โ ฮฑ โ ฮฑ.
602/// Parametricity implies these are exactly true and false.
603pub fn church_bool_ty() -> Expr {
604 pi(
605 BinderInfo::Default,
606 "ฮฑ",
607 type0(),
608 arrow(bvar(0), arrow(bvar(1), bvar(1))),
609 )
610}
611/// `CoherenceTheorem : โ {F : Type โ Type}
612/// (f g : โ ฮฑ, F ฮฑ), f = g`
613///
614/// The coherence theorem via parametricity:
615/// In a polymorphic type with sufficient constraints (e.g., functor laws),
616/// all parallel morphisms are equal. Parametricity gives coherence for free.
617pub fn coherence_theorem_ty() -> Expr {
618 impl_pi(
619 "F",
620 arrow(type0(), type0()),
621 pi(
622 BinderInfo::Default,
623 "f",
624 pi(BinderInfo::Default, "ฮฑ", type0(), app(bvar(1), bvar(0))),
625 pi(
626 BinderInfo::Default,
627 "g",
628 pi(BinderInfo::Default, "ฮฑ", type0(), app(bvar(2), bvar(0))),
629 app3(
630 cst("Eq"),
631 pi(BinderInfo::Default, "ฮฑ", type0(), app(bvar(3), bvar(0))),
632 bvar(1),
633 bvar(0),
634 ),
635 ),
636 ),
637 )
638}
639/// `ParametricityCoherence : โ {A B : Type} {F : Type โ Type โ Type}
640/// (f g : โ ฮฑ ฮฒ, F ฮฑ ฮฒ), f = g`
641///
642/// Coherence for bifunctors: parametricity forces all polymorphic terms
643/// of the same type to be equal (up to the relevant equations).
644pub fn parametricity_coherence_ty() -> Expr {
645 impl_pi(
646 "A",
647 type0(),
648 impl_pi(
649 "B",
650 type0(),
651 impl_pi(
652 "F",
653 arrow(type0(), arrow(type0(), type0())),
654 pi(
655 BinderInfo::Default,
656 "f",
657 pi(
658 BinderInfo::Default,
659 "ฮฑ",
660 type0(),
661 pi(
662 BinderInfo::Default,
663 "ฮฒ",
664 type0(),
665 app2(bvar(3), bvar(1), bvar(0)),
666 ),
667 ),
668 pi(
669 BinderInfo::Default,
670 "g",
671 pi(
672 BinderInfo::Default,
673 "ฮฑ",
674 type0(),
675 pi(
676 BinderInfo::Default,
677 "ฮฒ",
678 type0(),
679 app2(bvar(4), bvar(1), bvar(0)),
680 ),
681 ),
682 prop(),
683 ),
684 ),
685 ),
686 ),
687 )
688}
689/// `UniqueInhabitant : โ (ฯ : โ ฮฑ, F ฮฑ), Prop`
690///
691/// Parametricity can imply uniqueness: some polymorphic types have a unique
692/// (up to propositional equality) inhabitant by the free theorem.
693pub fn unique_inhabitant_ty() -> Expr {
694 impl_pi(
695 "F",
696 arrow(type0(), type0()),
697 arrow(
698 pi(BinderInfo::Default, "ฮฑ", type0(), app(bvar(1), bvar(0))),
699 prop(),
700 ),
701 )
702}
703/// `UniversalProperty : โ {F : Type โ Type}, (โ ฮฑ, F ฮฑ) โ Prop`
704///
705/// A polymorphic function satisfies a universal property if it is the unique
706/// natural transformation of its type โ which parametricity guarantees for
707/// many common functors.
708pub fn universal_property_ty() -> Expr {
709 impl_pi(
710 "F",
711 arrow(type0(), type0()),
712 arrow(
713 pi(BinderInfo::Default, "ฮฑ", type0(), app(bvar(1), bvar(0))),
714 prop(),
715 ),
716 )
717}
718/// `KripkeRelation : โ (W : Type) (A B : Type), Type`
719///
720/// A Kripke relation over a world type W between A and B:
721/// `W โ A โ B โ Prop`. Used in step-indexed logical relations.
722pub fn kripke_relation_ty() -> Expr {
723 pi(
724 BinderInfo::Default,
725 "W",
726 type0(),
727 pi(
728 BinderInfo::Default,
729 "A",
730 type0(),
731 pi(
732 BinderInfo::Default,
733 "B",
734 type0(),
735 arrow(bvar(2), arrow(bvar(2), arrow(bvar(2), prop()))),
736 ),
737 ),
738 )
739}
740/// `StepIndexedRelation : โ (A B : Type), Type`
741///
742/// A step-indexed (Appel-McAllester) logical relation between A and B,
743/// indexed by a step count n : Nat.
744/// Used to prove parametricity for recursive types (iso-recursive, equi-recursive).
745pub fn step_indexed_relation_ty() -> Expr {
746 pi(
747 BinderInfo::Default,
748 "A",
749 type0(),
750 pi(
751 BinderInfo::Default,
752 "B",
753 type0(),
754 arrow(nat_ty(), arrow(bvar(1), arrow(bvar(2), prop()))),
755 ),
756 )
757}
758/// `BiorthogonalityRelation : โ (A : Type), Type`
759///
760/// The biorthogonality (โฅโฅ) construction used in orthogonality-based
761/// logical relations (e.g., Pitts, Bierman-Pitts).
762/// `Biorthogonal A = { S : Set A | S = S^โฅโฅ }`.
763pub fn biorthogonality_relation_ty() -> Expr {
764 arrow(type0(), type0())
765}
766/// `AdmissibleRelation : โ (A B : Type), Rel A B โ Prop`
767///
768/// An admissible relation is one closed under directed limits (needed for
769/// domain-theoretic models of parametricity).
770pub fn admissible_relation_ty() -> Expr {
771 pi(
772 BinderInfo::Default,
773 "A",
774 type0(),
775 pi(
776 BinderInfo::Default,
777 "B",
778 type0(),
779 arrow(app2(cst("Rel"), bvar(1), bvar(0)), prop()),
780 ),
781 )
782}
783/// `PiType : โ (A : Type) (B : A โ Type), Type`
784///
785/// Dependent function type (Pi-type): ฮ (x : A), B x.
786/// The fundamental dependent type construct.
787pub fn pi_type_ty() -> Expr {
788 pi(
789 BinderInfo::Default,
790 "A",
791 type0(),
792 arrow(arrow(bvar(0), type0()), type0()),
793 )
794}
795/// `SigmaType : โ (A : Type) (B : A โ Type), Type`
796///
797/// Dependent pair type (Sigma-type): ฮฃ (x : A), B x.
798/// The existential type at the propositions-as-types level.
799pub fn sigma_type_ty() -> Expr {
800 pi(
801 BinderInfo::Default,
802 "A",
803 type0(),
804 arrow(arrow(bvar(0), type0()), type0()),
805 )
806}
807/// `SigmaFst : โ {A : Type} {B : A โ Type}, Sigma A B โ A`
808///
809/// First projection of a dependent pair.
810pub fn sigma_fst_ty() -> Expr {
811 impl_pi(
812 "A",
813 type0(),
814 impl_pi(
815 "B",
816 arrow(bvar(0), type0()),
817 arrow(app2(cst("SigmaType"), bvar(1), bvar(0)), bvar(2)),
818 ),
819 )
820}
821/// `SigmaSnd : โ {A : Type} {B : A โ Type} (p : Sigma A B), B (fst p)`
822///
823/// Second projection of a dependent pair.
824pub fn sigma_snd_ty() -> Expr {
825 impl_pi(
826 "A",
827 type0(),
828 impl_pi(
829 "B",
830 arrow(bvar(0), type0()),
831 pi(
832 BinderInfo::Default,
833 "p",
834 app2(cst("SigmaType"), bvar(1), bvar(0)),
835 app(bvar(1), app(cst("SigmaFst"), bvar(0))),
836 ),
837 ),
838 )
839}
840/// `PiExt : โ {A : Type} {B : A โ Type} (f g : ฮ x, B x),
841/// (โ x, f x = g x) โ f = g`
842///
843/// Eta-extensionality for Pi-types: pointwise equal functions are equal.
844pub fn pi_ext_ty() -> Expr {
845 impl_pi(
846 "A",
847 type0(),
848 impl_pi(
849 "B",
850 arrow(bvar(0), type0()),
851 pi(
852 BinderInfo::Default,
853 "f",
854 app2(cst("PiType"), bvar(1), bvar(0)),
855 pi(
856 BinderInfo::Default,
857 "g",
858 app2(cst("PiType"), bvar(2), bvar(1)),
859 arrow(
860 pi(
861 BinderInfo::Default,
862 "x",
863 bvar(3),
864 app3(
865 cst("Eq"),
866 app(bvar(3), bvar(0)),
867 app(bvar(2), bvar(0)),
868 app(bvar(1), bvar(0)),
869 ),
870 ),
871 app3(
872 cst("Eq"),
873 app2(cst("PiType"), bvar(3), bvar(2)),
874 bvar(1),
875 bvar(0),
876 ),
877 ),
878 ),
879 ),
880 ),
881 )
882}
883/// `IdType : โ {A : Type}, A โ A โ Type`
884///
885/// Martin-Lรถf identity type: `Id A a b` is the type of proofs that `a = b`.
886pub fn id_type_ty() -> Expr {
887 impl_pi("A", type0(), arrow(bvar(0), arrow(bvar(1), type0())))
888}
889/// `IdRefl : โ {A : Type} (a : A), Id A a a`
890///
891/// Reflexivity: the canonical element of the identity type.
892pub fn id_refl_ty() -> Expr {
893 impl_pi(
894 "A",
895 type0(),
896 pi(
897 BinderInfo::Default,
898 "a",
899 bvar(0),
900 app2(cst("IdType"), bvar(1), bvar(0)),
901 ),
902 )
903}
904/// `IdElim : โ {A : Type} (C : โ a b, Id A a b โ Type)
905/// (refl_case : โ a, C a a (IdRefl a))
906/// {a b : A} (p : Id A a b), C a b p`
907///
908/// The J eliminator (path induction).
909pub fn id_elim_ty() -> Expr {
910 impl_pi(
911 "A",
912 type0(),
913 pi(
914 BinderInfo::Default,
915 "C",
916 pi(
917 BinderInfo::Default,
918 "a",
919 bvar(0),
920 pi(
921 BinderInfo::Default,
922 "b",
923 bvar(1),
924 arrow(app2(cst("IdType"), bvar(2), bvar(0)), type0()),
925 ),
926 ),
927 pi(
928 BinderInfo::Default,
929 "refl_case",
930 pi(
931 BinderInfo::Default,
932 "a",
933 bvar(1),
934 app3(bvar(2), bvar(0), bvar(0), app(cst("IdRefl"), bvar(0))),
935 ),
936 impl_pi(
937 "a",
938 bvar(2),
939 impl_pi(
940 "b",
941 bvar(3),
942 pi(
943 BinderInfo::Default,
944 "p",
945 app2(cst("IdType"), bvar(4), bvar(0)),
946 app3(bvar(4), bvar(2), bvar(1), bvar(0)),
947 ),
948 ),
949 ),
950 ),
951 ),
952 )
953}
954/// `IdSymm : โ {A : Type} {a b : A}, Id A a b โ Id A b a`
955///
956/// Symmetry of the identity type.
957pub fn id_symm_ty() -> Expr {
958 impl_pi(
959 "A",
960 type0(),
961 impl_pi(
962 "a",
963 bvar(0),
964 impl_pi(
965 "b",
966 bvar(1),
967 arrow(
968 app2(cst("IdType"), bvar(2), bvar(0)),
969 app2(cst("IdType"), bvar(1), bvar(3)),
970 ),
971 ),
972 ),
973 )
974}
975/// `IdTrans : โ {A : Type} {a b c : A},
976/// Id A a b โ Id A b c โ Id A a c`
977///
978/// Transitivity (composition) of identity types.
979pub fn id_trans_ty() -> Expr {
980 impl_pi(
981 "A",
982 type0(),
983 impl_pi(
984 "a",
985 bvar(0),
986 impl_pi(
987 "b",
988 bvar(1),
989 impl_pi(
990 "c",
991 bvar(2),
992 arrow(
993 app2(cst("IdType"), bvar(3), bvar(1)),
994 arrow(
995 app2(cst("IdType"), bvar(3), bvar(0)),
996 app2(cst("IdType"), bvar(4), bvar(2)),
997 ),
998 ),
999 ),
1000 ),
1001 ),
1002 )
1003}
1004/// `TypeEquiv : โ (A B : Type), Type`
1005///
1006/// Type equivalence: A โ B. A pair (f : A โ B, g : B โ A) with
1007/// g โ f ~ id and f โ g ~ id.
1008pub fn type_equiv_ty() -> Expr {
1009 pi(
1010 BinderInfo::Default,
1011 "A",
1012 type0(),
1013 pi(BinderInfo::Default, "B", type0(), type0()),
1014 )
1015}
1016/// `UnivalenceAxiom : โ (A B : Type), (A โ B) โ (Id Type A B)`
1017///
1018/// The univalence axiom (Voevodsky): equivalence of types is equivalent
1019/// to identity of types. Implies function extensionality.
1020pub fn univalence_axiom_ty() -> Expr {
1021 pi(
1022 BinderInfo::Default,
1023 "A",
1024 type0(),
1025 pi(
1026 BinderInfo::Default,
1027 "B",
1028 type0(),
1029 app2(
1030 cst("TypeEquiv"),
1031 app2(cst("TypeEquiv"), bvar(1), bvar(0)),
1032 app2(cst("IdType"), type0(), bvar(1)),
1033 ),
1034 ),
1035 )
1036}
1037/// `FunExt : โ {A : Type} {B : A โ Type} (f g : ฮ x, B x),
1038/// (โ x, f x = g x) โ f = g`
1039///
1040/// Function extensionality: pointwise equal functions are propositionally equal.
1041/// A consequence of univalence.
1042pub fn funext_ty() -> Expr {
1043 impl_pi(
1044 "A",
1045 type0(),
1046 impl_pi(
1047 "B",
1048 arrow(bvar(0), type0()),
1049 pi(
1050 BinderInfo::Default,
1051 "f",
1052 app2(cst("PiType"), bvar(1), bvar(0)),
1053 pi(
1054 BinderInfo::Default,
1055 "g",
1056 app2(cst("PiType"), bvar(2), bvar(1)),
1057 arrow(
1058 pi(
1059 BinderInfo::Default,
1060 "x",
1061 bvar(3),
1062 app2(cst("IdType"), app(bvar(3), bvar(0)), app(bvar(2), bvar(0))),
1063 ),
1064 app2(cst("IdType"), bvar(1), bvar(0)),
1065 ),
1066 ),
1067 ),
1068 ),
1069 )
1070}
1071/// `PropExt : โ (P Q : Prop), (P โ Q) โ P = Q`
1072///
1073/// Propositional extensionality: logically equivalent propositions are equal.
1074pub fn prop_ext_ty() -> Expr {
1075 pi(
1076 BinderInfo::Default,
1077 "P",
1078 prop(),
1079 pi(
1080 BinderInfo::Default,
1081 "Q",
1082 prop(),
1083 arrow(
1084 app2(cst("Iff"), bvar(1), bvar(0)),
1085 app2(cst("IdType"), bvar(1), bvar(0)),
1086 ),
1087 ),
1088 )
1089}
1090/// `Trunc : Type โ Prop`
1091///
1092/// Propositional truncation (squash type): |A| is the proposition that A
1093/// is inhabited. The mere existence quantifier.
1094pub fn trunc_ty() -> Expr {
1095 arrow(type0(), prop())
1096}
1097/// `TruncIn : โ {A : Type}, A โ Trunc A`
1098///
1099/// Introduction rule for propositional truncation.
1100pub fn trunc_in_ty() -> Expr {
1101 impl_pi("A", type0(), arrow(bvar(0), app(cst("Trunc"), bvar(1))))
1102}
1103/// `TruncElim : โ {A : Type} {P : Prop},
1104/// (A โ P) โ Trunc A โ P`
1105///
1106/// Elimination into propositions.
1107pub fn trunc_elim_ty() -> Expr {
1108 impl_pi(
1109 "A",
1110 type0(),
1111 impl_pi(
1112 "P",
1113 prop(),
1114 arrow(
1115 arrow(bvar(1), bvar(0)),
1116 arrow(app(cst("Trunc"), bvar(2)), bvar(1)),
1117 ),
1118 ),
1119 )
1120}
1121/// `CircleHIT : Type`
1122///
1123/// The circle Sยน as a higher inductive type with one point and one path.
1124/// `base : Sยน` and `loop : Id Sยน base base`.
1125pub fn circle_hit_ty() -> Expr {
1126 type0()
1127}
1128/// `SuspensionHIT : Type โ Type`
1129///
1130/// Suspension ฮฃA of a type A, a HIT with North, South poles and a meridian
1131/// path for each `a : A`.
1132pub fn suspension_hit_ty() -> Expr {
1133 arrow(type0(), type0())
1134}
1135/// `IntervalHIT : Type`
1136///
1137/// The interval [0,1] as a HIT with two endpoints and a path between them.
1138pub fn interval_hit_ty() -> Expr {
1139 type0()
1140}
1141/// `PushoutHIT : โ {A B C : Type}, (A โ B) โ (A โ C) โ Type`
1142///
1143/// The pushout of two functions, a fundamental HIT for homotopy type theory.
1144pub fn pushout_hit_ty() -> Expr {
1145 impl_pi(
1146 "A",
1147 type0(),
1148 impl_pi(
1149 "B",
1150 type0(),
1151 impl_pi(
1152 "C",
1153 type0(),
1154 arrow(
1155 arrow(bvar(2), bvar(1)),
1156 arrow(arrow(bvar(3), bvar(1)), type0()),
1157 ),
1158 ),
1159 ),
1160 )
1161}
1162/// `ObsEq : โ (A : Type) (a b : A), Prop`
1163///
1164/// Observational equality: a =_A b. In OTT this is defined by recursion on
1165/// the type A, making it definitionally proof-irrelevant.
1166pub fn obs_eq_ty() -> Expr {
1167 pi(
1168 BinderInfo::Default,
1169 "A",
1170 type0(),
1171 arrow(bvar(0), arrow(bvar(1), prop())),
1172 )
1173}
1174/// `ObsEqRefl : โ {A : Type} (a : A), ObsEq A a a`
1175///
1176/// Reflexivity of observational equality.
1177pub fn obs_eq_refl_ty() -> Expr {
1178 impl_pi(
1179 "A",
1180 type0(),
1181 pi(
1182 BinderInfo::Default,
1183 "a",
1184 bvar(0),
1185 app3(cst("ObsEq"), bvar(1), bvar(0), bvar(0)),
1186 ),
1187 )
1188}
1189/// `Coerce : โ {A B : Type}, A = B โ A โ B`
1190///
1191/// Coercion / transport along a type equality.
1192pub fn coerce_ty() -> Expr {
1193 impl_pi(
1194 "A",
1195 type0(),
1196 impl_pi(
1197 "B",
1198 type0(),
1199 arrow(
1200 app2(cst("IdType"), bvar(1), bvar(0)),
1201 arrow(bvar(2), bvar(2)),
1202 ),
1203 ),
1204 )
1205}
1206/// `Coherence : โ {A B : Type} (p q : A = B), p = q`
1207///
1208/// Proof irrelevance for type equalities in OTT: all coercions from A to B
1209/// are propositionally equal.
1210pub fn coherence_ott_ty() -> Expr {
1211 impl_pi(
1212 "A",
1213 type0(),
1214 impl_pi(
1215 "B",
1216 type0(),
1217 pi(
1218 BinderInfo::Default,
1219 "p",
1220 app2(cst("IdType"), bvar(1), bvar(0)),
1221 pi(
1222 BinderInfo::Default,
1223 "q",
1224 app2(cst("IdType"), bvar(2), bvar(1)),
1225 app2(cst("IdType"), bvar(1), bvar(0)),
1226 ),
1227 ),
1228 ),
1229 )
1230}
1231/// `FibrantType : Type โ Prop`
1232///
1233/// Fibrant types are those that satisfy the Kan filling condition.
1234/// In two-level type theory, the inner level consists of fibrant types.
1235pub fn fibrant_type_ty() -> Expr {
1236 arrow(type0(), prop())
1237}
1238/// `StrictEquality : โ (A : Type) (a b : A), Prop`
1239///
1240/// Strict (definitional) equality in the outer level of 2LTT.
1241/// This is a decidable, trivial propositional equality.
1242pub fn strict_equality_ty() -> Expr {
1243 pi(
1244 BinderInfo::Default,
1245 "A",
1246 type0(),
1247 arrow(bvar(0), arrow(bvar(1), prop())),
1248 )
1249}
1250/// `InnerToOuter : โ {A : Type}, FibrantType A โ A โ A`
1251///
1252/// Embedding from the inner fibrant level to the outer strict level.
1253pub fn inner_to_outer_ty() -> Expr {
1254 impl_pi(
1255 "A",
1256 type0(),
1257 arrow(app(cst("FibrantType"), bvar(0)), arrow(bvar(1), bvar(2))),
1258 )
1259}
1260/// `Setoid : Type`
1261///
1262/// A setoid is a type equipped with an equivalence relation.
1263/// `Setoid = ฮฃ (A : Type), (A โ A โ Prop) ร IsEquiv`.
1264pub fn setoid_ty() -> Expr {
1265 type0()
1266}
1267/// `SetoidMap : Setoid โ Setoid โ Type`
1268///
1269/// A setoid morphism respects the equivalence relations.
1270pub fn setoid_map_ty() -> Expr {
1271 arrow(cst("Setoid"), arrow(cst("Setoid"), type0()))
1272}
1273/// `SetoidEquiv : Setoid โ Setoid โ Prop`
1274///
1275/// Two setoids are equivalent if there is a setoid isomorphism between them.
1276pub fn setoid_equiv_ty() -> Expr {
1277 arrow(cst("Setoid"), arrow(cst("Setoid"), prop()))
1278}
1279/// `SetoidQuotient : โ (S : Setoid), Type`
1280///
1281/// The quotient type of a setoid: the type of equivalence classes.
1282pub fn setoid_quotient_ty() -> Expr {
1283 arrow(cst("Setoid"), type0())
1284}
1285/// `PCA : Type`
1286///
1287/// A Partial Combinatory Algebra (PCA): the base structure for realizability.
1288/// Equipped with an application operation that may be partial.
1289pub fn pca_ty() -> Expr {
1290 type0()
1291}
1292/// `Realizer : โ (A : Type), PCA โ Prop`
1293///
1294/// A realizer for an element of A: a PCA element that witnesses the
1295/// computational content of an element of A.
1296pub fn realizer_ty() -> Expr {
1297 arrow(type0(), arrow(cst("PCA"), prop()))
1298}
1299/// `RealizabilityTripos : Type`
1300///
1301/// A tripos (a higher-order fibration) arising from realizability.
1302/// The Kleene realizability tripos is the canonical example.
1303pub fn realizability_tripos_ty() -> Expr {
1304 type0()
1305}
1306/// `EffectiveTopos : Type`
1307///
1308/// The effective topos (Hyland 1982): the realizability topos over
1309/// Kleene's first algebra. Models constructive mathematics with
1310/// all functions being computable.
1311pub fn effective_topos_ty() -> Expr {
1312 type0()
1313}
1314/// `PER : Type โ Type`
1315///
1316/// A partial equivalence relation on a type A: a symmetric and transitive
1317/// (but not necessarily reflexive) relation. The domain of a PER is the
1318/// set of elements related to themselves.
1319pub fn per_ty() -> Expr {
1320 arrow(type0(), type0())
1321}
1322/// `PERDomain : โ {A : Type}, PER A โ A โ Prop`
1323///
1324/// The domain of a PER: elements a such that R(a, a).
1325pub fn per_domain_ty() -> Expr {
1326 impl_pi(
1327 "A",
1328 type0(),
1329 arrow(app(cst("PER"), bvar(0)), arrow(bvar(1), prop())),
1330 )
1331}
1332/// `PERMap : โ {A B : Type}, PER A โ PER B โ (A โ B) โ Prop`
1333///
1334/// A function respects two PERs: if R(a, a') then S(f a, f a').
1335pub fn per_map_ty() -> Expr {
1336 impl_pi(
1337 "A",
1338 type0(),
1339 impl_pi(
1340 "B",
1341 type0(),
1342 arrow(
1343 app(cst("PER"), bvar(1)),
1344 arrow(
1345 app(cst("PER"), bvar(1)),
1346 arrow(arrow(bvar(3), bvar(2)), prop()),
1347 ),
1348 ),
1349 ),
1350 )
1351}
1352/// `PERModel : Type`
1353///
1354/// The PER model of a type theory: each type is interpreted as a PER,
1355/// and terms are interpreted as functions respecting the PERs.
1356pub fn per_model_ty() -> Expr {
1357 type0()
1358}
1359/// `Orthogonal : โ {A B C D : Type}, (A โ B) โ (C โ D) โ Prop`
1360///
1361/// Two morphisms are orthogonal if every lifting problem has a unique solution:
1362/// `โ (u : A โ C) (v : B โ D), โ! h, h โ f = u โง g โ h = v`.
1363pub fn orthogonal_ty() -> Expr {
1364 impl_pi(
1365 "A",
1366 type0(),
1367 impl_pi(
1368 "B",
1369 type0(),
1370 impl_pi(
1371 "C",
1372 type0(),
1373 impl_pi(
1374 "D",
1375 type0(),
1376 arrow(
1377 arrow(bvar(3), bvar(2)),
1378 arrow(arrow(bvar(3), bvar(2)), prop()),
1379 ),
1380 ),
1381 ),
1382 ),
1383 )
1384}
1385/// `WFS : Type`
1386///
1387/// A weak factorization system (WFS) on a category: a pair (L, R) of
1388/// morphism classes such that L โฅ R and every morphism factors as
1389/// an L-map followed by an R-map.
1390pub fn wfs_ty() -> Expr {
1391 type0()
1392}
1393/// `SmallObjectArgument : โ (I : Type), WFS`
1394///
1395/// The small object argument: given a set of generating cofibrations I,
1396/// produces a WFS (cof(I), inj(I)).
1397pub fn small_object_argument_ty() -> Expr {
1398 arrow(type0(), cst("WFS"))
1399}
1400/// `DynType : Type`
1401///
1402/// The dynamic type: the type of dynamically-typed values.
1403/// Every type embeds into DynType, and extraction may fail at runtime.
1404pub fn dyn_type_ty() -> Expr {
1405 type0()
1406}
1407/// `Inject : โ {A : Type}, A โ DynType`
1408///
1409/// Injection of a statically-typed value into the dynamic type.
1410pub fn inject_ty() -> Expr {
1411 impl_pi("A", type0(), arrow(bvar(0), cst("DynType")))
1412}
1413/// `Project : โ {A : Type}, DynType โ Option A`
1414///
1415/// Projection (cast) from the dynamic type to a static type.
1416/// May fail if the runtime type does not match.
1417pub fn project_ty() -> Expr {
1418 impl_pi(
1419 "A",
1420 type0(),
1421 arrow(cst("DynType"), app(cst("Option"), bvar(1))),
1422 )
1423}
1424/// `GradualConsistency : โ (A B : Type), Prop`
1425///
1426/// Type consistency in gradual typing: A ~ B holds when A and B are
1427/// compatible under the gradualization, i.e., one could be a specialization
1428/// of the other via the dynamic type.
1429pub fn gradual_consistency_ty() -> Expr {
1430 pi(
1431 BinderInfo::Default,
1432 "A",
1433 type0(),
1434 pi(BinderInfo::Default, "B", type0(), prop()),
1435 )
1436}
1437/// `CastEvidence : โ {A B : Type}, GradualConsistency A B โ A โ B`
1438///
1439/// A cast with explicit evidence of type consistency.
1440pub fn cast_evidence_ty() -> Expr {
1441 impl_pi(
1442 "A",
1443 type0(),
1444 impl_pi(
1445 "B",
1446 type0(),
1447 arrow(
1448 app2(cst("GradualConsistency"), bvar(1), bvar(0)),
1449 arrow(bvar(2), bvar(2)),
1450 ),
1451 ),
1452 )
1453}
1454/// `EffectSig : Type`
1455///
1456/// An algebraic effect signature: a set of operations with arities.
1457/// Example: State sig = { get : Unit โ S, put : S โ Unit }.
1458pub fn effect_sig_ty() -> Expr {
1459 type0()
1460}
1461/// `EffectTree : EffectSig โ Type โ Type`
1462///
1463/// The free monad over an effect signature: computation trees.
1464/// `EffectTree ฮฃ A = Pure A | Op (ฮฃ.op) (ฮฃ.arity op โ EffectTree ฮฃ A)`.
1465pub fn effect_tree_ty() -> Expr {
1466 arrow(cst("EffectSig"), arrow(type0(), type0()))
1467}
1468/// `Handler : โ {ฮฃ : EffectSig} {A B : Type},
1469/// EffectTree ฮฃ A โ (A โ B) โ (โ op, ฮฃ.arity op โ (ฮฃ.result op โ B) โ B) โ B`
1470///
1471/// Effect handler: interprets an effect tree using a pure return case
1472/// and operation cases.
1473pub fn handler_ty() -> Expr {
1474 impl_pi(
1475 "ฮฃ",
1476 cst("EffectSig"),
1477 impl_pi(
1478 "A",
1479 type0(),
1480 impl_pi(
1481 "B",
1482 type0(),
1483 arrow(
1484 app2(cst("EffectTree"), bvar(2), bvar(1)),
1485 arrow(arrow(bvar(2), bvar(1)), bvar(2)),
1486 ),
1487 ),
1488 ),
1489 )
1490}
1491/// `MonadLaw : โ (M : Type โ Type), Prop`
1492///
1493/// The monad laws for M: left unit, right unit, and associativity of bind.
1494pub fn monad_law_ty() -> Expr {
1495 pi(BinderInfo::Default, "M", arrow(type0(), type0()), prop())
1496}
1497/// `MonadMorphism : โ {M N : Type โ Type}, (โ A, M A โ N A) โ Prop`
1498///
1499/// A monad morphism: a natural transformation between monads that commutes
1500/// with return and bind.
1501pub fn monad_morphism_ty() -> Expr {
1502 impl_pi(
1503 "M",
1504 arrow(type0(), type0()),
1505 impl_pi(
1506 "N",
1507 arrow(type0(), type0()),
1508 arrow(
1509 pi(
1510 BinderInfo::Default,
1511 "A",
1512 type0(),
1513 arrow(app(bvar(2), bvar(0)), app(bvar(2), bvar(0))),
1514 ),
1515 prop(),
1516 ),
1517 ),
1518 )
1519}
1520/// Register all parametricity and free theorem axioms into the kernel environment.
1521#[allow(clippy::too_many_arguments)]
1522pub fn register_parametricity(env: &mut Environment) {
1523 let axioms: &[(&str, Expr)] = &[
1524 ("Rel", rel_ty()),
1525 ("RelId", rel_id_ty()),
1526 ("RelComp", rel_comp_ty()),
1527 ("RelConverse", rel_converse_ty()),
1528 ("RelFun", rel_fun_ty()),
1529 ("ReynoldsParametricity", reynolds_parametricity_ty()),
1530 ("ParametricFunction", parametric_function_ty()),
1531 ("ParametricityCondition", parametricity_condition_ty()),
1532 ("RelTypeConstructor", rel_type_constructor_ty()),
1533 ("FreeTheorem", free_theorem_ty()),
1534 ("FreeTheoremId", free_theorem_id_ty()),
1535 ("FreeTheoremList", free_theorem_list_ty()),
1536 ("FreeTheoremFold", free_theorem_fold_ty()),
1537 ("Naturality", naturality_ty()),
1538 ("DiNaturality", dinaturality_ty()),
1539 ("NaturalTransformation", natural_transformation_ty()),
1540 ("NaturalIso", natural_iso_ty()),
1541 ("AbstractType", abstract_type_ty()),
1542 ("AbstractPackage", abstract_package_ty()),
1543 (
1544 "RepresentationIndependence",
1545 representation_independence_ty(),
1546 ),
1547 ("AbstractionTheorem", abstraction_theorem_ty()),
1548 ("ExistentialType", existential_type_ty()),
1549 ("Pack", pack_ty()),
1550 ("Unpack", unpack_ty()),
1551 ("LogicalRelation", logical_relation_ty()),
1552 ("FundamentalLemma", fundamental_lemma_ty()),
1553 ("ClosedRelation", closed_relation_ty()),
1554 ("RelationalModel", relational_model_ty()),
1555 ("ParametricModel", parametric_model_ty()),
1556 ("SystemFType", system_f_type_ty()),
1557 ("SystemFTerm", system_f_term_ty()),
1558 ("PolymorphicId", polymorphic_id_ty()),
1559 ("PolymorphicConst", polymorphic_const_ty()),
1560 ("PolymorphicFlip", polymorphic_flip_ty()),
1561 ("ChurchNumeral", church_numeral_ty()),
1562 ("ChurchBool", church_bool_ty()),
1563 ("CoherenceTheorem", coherence_theorem_ty()),
1564 ("ParametricityCoherence", parametricity_coherence_ty()),
1565 ("UniqueInhabitant", unique_inhabitant_ty()),
1566 ("UniversalProperty", universal_property_ty()),
1567 ("KripkeRelation", kripke_relation_ty()),
1568 ("StepIndexedRelation", step_indexed_relation_ty()),
1569 ("BiorthogonalityRelation", biorthogonality_relation_ty()),
1570 ("AdmissibleRelation", admissible_relation_ty()),
1571 ("PiType", pi_type_ty()),
1572 ("SigmaType", sigma_type_ty()),
1573 ("SigmaFst", sigma_fst_ty()),
1574 ("SigmaSnd", sigma_snd_ty()),
1575 ("PiExt", pi_ext_ty()),
1576 ("IdType", id_type_ty()),
1577 ("IdRefl", id_refl_ty()),
1578 ("IdElim", id_elim_ty()),
1579 ("IdSymm", id_symm_ty()),
1580 ("IdTrans", id_trans_ty()),
1581 ("TypeEquiv", type_equiv_ty()),
1582 ("UnivalenceAxiom", univalence_axiom_ty()),
1583 ("FunExt", funext_ty()),
1584 ("PropExt", prop_ext_ty()),
1585 ("Trunc", trunc_ty()),
1586 ("TruncIn", trunc_in_ty()),
1587 ("TruncElim", trunc_elim_ty()),
1588 ("CircleHIT", circle_hit_ty()),
1589 ("SuspensionHIT", suspension_hit_ty()),
1590 ("IntervalHIT", interval_hit_ty()),
1591 ("PushoutHIT", pushout_hit_ty()),
1592 ("ObsEq", obs_eq_ty()),
1593 ("ObsEqRefl", obs_eq_refl_ty()),
1594 ("Coerce", coerce_ty()),
1595 ("CoherenceOTT", coherence_ott_ty()),
1596 ("FibrantType", fibrant_type_ty()),
1597 ("StrictEquality", strict_equality_ty()),
1598 ("InnerToOuter", inner_to_outer_ty()),
1599 ("Setoid", setoid_ty()),
1600 ("SetoidMap", setoid_map_ty()),
1601 ("SetoidEquiv", setoid_equiv_ty()),
1602 ("SetoidQuotient", setoid_quotient_ty()),
1603 ("PCA", pca_ty()),
1604 ("Realizer", realizer_ty()),
1605 ("RealizabilityTripos", realizability_tripos_ty()),
1606 ("EffectiveTopos", effective_topos_ty()),
1607 ("PER", per_ty()),
1608 ("PERDomain", per_domain_ty()),
1609 ("PERMap", per_map_ty()),
1610 ("PERModel", per_model_ty()),
1611 ("Orthogonal", orthogonal_ty()),
1612 ("WFS", wfs_ty()),
1613 ("SmallObjectArgument", small_object_argument_ty()),
1614 ("DynType", dyn_type_ty()),
1615 ("Inject", inject_ty()),
1616 ("Project", project_ty()),
1617 ("GradualConsistency", gradual_consistency_ty()),
1618 ("CastEvidence", cast_evidence_ty()),
1619 ("EffectSig", effect_sig_ty()),
1620 ("EffectTree", effect_tree_ty()),
1621 ("Handler", handler_ty()),
1622 ("MonadLaw", monad_law_ty()),
1623 ("MonadMorphism", monad_morphism_ty()),
1624 ];
1625 for (name, ty) in axioms {
1626 env.add(Declaration::Axiom {
1627 name: Name::str(*name),
1628 univ_params: vec![],
1629 ty: ty.clone(),
1630 })
1631 .ok();
1632 }
1633}