diff --git "a/docs/Bonak.\316\275Type.HSet.html" "b/docs/Bonak.\316\275Type.HSet.html" new file mode 100644 index 0000000..bf3a3e2 --- /dev/null +++ "b/docs/Bonak.\316\275Type.HSet.html" @@ -0,0 +1,175 @@ + + + + + +Bonak.νType.HSet + + + + +
+ + + +
+ +

Library Bonak.νType.HSet

+ +
+
+ +
+This file defines HSet and provides unit, sigT and forall on HSet +
+
+ +
+Require Import Logic.FunctionalExtensionality.
+Require Import Logic.Eqdep_dec. Require Import Notation.
+ +
+Set Universe Polymorphism.
+ +
+Record HSet := {
+  Dom:> Type;
+  UIP {x y: Dom} {h g: x = y}: h = g;
+}.
+ +
+
+ +
+unit seen as an HSet +
+
+ +
+Lemma unit_UIP (x y: unit) (h g: x = y): h = g.
+Proof.
+  destruct g, x. now apply UIP_refl_unit.
+Qed.
+ +
+Lemma bool_UIP (x y: bool) (h g: x = y): h = g.
+Proof.
+  destruct g, x. all: now apply UIP_refl_bool.
+Qed.
+ +
+Definition hunit@{m}: HSet@{m} := {|
+  Dom := unit;
+  UIP := unit_UIP;
+|}.
+ +
+Definition hbool@{m}: HSet@{m} := {|
+  Dom := bool;
+  UIP := bool_UIP;
+|}.
+ +
+
+ +
+sigT seen as a type constructor on HSet +
+
+ +
+Lemma sigT_eq {A: Type} {B} {x y: {a: A & B a}}:
+  (x.1; x.2) = (y.1; y.2) → x = y.
+Proof.
+  now repeat rewrite <- sigT_eta.
+Qed.
+ +
+Lemma sigT_decompose_eq {A: Type} {B} {x y: {a: A & B a}} {p: x = y}:
+  p = (sigT_eta x) • (= projT1_eq p; projT2_eq p) • (eq_sym (sigT_eta y)).
+Proof.
+  now destruct p, x.
+Qed.
+ +
+Lemma sigT_decompose {A: Type} {B} {x y: {a: A & B a}} {p q: x = y}
+  {alpha: projT1_eq p = projT1_eq q}
+  {beta: rew [fun r ⇒ rew [fun b: A ⇒ B b] r in x.2 = y.2] alpha in
+   projT2_eq p = projT2_eq q}: p = q.
+Proof.
+  rewrite (sigT_decompose_eq (p := q)), (sigT_decompose_eq (p := p)).
+  destruct x, y; simpl. now destruct beta, alpha.
+Qed.
+ +
+Lemma sigT_UIP {A: HSet} {B: A → HSet} (x y: {a: A & B a}) (p q: x = y): p = q.
+Proof.
+  unshelve eapply sigT_decompose. now apply A. now apply (B y.1).
+Qed.
+ +
+Definition hsigT {A: HSet} (B: A → HSet): HSet := {|
+  Dom := {a: A & B a};
+  UIP := sigT_UIP;
+|}.
+ +
+Set Warnings "-notation-overridden".
+ +
+Notation "{ x & P }" := (hsigT (fun x ⇒ P)): type_scope.
+Notation "{ x : A & P }" := (hsigT (A := A) (fun x ⇒ P)): type_scope.
+ +
+
+ +
+∀ defined over an HSet codomain +
+
+ +
+Lemma hpiT_decompose {A: Type} (B: A → HSet)
+  (f g: ∀ a: A, B a) (p: f = g):
+  functional_extensionality_dep_good _ _ (fun x ⇒ f_equal (fun H ⇒ H x) p) = p.
+Proof.
+  destruct p; simpl; now apply functional_extensionality_dep_good_refl.
+Qed.
+ +
+Definition hpiT_UIP {A: Type} (B: A → HSet)
+  (f g: ∀ a: A, B a) (p q: f = g): p = q.
+Proof.
+  rewrite <- hpiT_decompose with (p := p).
+  rewrite <- hpiT_decompose with (p := q).
+  f_equal.
+  apply functional_extensionality_dep_good; intros a.
+  apply (B a).
+Qed.
+ +
+Definition hpiT {A: Type} (B: A → HSet): HSet.
+Proof.
+  ∃ (∀ a: A, B a). intros x y h g. now apply hpiT_UIP.
+Defined.
+ +
+Notation "'hforall' x , B" := (hpiT (fun x ⇒ B))
+  (x binder, at level 200): type_scope.
+ +
+Notation "'hforall' x : A , B" := (hpiT (fun x: A ⇒ B))
+  (x binder, at level 200): type_scope.
+
+
+ + + +
+ + + \ No newline at end of file diff --git "a/docs/Bonak.\316\275Type.LeInductive.html" "b/docs/Bonak.\316\275Type.LeInductive.html" new file mode 100644 index 0000000..607cb65 --- /dev/null +++ "b/docs/Bonak.\316\275Type.LeInductive.html" @@ -0,0 +1,67 @@ + + + + + +Bonak.νType.LeInductive + + + + +
+ + + +
+ +

Library Bonak.νType.LeInductive

+ +
+Require Import Notation.
+ +
+
+ +
+An inductive definition of le +
+
+Reserved Infix "<~" (at level 70).
+Inductive leI: nat → nat → Type :=
+| leI_refl n: n <~ n
+| leI_down {n p}: p.+1 <~ n → p <~ n
+where "n <~ m" := (leI n m): nat_scope.
+ +
+Lemma leI_up {n p: nat}: n <~ p → n <~ p.+1.
+  induction 1. constructor. now constructor. now constructor.
+Defined.
+ +
+Lemma leI_0 {p}: O <~ p.
+  induction p. now constructor. now apply leI_up.
+Defined.
+ +
+Lemma leI_lower_both {n p}: p.+1 <~ n.+1 → p <~ n.
+  induction 1 using leI_rec with (P := fun p n _ ⇒ pred p <~ pred n).
+  now constructor. destruct p0. now apply leI_0. now constructor.
+Defined.
+ +
+Lemma leI_raise_both {n p}: p <~ n → p.+1 <~ n.+1.
+  induction 1. now constructor. now constructor.
+Defined.
+
+
+ + + +
+ + + \ No newline at end of file diff --git "a/docs/Bonak.\316\275Type.LeYoneda.html" "b/docs/Bonak.\316\275Type.LeYoneda.html" new file mode 100644 index 0000000..5d13500 --- /dev/null +++ "b/docs/Bonak.\316\275Type.LeYoneda.html" @@ -0,0 +1,399 @@ + + + + + +Bonak.νType.LeYoneda + + + + +
+ + + +
+ +

Library Bonak.νType.LeYoneda

+ +
+
+ +
+Two definitions of "less than or equal" in SProp: +
    +
  • Recursive definition + +
    • +
  • "Yoneda trick" + +
    • +
+
+
+ +
+Require Import Notation.
+Require Import LeInductive.
+ +
+Set Warnings "-notation-overridden".
+ +
+
+ +
+False and True in SProp +
+
+Inductive SFalse : SProp :=.
+Inductive STrue : SProp := sI.
+ +
+
+ +
+A recursive definition of le +
+
+Fixpoint leR (n m : nat) : SProp :=
+  match n, m with
+  | O, _ ⇒ STrue
+  | S n, O ⇒ SFalse
+  | S n, S m ⇒ leR n m
+  end.
+ +
+Lemma leR_refl {n} : leR n n.
+Proof.
+  now induction n.
+Qed.
+ +
+
+ +
+A Yoneda-style encoding of the recursive definition of le +
+
+Definition leY n m := ∀ p, leR p n → leR p m.
+Infix "≤" := leY: nat_scope.
+ +
+Inductive eqsprop {A: SProp} (x: A): A → Prop := eqsprop_refl: eqsprop x x.
+Infix "=S" := eqsprop (at level 70): type_scope.
+ +
+Theorem leY_irrelevance: ∀ {n m} (H H': n ≤ m), H =S H'.
+  now reflexivity.
+Qed.
+ +
+
+ +
+A simple contraction used in the next lemma +
+
+Lemma leR_contra {p}: leR p.+1 O → SFalse.
+  now auto.
+Qed.
+ +
+
+ +
+Contradiction of type n.+1 <= 0 +
+
+Theorem leY_contra {n}: n.+1 ≤ O → False.
+  intros. cut SFalse. intro Hn; elim Hn. unfold leY in H.
+  specialize H with (p := 1); eapply leR_contra.
+  apply H; clear H. now auto.
+Qed.
+ +
+Lemma leR_0 {n}: leR O n.
+  destruct n. all: now auto.
+Qed.
+ +
+Lemma leY_0 {n}: O ≤ n.
+  unfold leY. destruct p.
+  - intros O. now apply leR_0.
+  - intros H. now apply leR_contra in H.
+Qed.
+ +
+
+ +
+Reflexivity in leY +
+
+Definition leY_refl n: n ≤ n :=
+  fun _ x ⇒ x. +
+Notation "♢" := leY_refl (at level 0).
+ +
+
+ +
+Transitivity in leY +
+
+Definition leY_trans {n m p} (Hnm: n ≤ m) (Hmp: m ≤ p): n ≤ p :=
+  fun q (Hqn: leR q n) ⇒ Hmp _ (Hnm _ Hqn).
+ +
+Infix "↕" := leY_trans (at level 45).
+ +
+
+ +
+Some trivial inequality proofs in leYoneda +
+
+ +
+Lemma leR_up {n m} (Hnm: leR n m): leR n m.+1.
+  revert m Hnm. induction n. now auto. destruct m. intros H.
+  now apply leR_contra in H. now apply IHn.
+Qed.
+ +
+Lemma leY_up {n m} (Hnm: n ≤ m): n ≤ m.+1.
+  unfold "<=" in ×. intros p Hpn. now apply leR_up, Hnm, Hpn.
+Qed.
+ +
+Notation "↑ h" := (leY_up h) (at level 40).
+ +
+Lemma leR_down {n m} (Hnm: leR n.+1 m): leR n m.
+  revert m Hnm. induction n. now auto. destruct m. intros H.
+  now apply leR_contra in H. now apply IHn.
+Qed.
+ +
+Lemma leY_down {n m} (Hnm: n.+1 ≤ m): n ≤ m.
+  unfold "<=" in ×. intros p Hpn. now apply leR_down, Hnm.
+Qed.
+ +
+Notation "↓ p" := (leY_down p) (at level 40).
+ +
+Lemma leR_lower_both {n m} (Hnm: leR n.+1 m.+1): leR n m.
+  now auto.
+Qed.
+ +
+Lemma leY_lower_both {n m} (Hnm: n.+1 ≤ m.+1): n ≤ m.
+  unfold "<=" in ×. intros p Hpn. now apply leR_lower_both, Hnm.
+Qed.
+ +
+Notation "⇓ p" := (leY_lower_both p) (at level 40).
+ +
+Lemma leR_raise_both {n m} (Hnm: leR n m): leR n.+1 m.+1.
+  now auto.
+Qed.
+ +
+Lemma leY_raise_both {n m} (Hnm: n ≤ m): n.+1 ≤ m.+1.
+  unfold "<=" in ×. intros p Hpn. destruct p. now auto.
+  now apply leR_raise_both, Hnm.
+Qed.
+ +
+Notation "⇑ p" := (leY_raise_both p) (at level 40).
+ +
+
+ +
+A tactic to turn inequalities of the form p.+2 <= q.+1 into p.+2 <= q.+2; + find_raise is a helper for the tactic +
+
+ +
+Ltac find_raise q :=
+  match q with
+  | ?q.+1 ⇒ find_raise q
+  | _ ⇒ constr:(q)
+  end.
+ +
+Ltac invert_le Hpq :=
+  match type of Hpq with
+  | ?p.+1 ≤ ?q ⇒ let c := find_raise q in destruct c;
+                   [exfalso; clear -Hpq; repeat apply leY_lower_both in Hpq;
+                   now apply leY_contra in Hpq |]
+  end.
+ +
+
+ +
+Connecting leI with leY +
+
+ +
+Lemma leY_of_leI {n p}: p <~ n → p ≤ n.
+Proof.
+  intros [refl | q r]. now apply leY_refl. apply leY_down. induction l.
+  now apply leY_refl. now apply leY_down.
+Qed.
+ +
+Lemma leI_of_leY {n p}: p ≤ n → p <~ n.
+Proof.
+  intros H. unfold "<=" in H. specialize H with (1 := leR_refl).
+  revert n H. induction p, n. now constructor.
+  intros _; now apply leI_0. intros H; now contradiction.
+  intros H. simpl in H. apply IHp in H. now apply leI_raise_both.
+Defined.
+ +
+
+ +
+A couple of properties of the two connections, asserting the equality + of morphisms +
+
+ +
+Lemma leI_refl_morphism n: leI_of_leY (♢ n) = leI_refl _.
+Proof.
+  induction n. now simpl.
+  change (leI_refl n.+1) with (leI_raise_both (leI_refl n)). now rewrite <- IHn.
+Qed.
+ +
+Lemma leI_down_morphism {n p} (Hp: p.+1 ≤ n.+1):
+  leI_of_leY (↓ Hp) = leI_down (leI_of_leY Hp).
+Proof.
+  revert n Hp. induction p, n.
+  - unfold leI_of_leY at 1; now simpl.
+  - unfold leI_of_leY; simpl. intros _. induction (leI_up leI_0). now auto.
+    simpl. now rewrite IHl.
+  - intros Hp. exfalso.
+    now apply leY_lower_both, leY_contra in Hp.
+  - intros Hp.
+    change (leI_of_leY (↓ Hp)) with (leI_raise_both (leI_of_leY (↓ ⇓ Hp))).
+    now rewrite IHp.
+Defined.
+ +
+
+ +
+An inductive on leY +
+
+Inductive leYind n : ∀ p, p ≤ n → Type :=
+| leYind_refl : leYind n n (♢ n)
+| leYind_down p Hp : leYind n p.+1 Hp → leYind n p (↓ Hp).
+ +
+
+ +
+A constructor of leYind +
+
+Lemma leYind_construct {n p} Hp: leYind n p Hp.
+Proof.
+  intros; induction (leI_of_leY Hp).
+  - rewrite (leY_irrelevance Hp (♢ n)).     exact (leYind_refl _).
+  - rewrite (leY_irrelevance Hp (↓ (leY_of_leI l))).
+    apply leYind_down, IHl.
+Defined.
+ +
+
+ +
+le_induction along with a couple of computational properties +
+
+ +
+Theorem le_induction {n p} (Hp: p ≤ n) (P: ∀ p (Hp: p ≤ n), Type)
+  (H_base: P n (♢ n))
+  (H_step: ∀ p (Hp: p.+1 ≤ n) (H: P p.+1 Hp), P p (↓ Hp)): P p Hp.
+Proof.
+  induction (leYind_construct Hp); now auto.
+Defined.
+ +
+Lemma le_induction_base_computes {n P H_base H_step}:
+  le_induction (♢ n) P H_base H_step = H_base.
+Proof.
+  unfold le_induction, leYind_construct. rewrite leI_refl_morphism; simpl.
+  now destruct leY_irrelevance.
+Qed.
+ +
+Lemma le_induction_step_computes {n p P H_base H_step} {Hp: p.+1 ≤ n}:
+  le_induction (↓ Hp) P H_base H_step =
+    H_step p Hp (le_induction Hp P H_base H_step).
+Proof.
+  invert_le Hp. unfold le_induction, leYind_construct.
+  rewrite leI_down_morphism; simpl. now destruct leY_irrelevance.
+Qed.
+ +
+
+ +
+Some helper-abbreviations +
+
+ +
+Definition le_induction' {n p} (Hp: p.+1 ≤ n.+1)
+  (P: ∀ p (Hp: p.+1 ≤ n.+1), Type)
+  (H_base: P n (♢ n.+1))
+  (H_step: ∀ p (H : p.+2 ≤ n.+1), P p.+1 H → P p (↓ H)): P p Hp :=
+  le_induction (⇓ Hp) (fun p Hp ⇒ P p (⇑ Hp)) H_base
+    (fun q Hq ⇒ H_step q (⇑ Hq)).
+ +
+Definition le_induction'' {n p} (Hp: p.+2 ≤ n.+2)
+  (P : ∀ p (Hp: p.+2 ≤ n.+2), Type)
+  (H_base: P n (♢ n.+2))
+  (H_step: ∀ p (H : p.+3 ≤ n.+2), P p.+1 H → P p (↓ H)): P p Hp :=
+  le_induction' (⇓ Hp) (fun p Hp ⇒ P p (⇑ Hp)) H_base
+    (fun q Hq ⇒ H_step q (⇑ Hq)).
+ +
+Definition le_induction'_base_computes {n P H_base H_step}:
+  le_induction' (♢ n.+1) P H_base H_step = H_base :=
+  le_induction_base_computes.
+ +
+Definition le_induction'_step_computes {n p P H_base H_step} {Hp: p.+2 ≤ n.+1}:
+  le_induction' (↓ Hp) P H_base H_step =
+    H_step p Hp (le_induction' Hp P H_base H_step) :=
+      le_induction_step_computes.
+
+
+ + + +
+ + + \ No newline at end of file diff --git "a/docs/Bonak.\316\275Type.Notation.html" "b/docs/Bonak.\316\275Type.Notation.html" new file mode 100644 index 0000000..0fdf4c2 --- /dev/null +++ "b/docs/Bonak.\316\275Type.Notation.html" @@ -0,0 +1,79 @@ + + + + + +Bonak.νType.Notation + + + + +
+ + + +
+ +

Library Bonak.νType.Notation

+ +
+
+ +
+Miscellaneous notations and lemmas +
+
+ +
+Notation "( a ; b )" := (existT _ a b).
+Notation "x .1" := (projT1 x) (at level 1, left associativity, format "x .1").
+Notation "x .2" := (projT2 x) (at level 1, left associativity, format "x .2").
+Notation "x .+1" := (S x) (at level 1, left associativity, format "x .+1").
+Notation "x .+2" := (S (S x)) (at level 1, left associativity, format "x .+2").
+Notation "x .+3" := (S (S (S x))) (at level 1, left associativity, format "x .+3").
+ +
+
+ +
+This is in Program.Basics for some strange reason +
+
+Arguments id {A} x.
+ +
+
+ +
+Notations for rew +
+
+Notation "'rew' [ P ] H 'in' H'" := (eq_rect _ P H' _ H)
+    (at level 10, H' at level 10,
+    format "'[' 'rew' [ P ] '/ ' H in '/' H' ']'").
+Notation "'rew' <- [ P ] H 'in' H'" := (eq_rect_r P H' H)
+    (at level 10, H' at level 10,
+    format "'[' 'rew' <- [ P ] '/ ' H in '/' H' ']'").
+ +
+Notation "(= u ; v )" := (eq_existT_curried u v)
+(at level 0, format "(= u ; '/ ' v )").
+ +
+Infix "•" := eq_trans (at level 65, left associativity).
+Notation "[ x ⇒ f ] e" := (f_equal (fun x ⇒ f) e)
+(at level 60, left associativity).
+Notation "x ^" := (eq_sym x) (at level 55, left associativity, format "x ^").
+
+
+ + + +
+ + + \ No newline at end of file diff --git "a/docs/Bonak.\316\275Type.RewLemmas.html" "b/docs/Bonak.\316\275Type.RewLemmas.html" new file mode 100644 index 0000000..63cb1e0 --- /dev/null +++ "b/docs/Bonak.\316\275Type.RewLemmas.html" @@ -0,0 +1,135 @@ + + + + + +Bonak.νType.RewLemmas + + + + +
+ + + +
+ +

Library Bonak.νType.RewLemmas

+ +
+
+ +
+A few rewriting lemmas not in the standard library +
+
+ +
+Import Logic.EqNotations.
+Require Import Notation.
+ +
+Lemma rew_rew {A} {x y: A} (H : x = y) P {a: P x} :
+rew <- [P] H in rew [P] H in a = a.
+  now destruct H.
+Qed.
+ +
+Lemma rew_rew' {A} {x y: A} (H: x = y) P {a: P y} :
+rew [P] H in rew <- [P] H in a = a.
+  now destruct H.
+Qed.
+ +
+Lemma rew_context {A} {x y: A} (eq: x = y) {P} {a: P x}
+{Q: ∀ a, P a → Type}: Q y (rew eq in a) = Q x a.
+  now destruct eq.
+Qed.
+ +
+Lemma rew_pair: ∀ A {a} (P Q: A → Type) (x: P a) (y: Q a)
+  {b} (H: a = b), (rew H in x, rew H in y) =
+                   rew [fun a ⇒ (P a × Q a)%type] H in (x, y).
+Proof.
+  now destruct H.
+Qed.
+ +
+Lemma rew_sigT {A x} {P: A → Type} (Q: ∀ a, P a → Type)
+  (u: { p: P x & Q x p }) {y} (H: x = y)
+    : rew [fun x ⇒ { p : P x & Q x p }] H in u
+      = (rew H in u.1; rew dependent [fun x H ⇒ Q x (rew H in u.1)] H in u.2).
+Proof.
+  now destruct H, u.
+Qed.
+ +
+Lemma rew_existT_curried {A x} {P: A → Type} {Q: {a & P a} → Type}
+   {y} {H: x = y}
+   {u: P x} {v: Q (x; u)}
+   {u': P y} {v': Q (y; u')}
+   {Hu: rew H in u = u'} {Hv: rew (=H; Hu) in v = v'}:
+   rew [fun x ⇒ {a: P x & Q (x; a)}] H in (u; v) = (u'; v').
+Proof.
+   now destruct Hu, Hv, H.
+Qed.
+ +
+Theorem rew_permute A (P Q: A → Type) (x y: A) (H: ∀ z, Q z = P z)
+  (H': x = y) (a: P x) :
+  rew <- [id] H y in rew H' in a =
+  rew [Q] H' in rew <- [id] H x in a.
+Proof.
+  now destruct H'.
+Qed.
+ +
+Theorem rew_permute' A (P Q: A → Type) (x y: A) (H: ∀ z, P z = Q z)
+  (H': x = y) (a: P x) :
+  rew [id] H y in rew H' in a =
+  rew [Q] H' in rew [id] H x in a.
+Proof.
+  now destruct H'.
+Qed.
+ +
+Lemma rew_swap : ∀ A (P : A → Type) a b (H: a = b) (x : P a) (y : P b),
+  x = rew <- H in y ↔ rew H in x = y.
+Proof.
+  now destruct H.
+Qed.
+ +
+Lemma rew_app A (P : A → Type) (x y : A) (H H' : x = y) (a : P x) :
+  H = H' → rew <- [P] H in rew [P] H' in a = a.
+Proof.
+  intros × →. now destruct H'.
+Qed.
+ +
+Lemma eq_ind_r_refl {A} {x y: A} {H: x = y} :
+  eq_ind_r (fun x ⇒ eq x y) eq_refl H = H.
+Proof.
+  now destruct H.
+Qed.
+ +
+Lemma map_subst_app {A B} {x y} {𝛉: A} (H: x = y :> B) (P: A → B → Type)
+  (f: ∀ 𝛉, P 𝛉 x):
+  rew [P 𝛉] H in f 𝛉 = (rew [fun x ⇒ ∀ 𝛉, P 𝛉 x] H in f) 𝛉.
+Proof.
+  now destruct H.
+Defined.
+
+
+ + + +
+ + + \ No newline at end of file diff --git "a/docs/Bonak.\316\275Type.\316\275Type.html" "b/docs/Bonak.\316\275Type.\316\275Type.html" new file mode 100644 index 0000000..657cf2b --- /dev/null +++ "b/docs/Bonak.\316\275Type.\316\275Type.html" @@ -0,0 +1,891 @@ + + + + + +Bonak.νType.νType + + + + +
+ + + +
+ +

Library Bonak.νType.νType

+ +
+
+ +
+An "indexed" construction of ν-parametric sets + For ν=1, this builds augmented semi-simplicial sets + For ν=2, this builds semi-cubical sets +
+
+ +
+Import Logic.EqNotations.
+Require Import Logic.FunctionalExtensionality.
+Require Import Notation.
+Require Import RewLemmas.
+ +
+Set Warnings "-notation-overridden".
+Require Import HSet.
+ +
+Require Import LeYoneda.
+ +
+Set Printing Projections.
+Set Keyed Unification.
+Remove Printing Let sigT.
+Remove Printing Let prod.
+ +
+
+ +
+The universe where the ν-parametric sets live +
+
+Universe m.
+ +
+
+ +
+The universe where the type of ν-parametric sets live +
+
+Universe m'.
+ +
+Section νType.
+
+ +
+The arity ν of parametric sets +
+
+Variable arity: HSet.
+ +
+
+ +
+A ν-parametric set is a family of sets obtained by iterating + Reynolds' parametricity translation. + +
+ + For ν=1: this is a collection of colors, of points depending on a + color, of lines connecting two points of the same color, of + triangles filling a frame made of three connected lines, of + tetrahedra filling a frame made of four glued triangles, etc. + Intuitively, this is: + X₀ : hSet colors + X₁ : X₀ → hSet points + X₂ : Πx₀:X₀. X₁x₀ × X₁x₀ → hSet lines + X₃ : Πx₀:X₀. Πy₀y₁y₂:X₁x₀. X₂x₀(y₀,y₁) × X₂x₀(y₀,y₂) × X₂x₀(y₁y₂) → hSet triangles + ... + Formally, following the recursive recipe defined in the file, + this is equivalently defined as: + X₀ : unit → hSet colors + X₁ : Σ⋆:unit.X₀⋆ → hSet points + X₂ : Σx₁:(Σx₀:(Σ⋆:unit.X₀⋆).X₁x₀).X₁(x₁.1) → hSet lines + X₃ : Σx₂':(Σx₂:(Σx₁':(Σx₁:(Σx₀:(Σ⋆:unit.X₀⋆).X₁x₀).X₁(x₁.1)).X₂(x₁')). + Σx₁:X₁(x₂.1.1).X₂(x₂.1,x₁)). + X₂((x₂'.1.1.1.1,x₂'.1.1.2),x₂'.2.1) → hSet triangles + +
+ + where each Xₙ has generically a type Xₙ : frameₙₙ(X₀,...,Xₙ₋₁) → hSet + +
+ + Above, frameₙₙ has type pspₙ → hSet, where psp, standing for + "parametric set prefix", represents an initial sequence + X₀,...,Xₙ₋₁ of parametric sets. + +
+ + Also, arguments of each Xᵢ in a frame are computed from + previous arguments using "restrictions". These restrictions + themselves obey coherence rules. + +
+ + For ν=2: this is a collection of points, of lines connecting two + points, of squares filling a frame made of four lines, of cubes + filling a frame made of six squares, etc. + Intuitively, this is: + X₀ : hSet points + X₁ : X₀×X₀ → hSet lines + X₂ : Πx₀₀x₀₁x₁₀x₁₁:X₀. X₁x₀₀x₁₀ × X₁x₁₀x₁₁ × X₁x₀₀x₀₁ × X₁x₁₀x₁₁ → hSet squares + +
+ + Formally, it is built on a variant of frame that takes 2 copies of each X instead of 1. + +
+ + The construction mutually builds the type of frames, frame + restrictions and coherence conditions on frame restrictions. + +
+ + Frames +
+ + The construction maintains at each step of the induction the three + last levels of frames (called frame'', frame', frame), the + two restrictions between them (called restrFrame' and + restrFrame) and the coherence between these two restrictions + (called cohFrame). +
+ + FrameBlockPrev consists of the levels we remember before the + current one and for each such previous data, FrameBlock + consists of the data to maintain at the current level. +
+
+Class FrameBlockPrev (n: nat) (prefix: Type@{m'}) := {
+  frame' {p} (Hp: p.+1 ≤ n): prefix → HSet@{m};
+  frame'' {p} (Hp: p.+2 ≤ n): prefix → HSet@{m};
+  restrFrame' {p q} {Hpq: p.+2 ≤ q.+2} (Hq: q.+2 ≤ n) (ε: arity) {D: prefix}:
+    frame' (↓ (Hpq ↕ Hq)) D → frame'' (Hpq ↕ Hq) D;
+}.
+ +
+Arguments frame' {n prefix} _ {p} Hp D.
+Arguments frame'' {n prefix} _ {p} Hp D.
+Arguments restrFrame' {n prefix} _ {p q Hpq} Hq ε {D} d.
+ +
+Class FrameBlock (n p: nat) (prefix: Type@{m'})
+  (FramePrev: FrameBlockPrev n prefix) := {
+  frame (Hp: p ≤ n): prefix → HSet@{m};
+  restrFrame {q} {Hpq: p.+1 ≤ q.+1} (Hq: q.+1 ≤ n) (ε: arity) {D: prefix}:
+    frame (↓ (Hpq ↕ Hq)) D → FramePrev.(frame') (Hpq ↕ Hq) D;
+  cohFrame {q r} {Hpr: p.+2 ≤ r.+2} {Hrq: r.+2 ≤ q.+2} {Hq: q.+2 ≤ n}
+    {ε: arity} {ω: arity} {D: prefix} (d: frame (↓ (⇓ Hpr ↕ (↓ (Hrq ↕ Hq)))) D):
+    FramePrev.(restrFrame') (Hpq := Hpr ↕ Hrq) Hq ε
+      (restrFrame (Hpq := ⇓ Hpr) (↓ (Hrq ↕ Hq)) ω d) =
+    (FramePrev.(restrFrame') (Hpq := Hpr) (Hrq ↕ Hq) ω
+      (restrFrame (Hpq := ↓ (Hpr ↕ Hrq)) Hq ε d));
+}.
+ +
+Arguments frame {n p prefix FramePrev} _ Hp D.
+Arguments restrFrame {n p prefix FramePrev} _ {q Hpq} Hq ε {D} d.
+Arguments cohFrame {n p prefix FramePrev} _ {q r Hpr Hrq Hq ε ω D} d.
+ +
+
+ +
+Paintings +
+ + We build paintings using an iterated construction: a painting at level n + depends on paintings at level n-1 and n-2; just as we have frame' and + frame'', we have painting' and painting''. +
+
+Class PaintingBlockPrev (n: nat) (prefix: Type@{m'})
+  (FramePrev : FrameBlockPrev n prefix) := {
+  painting' {p} {Hp: p.+1 ≤ n} {D: prefix}:
+    FramePrev.(frame') Hp D → HSet@{m};
+  painting'' {p} {Hp: p.+2 ≤ n} {D: prefix}:
+    FramePrev.(frame'') Hp D → HSet@{m};
+  restrPainting' {p q} {Hpq: p.+2 ≤ q.+2} (Hq: q.+2 ≤ n) (ε: arity) {D: prefix}
+    {d : FramePrev.(frame') (↓ (Hpq ↕ Hq)) D}:
+    painting' d → painting'' (FramePrev.(restrFrame') Hq ε d);
+}.
+ +
+Arguments painting' {n prefix FramePrev} _ {p Hp D} d.
+Arguments painting'' {n prefix FramePrev} _ {p Hp D} d.
+Arguments restrPainting' {n prefix FramePrev} _ {p q Hpq} Hq ε {D} [d] b.
+ +
+
+ +
+Painting consists of painting, restrPainting, and coherence conditions between them +
+
+Class PaintingBlock (n: nat) (prefix: Type@{m'})
+  {FramePrev: FrameBlockPrev n prefix}
+  (PaintingPrev: PaintingBlockPrev n prefix FramePrev)
+  (Frame: ∀ {p}, FrameBlock n p prefix FramePrev) := {
+  painting {p} {Hp: p ≤ n} {D: prefix}:
+    (Frame.(frame) (♢ _) D → HSet@{m}) → Frame.(frame) Hp D → HSet@{m};
+  restrPainting {p q} {Hpq: p.+1 ≤ q.+1}
+    (Hq: q.+1 ≤ n) (ε: arity) {D : prefix}
+    {E: Frame.(frame) (♢ _) D → HSet@{m}}
+    {d: Frame.(frame) (↓ (Hpq ↕ Hq)) D} (c: painting E d):
+    PaintingPrev.(painting') (Frame.(restrFrame) Hq ε d);
+  cohPainting {p q r} {Hpr: p.+2 ≤ r.+2}
+    {Hrq: r.+2 ≤ q.+2} {Hq: q.+2 ≤ n}
+    (ε: arity) (ω : arity) {D: prefix} (E: Frame.(frame) (♢ _) D → HSet@{m})
+    (d: Frame.(frame) (↓ (⇓ Hpr ↕ (↓ (Hrq ↕ Hq)))) D) (c: painting E d):
+    rew [PaintingPrev.(painting'')] (Frame.(cohFrame) d) in
+    PaintingPrev.(restrPainting') (Hpq := Hpr ↕ Hrq) Hq
+    ε (restrPainting (Hpq := ⇓ Hpr) (↓ (Hrq ↕ Hq)) ω c) =
+      (PaintingPrev.(restrPainting') (Hpq := Hpr) (Hrq ↕ Hq)
+      ω (restrPainting (Hpq := ↓ (Hpr ↕ Hrq)) Hq ε c));
+}.
+ +
+Arguments painting {n prefix FramePrev PaintingPrev Frame} _ {p Hp D} E.
+Arguments restrPainting {n prefix FramePrev PaintingPrev Frame} _
+  {p q Hpq Hq ε D E} [d] c.
+Arguments cohPainting {n prefix FramePrev PaintingPrev Frame} _
+  {p q r Hpr Hrq Hq ε ω D E d} c.
+ +
+
+ +
+An ν-parametric type truncated at level n consists of: + +
+ +
    +
  • a prefix of parametric types up to dimension n, + +
    • +
  • a type of frames with their restrictions and coherence of + restrictions Frame (depending on their values are dimension n-1 + and n-2) that are Σ-types of length n that is recursively built + out by induction on some p ranging from 0 to n + +
    • +
  • a type of paintings (with their restrictions and coherence of + restrictions) Painting (depending on their values PaintingPrev at + dimensions n-1 and n-2) that are also recursively built out from + partial paintings + +
    • +
  • axioms characterizing the definition of Frame and Painting in + the previous dimensions, so that the induction can be carried + +
    • +
+ +
+
+ +
+Class νType (n : nat) := {
+  prefix: Type@{m'};
+  FramePrev: FrameBlockPrev n prefix;
+  Frame {p}: FrameBlock n p prefix FramePrev;
+  PaintingPrev: PaintingBlockPrev n prefix FramePrev;
+  Painting: PaintingBlock n prefix PaintingPrev (@Frame);
+
+  
+ +
+Abbreviations for ν-family of previous paintings, one for + each ϵ-restriction of the previous frame (ϵ∈ν) +
+
+  Layer {p} {Hp: p.+1 ≤ n} {D: prefix} (d: Frame.(frame) (↓ Hp) D) :=
+    hforall ε, PaintingPrev.(painting') (Frame.(restrFrame) Hp ε d);
+  Layer' {p} {Hp: p.+2 ≤ n} {D: prefix} (d: FramePrev.(frame') (↓ Hp) D) :=
+    hforall ε, PaintingPrev.(painting'') (FramePrev.(restrFrame') Hp ε d);
+  RestrLayer {p q ε} {Hpq: p.+2 ≤ q.+2} {Hq: q.+2 ≤ n} {D: prefix}
+    (d: Frame.(frame) (↓ ↓ (Hpq ↕ Hq)) D) (l: Layer d):
+    Layer' (Frame.(restrFrame) Hq ε d) :=
+  fun ω ⇒ rew [PaintingPrev.(painting'')] Frame.(cohFrame) (Hrq := Hpq) d in
+    PaintingPrev.(restrPainting') Hq ε (l ω);
+
+  
+ +
+Equations carrying the definition of frame and painting from level + n-1 and n-2 +
+
+  eqFrame0 {len0: 0 ≤ n} {D: prefix}: (Frame.(frame) len0 D).(Dom) = unit;
+  eqFrame0' {len1: 1 ≤ n} {D: prefix}:
+    (FramePrev.(frame') len1 D).(Dom) = unit;
+  eqFrameSp {p} {Hp: p.+1 ≤ n} {D: prefix}:
+    Frame.(frame) Hp D = {d: Frame.(frame) (↓ Hp) D & Layer d} :> Type;
+  eqFrameSp' {p} {Hp: p.+2 ≤ n} {D: prefix}:
+    FramePrev.(frame') Hp D = {d : FramePrev.(frame') (↓ Hp) D & Layer' d}
+      :> Type;
+  eqRestrFrame0 {q} {Hpq: 1 ≤ q.+1} {Hq: q.+1 ≤ n} {ε: arity} {D: prefix}:
+    Frame.(restrFrame) (Hpq := Hpq) Hq ε (rew <- [id] eqFrame0 (D := D) in tt) =
+      (rew <- [id] eqFrame0' in tt);
+  eqRestrFrameSp {ε p q} {D: prefix} {Hpq: p.+2 ≤ q.+2} {Hq: q.+2 ≤ n}
+    {d: Frame.(frame) (↓ ↓ (Hpq ↕ Hq)) D}
+    {l: Layer (Hp := ↓ (Hpq ↕ Hq)) d}:
+    Frame.(restrFrame) Hq ε (rew <- [id] eqFrameSp in (d; l)) =
+      rew <- [id] eqFrameSp' in (Frame.(restrFrame) Hq ε d; RestrLayer d l);
+  eqPaintingSp {p} {Hp: p.+1 ≤ n} {D: prefix} {E d}:
+    Painting.(painting) (Hp := ↓ Hp) E d = {l: Layer d &
+      Painting.(painting) (D := D) E (rew <- [id] eqFrameSp in (d; l))} :> Type;
+  eqPaintingSp' {p} {Hp: p.+2 ≤ n} {D: prefix} {d}:
+    PaintingPrev.(painting') (Hp := ↓ Hp) d = {b : Layer' d &
+      PaintingPrev.(painting')
+        (rew <- [id] eqFrameSp' (D := D) in (d; b))} :> Type;
+  eqRestrPainting0 {p} {Hp: p.+1 ≤ n} {D: prefix} {E} {d} {ε: arity}
+    {l: Layer d}
+    {Q: Painting.(painting) (D := D) E (rew <- eqFrameSp in (d; l))}:
+    l ε = Painting.(restrPainting) (Hq := Hp)
+      (rew <- [id] eqPaintingSp in (l; Q));
+  eqRestrPaintingSp {p q} {Hpq: p.+2 ≤ q.+2} {Hq: q.+2 ≤ n} {D: prefix}
+    {E} {d} {ε: arity} {l: Layer (Hp := ↓ (Hpq ↕ Hq)) d}
+    {Q: Painting.(painting) (D := D) E (rew <- eqFrameSp in (d; l))}:
+    Painting.(restrPainting) (Hpq := ↓ Hpq) (ε := ε)
+    (rew <- [id] eqPaintingSp in (l; Q)) =
+      rew <- [id] eqPaintingSp' (Hp := Hpq ↕ Hq) in
+        (RestrLayer d l; rew [PaintingPrev.(painting')] eqRestrFrameSp in
+          Painting.(restrPainting) Q);
+}.
+ +
+Arguments prefix {n} _.
+Arguments FramePrev {n} _.
+Arguments PaintingPrev {n} _.
+Arguments Frame {n} _ {p}.
+Arguments Painting {n} _.
+Arguments Layer {n} _ {p Hp D} d.
+Arguments Layer' {n} _ {p Hp D} d.
+Arguments RestrLayer {n} _ {p q} ε {Hpq Hq D d} l.
+Arguments eqFrame0 {n} _ {len0 D}.
+Arguments eqFrame0' {n} _ {len1 D}.
+Arguments eqFrameSp {n} _ {p Hp D}.
+Arguments eqFrameSp' {n} _ {p Hp D}.
+Arguments eqRestrFrame0 {n} _ {q Hpq Hq ε D}.
+Arguments eqRestrFrameSp {n} _ {ε p q D Hpq Hq d l}.
+Arguments eqPaintingSp {n} _ {p Hp D E d}.
+Arguments eqPaintingSp' {n} _ {p Hp D d}.
+Arguments eqRestrPainting0 {n} _ {p Hp D E d ε l Q}.
+Arguments eqRestrPaintingSp {n} _ {p q Hpq Hq D E d ε l Q}.
+ +
+
+ +
+The construction of νType n+1 from νType n +
+ + Extending the initial prefix +
+
+Definition mkprefix {n} {C: νType n}: Type@{m'} :=
+  sigT (fun D : C.(prefix) ⇒ C.(Frame).(frame) (♢ _) D → HSet@{m}).
+ +
+
+ +
+Memoizing the previous levels of Frame +
+
+Definition mkFramePrev {n} {C: νType n}: FrameBlockPrev n.+1 mkprefix := {|
+  frame' (p: nat) (Hp: p.+1 ≤ n.+1) (D: mkprefix) :=
+    C.(Frame).(frame) (⇓ Hp) D.1;
+  frame'' (p: nat) (Hp: p.+2 ≤ n.+1) (D: mkprefix) :=
+    C.(FramePrev).(frame') (⇓ Hp) D.1;
+  restrFrame' (p q: nat) (Hpq: p.+2 ≤ q.+2) (Hq: q.+2 ≤ n.+1) (ε: arity)
+    (D: mkprefix) (d: _) :=
+    C.(Frame).(restrFrame) (Hpq := ⇓ Hpq) (⇓ Hq) ε d;
+|}.
+ +
+
+ +
+The coherence conditions that Frame needs to satisfy to build the next level + of Frame. These will be used in the proof script of mkFrame. +
+
+ +
+Definition mkLayer {n p} {Hp: p.+1 ≤ n.+1} {C: νType n} {D: mkprefix}
+  {Frame: FrameBlock n.+1 p mkprefix mkFramePrev}
+  {d: Frame.(frame) (↓ Hp) D}: HSet :=
+  hforall ε, C.(Painting).(painting) D.2
+    (Frame.(restrFrame) (Hpq := ♢ _) Hp ε d).
+ +
+Definition mkRestrLayer {n p q} {ε: arity} {Hpq: p.+2 ≤ q.+2}
+  {Hq: q.+2 ≤ n.+1} {C: νType n} {D: mkprefix}
+  {Frame: FrameBlock n.+1 p mkprefix mkFramePrev}
+  (d: Frame.(frame) (↓ ↓ (Hpq ↕ Hq)) D) (l: mkLayer):
+  C.(Layer) (Frame.(restrFrame) Hq ε d) :=
+  fun ω ⇒ rew [C.(PaintingPrev).(painting')] Frame.(cohFrame) d in
+    C.(Painting).(restrPainting) (Hpq := ⇓ Hpq) (l ω).
+ +
+Definition mkCohLayer {n p q r} {ε ω: arity} {Hpr: p.+3 ≤ r.+3}
+  {Hrq: r.+3 ≤ q.+3} {Hq: q.+3 ≤ n.+1} {C: νType n} {D: mkprefix}
+  {Frame: FrameBlock n.+1 p mkprefix mkFramePrev}
+  {d: Frame.(frame) (↓ ↓ ↓ (Hpr ↕ Hrq ↕ Hq)) D} (l: mkLayer):
+  let sl := C.(RestrLayer) (Hpq := ⇓ (Hpr ↕ Hrq)) ε
+              (mkRestrLayer (Hpq := ⇓ Hpr) d l) in
+  let sl' := C.(RestrLayer) (Hpq := ⇓ Hpr) ω
+               (mkRestrLayer (Hpq := ↓ (Hpr ↕ Hrq)) d l) in
+  rew [C.(Layer')] Frame.(cohFrame) (Hpr := ↓ Hpr) (Hrq := Hrq) (Hq := Hq) d in sl = sl'.
+Proof.
+  intros ×.
+  subst sl sl'; apply functional_extensionality_dep; intros 𝛉; unfold Layer'.
+  rewrite <- map_subst_app with
+    (P := fun 𝛉 x ⇒ C.(PaintingPrev).(painting'') (C.(FramePrev).(restrFrame') _ 𝛉 x))
+    (f := C.(RestrLayer) _ (mkRestrLayer d l)).
+  unfold RestrLayer, mkRestrLayer.
+  rewrite <- map_subst with (f := C.(PaintingPrev).(restrPainting') (⇓ Hq) ε).
+  rewrite <- map_subst with
+    (f := C.(PaintingPrev).(restrPainting') (⇓ (Hrq ↕ Hq)) ω).
+  rewrite rew_map with
+    (P := fun x ⇒ (C.(PaintingPrev).(painting'') x).(Dom))
+    (f := fun x ⇒ C.(FramePrev).(restrFrame') (⇓ (Hpr ↕ Hrq) ↕ ⇓ Hq) 𝛉 x).
+  rewrite rew_map with
+    (P := fun x ⇒ (C.(PaintingPrev).(painting'') x).(Dom))
+    (f := fun x ⇒ C.(FramePrev).(restrFrame') (⇓ Hq) ε x).
+  rewrite rew_map with
+    (P := fun x ⇒ (C.(PaintingPrev).(painting'') x).(Dom))
+    (f := fun x ⇒ (C.(FramePrev).(restrFrame') (⇓ (Hrq ↕ Hq)) ω x)).
+  rewrite <- (C.(Painting).(cohPainting) (Hrq := ⇓ Hrq) (Hq := ⇓ Hq)).
+  repeat rewrite rew_compose.
+  apply rew_swap with (P := fun x ⇒ (C.(PaintingPrev).(painting'') x).(Dom)).
+  rewrite rew_app. now reflexivity.
+  now apply (C.(FramePrev).(frame'') _ _).(UIP).
+Qed.
+ +
+
+ +
+The Frame at level n.+1 with p = O +
+
+#[local]
+Instance mkFrame0 {n} {C: νType n}: FrameBlock n.+1 O mkprefix mkFramePrev.
+  unshelve esplit.
+  × intros; now exact hunit.
+  × simpl; intros; rewrite C.(eqFrame0). now exact tt.
+  × simpl; intros.
+    now rewrite eqRestrFrame0 with (Hpq := ⇓ Hpr),
+                eqRestrFrame0 with (Hpq := ⇓ (Hpr ↕ Hrq)).
+Defined.
+ +
+
+ +
+The Frame at level n.+1 for p.+1 knowing the Frame at level n.+1 for p +
+
+#[local]
+Instance mkFrameSp {n p} {C: νType n}
+  {Frame: FrameBlock n.+1 p mkprefix mkFramePrev}:
+  FrameBlock n.+1 p.+1 mkprefix mkFramePrev.
+  unshelve esplit.
+  × intros Hp D; exact {d : Frame.(frame) (↓ Hp) D & mkLayer (d := d)}.
+  × simpl; intros × ε × (d, l); invert_le Hpq.
+    now exact (rew <- [id] C.(eqFrameSp) in
+      (Frame.(restrFrame) Hq ε d; mkRestrLayer d l)).
+  × simpl; intros q r Hpr Hrq Hq ε ω D (d, l).
+    invert_le Hpr; invert_le Hrq.
+ +
+    etransitivity.
+    apply (C.(eqRestrFrameSp) (Hpq := ⇓ (Hpr ↕ Hrq)) (Hq := ⇓ Hq)).
+    etransitivity.
+    2: symmetry; apply (C.(eqRestrFrameSp) (Hpq := ⇓ Hpr) (Hq := ⇓ (Hrq ↕ Hq))).
+ +
+    apply f_equal with (B := C.(FramePrev).(frame') _ D.1)
+      (f := fun x ⇒ rew <- (C.(eqFrameSp') (Hp := ⇓ (Hpr ↕ Hrq) ↕ ⇓ Hq)) in x).
+    now exact (= Frame.(cohFrame) (Hrq := Hrq) d; mkCohLayer l).
+Defined.
+ +
+
+ +
+Finally, we can define mkFrame at level n.+1 for all p +
+
+#[local]
+Instance mkFrame {n} {C: νType n} p: FrameBlock n.+1 p mkprefix mkFramePrev.
+  induction p.
+  + now exact mkFrame0.   + now exact (mkFrameSp (Frame := IHp)). Defined.
+ +
+
+ +
+For Painting, we take a different strategy. We first define mkpainting, + mkRestrPainting, and lemmas corresponding to their computational properties +
+ + First, memoizing the previous levels of Painting +
+
+#[local]
+Instance mkPaintingPrev {n} {C: νType n}:
+  PaintingBlockPrev n.+1 mkprefix mkFramePrev :=
+{|
+  painting' (p: nat) (Hp: p.+1 ≤ n.+1) (D: mkprefix) := C.(Painting).(painting) D.2:
+    mkFramePrev.(frame') Hp D → HSet;
+  painting'' (p: nat) (Hp: p.+2 ≤ n.+1) (D: mkprefix)
+    (d : mkFramePrev.(frame'') Hp D) :=
+    C.(PaintingPrev).(painting') d;
+  restrPainting' (p q: nat) (Hpq: p.+2 ≤ q.+2) (Hq: q.+2 ≤ n.+1) (ε: arity)
+    (D: mkprefix) (d : _) (b : _) := C.(Painting).(restrPainting) (Hpq := ⇓ Hpq)
+    (Hq := ⇓ Hq) (E := D.2) b;
+|}.
+ +
+
+ +
+Then, the component painting of Painting, built by upwards induction from p to n +
+
+ +
+Definition mkpainting {n p} {C: νType n} {Hp: p ≤ n.+1} {D: mkprefix}
+  (E: (mkFrame n.+1).(frame) (♢ _) D → HSet)
+  (d: (mkFrame p).(frame) Hp D): HSet.
+Proof.
+  revert d; apply le_induction with (Hp := Hp); clear p Hp.
+  + now exact E.
+  + intros p Hp mkpaintingSp d; exact {l : mkLayer & mkpaintingSp (d; l)}.
+Defined.
+ +
+Lemma mkpainting_computes {n p} {C: νType n} {Hp: p.+1 ≤ n.+1} {D: mkprefix}
+  {E: (mkFrame n.+1).(frame) (♢ _) D → HSet} {d}:
+  mkpainting (Hp := ↓ Hp) E d =
+  {l : mkLayer & mkpainting (Hp := Hp) E (d; l)} :> Type.
+Proof.
+  unfold mkpainting; now rewrite le_induction_step_computes.
+Qed.
+ +
+
+ +
+Now, restrPainting, and the corresponding computational properties. +
+
+ +
+Definition mkRestrPainting {n} {C: νType n} {p q} {Hpq: p.+1 ≤ q.+1}
+  {Hq: q.+1 ≤ n.+1} {ε: arity} {D}
+  (E: (mkFrame n.+1).(frame) (♢ _) D → HSet)
+  (d: (mkFrame p).(frame) (↓ (Hpq ↕ Hq)) D)
+  (Painting: mkpainting (Hp := ↓ (Hpq ↕ Hq)) E d):
+    mkPaintingPrev.(painting') ((mkFrame p).(restrFrame) Hq ε d).
+Proof.
+  intros *; revert d Painting; simpl.
+  pattern p, Hpq.   apply le_induction'.
+  + intros d c; rewrite mkpainting_computes in c. destruct c as (l, _).
+    now exact (l ε).
+  + clear p Hpq; intros p Hpq mkRestrPaintingSp d c; invert_le Hpq.
+    rewrite mkpainting_computes in c; destruct c as (l, c).
+    change (⇓ (↓ ?Hpq ↕ ?Hq)) with (↓ ⇓ (Hpq ↕ Hq)); rewrite C.(eqPaintingSp).
+    apply mkRestrPaintingSp in c.
+    now exact (mkRestrLayer d l; c).
+Defined.
+ +
+Lemma mkRestrPainting_base_computes {p n} {C: νType n} {Hp: p.+1 ≤ n.+1}
+  {ε: arity} {D E} {d: (mkFrame p).(frame) _ D} {c}:
+  mkRestrPainting (Hq := Hp) E d c =
+  match (rew [id] mkpainting_computes in c) with
+  | (l; _) ⇒ l ε
+  end.
+Proof.
+  unfold mkRestrPainting; now rewrite le_induction'_base_computes.
+Qed.
+ +
+Lemma mkRestrPainting_step_computes {q r n} {C: νType n} {Hq: q.+2 ≤ n.+1}
+  {Hrq: r.+2 ≤ q.+2} {ε: arity} {D E} {d: (mkFrame r).(frame) _ D} {c}:
+  mkRestrPainting (Hpq := ↓ Hrq) (Hq := Hq) (ε := ε) E d c =
+  match (rew [id] mkpainting_computes in c) with
+  | (l; c) ⇒ rew <- [id] C.(eqPaintingSp) in
+    (mkRestrLayer d l; mkRestrPainting (Hpq := Hrq) E (d; l) c)
+  end.
+Proof.
+  unfold mkRestrPainting; now rewrite le_induction'_step_computes.
+Qed.
+ +
+
+ +
+Now, for the last part of the proof: proving coherence conditions + on cohPainting +
+ + The base case is easily discharged +
+
+Definition mkCohPainting_base {q r n} {ε ω: arity} {C: νType n} {D: mkprefix}
+  {Hrq: r.+2 ≤ q.+2} {Hq: q.+2 ≤ n.+1}
+  {E: (mkFrame n.+1).(frame) (♢ _) D → HSet}
+  (d: (mkFrame r).(frame) (↓ ↓ (Hrq ↕ Hq)) D)
+  (c: mkpainting E d):
+  rew [mkPaintingPrev.(painting'')] (mkFrame r).(cohFrame) (Hpr := ♢ _) d in
+    mkPaintingPrev.(restrPainting') (Hpq := Hrq) Hq ε
+      (mkRestrPainting (ε := ω) (Hpq := ♢ _) (Hq := ↓ (Hrq ↕ Hq)) E d c) =
+  mkPaintingPrev.(restrPainting') (Hpq := ♢ _) (Hrq ↕ Hq) ω
+    (mkRestrPainting (ε := ε) (Hpq := ↓ Hrq) (Hq := Hq) E d c).
+Proof.
+  change (♢ _ ↕ ?H) with H; change (⇓ (♢ _) ↕ ?H) with H.
+  rewrite mkRestrPainting_base_computes, mkRestrPainting_step_computes.
+  destruct (rew [id] mkpainting_computes in c) as (l, c'); clear c.
+  now refine (C.(eqRestrPainting0)
+    (Q := mkRestrPainting (Hpq := Hrq) E (_; _) c')).
+Qed.
+ +
+
+ +
+A small abbreviation +
+
+Definition mkCohPaintingHyp p {q r n} {ε ω: arity} {C: νType n} {D: mkprefix}
+  (Hpr: p.+2 ≤ r.+3) {Hrq: r.+3 ≤ q.+3} {Hq: q.+3 ≤ n.+1}
+  {E: (mkFrame n.+1).(frame) (♢ _) D → HSet}
+  (d: (mkFrame p).(frame) (↓ ↓ (Hpr ↕ Hrq ↕ Hq)) D)
+  (c: mkpainting E d) :=
+  rew [mkPaintingPrev.(painting'')] (mkFrame p).(cohFrame) (Hrq := Hrq) d in
+  C.(Painting).(restrPainting) (ε := ε) (Hpq := ⇓ (Hpr ↕ Hrq)) (Hq := ⇓ Hq)
+    (mkRestrPainting (ε := ω) (Hpq := (⇓ Hpr)) (Hq := ↓ (Hrq ↕ Hq)) E d c) =
+  C.(Painting).(restrPainting) (ε := ω) (Hpq := (⇓ Hpr)) (Hq := ⇓ (Hrq ↕ Hq))
+    (mkRestrPainting (ε := ε) (Hpq := ↓ (Hpr ↕ Hrq)) (Hq := Hq) E d c).
+ +
+
+ +
+The step case is discharged as (mkCohLayer; IHP) +
+
+Definition mkCohPainting_step {p q r n} {ε ω: arity} {C: νType n} {D: mkprefix}
+  {Hpr: p.+3 ≤ r.+3} {Hrq: r.+3 ≤ q.+3} {Hq: q.+3 ≤ n.+1}
+  {E: (mkFrame n.+1).(frame) (♢ _) D → HSet}
+  {d: (mkFrame p).(frame) (↓ ↓ (↓ Hpr ↕ Hrq ↕ Hq)) D}
+  {c: mkpainting E d}
+  {IHP: ∀ (d: (mkFrame p.+1).(frame) (↓ ↓ (Hpr ↕ Hrq ↕ Hq)) D)
+        (c: mkpainting E d), mkCohPaintingHyp p.+1 Hpr (ε := ε) (ω := ω) d c}:
+        mkCohPaintingHyp p (↓ Hpr) (ε := ε) (ω := ω) d c.
+Proof.
+  unfold mkCohPaintingHyp in *; simpl projT1 in *; simpl projT2 in ×.
+  change (⇓ (↓ ?Hpr)) with (↓ (⇓ Hpr)).
+  do 2 rewrite mkRestrPainting_step_computes.
+  destruct (rew [id] mkpainting_computes in c) as (l, c'); clear c.
+  rewrite (C.(eqRestrPaintingSp) (Hpq := ⇓ (Hpr ↕ Hrq)) (Hq := ⇓ Hq)).
+  rewrite (C.(eqRestrPaintingSp) (Hpq := ⇓ Hpr) (Hq := ⇓ (Hrq ↕ Hq))).
+  change ((fun _ (x : leR _ ?y) ⇒ x) ↕ ?z) with z.
+  change (⇓ ?x ↕ ⇓ ?y) with (⇓ (x ↕ y)).
+  rewrite <- rew_permute with (H := @eqPaintingSp' _ _ _ (⇓ _) _)
+                              (H' := (mkFrame p).(cohFrame) _).
+  change (↓ ?Hpr ↕ ?Hrq) with (↓ (Hpr ↕ Hrq)).
+  f_equal.
+  unshelve eapply (rew_existT_curried (P := C.(Layer'))
+  (Q := fun x ⇒ C.(PaintingPrev).(painting') (rew <- [id] C.(eqFrameSp') in x))
+  (H := (mkFrame p).(cohFrame) (Hpr := ↓ Hpr) (Hrq := Hrq) (Hq := Hq) (ε := ε)
+        (ω := ω) (D := D) d)
+  (u := C.(RestrLayer) (Hpq := ⇓ (Hpr ↕ Hrq)) (Hq := ⇓ Hq) (D := D.1) ε
+          (mkRestrLayer (Hpq := ⇓ Hpr) (Hq := ↓ (Hrq ↕ Hq)) (C := C) (D := D)
+          (Frame := mkFrame p) (ε := ω) d l))
+  (v := rew [C.(PaintingPrev).(painting')] C.(eqRestrFrameSp) in
+    C.(Painting).(restrPainting) (Hpq := ⇓ (Hpr ↕ Hrq)) (Hq := ⇓ Hq) (ε := ε)
+                       (D := D.1) (E := D.2)
+                       (mkRestrPainting (Hpq := ⇓ Hpr) (Hq := ↓ (Hrq ↕ Hq))
+                       (D := D) (ε := ω) E (d; l) c'))).
+  now exact (mkCohLayer (Hpr := Hpr) (Hrq := Hrq) (Hq := Hq) l).
+  rewrite <- IHP with (d := (d; l)) (c := c').
+  simpl (mkFrame p.+1). unfold mkPaintingPrev, painting''.
+  change (fun x ⇒ C.(PaintingPrev).(painting') (Hp := ?Hp) (D := ?D) x) with
+    (C.(PaintingPrev).(painting') (Hp := Hp) (D := D)).
+  unfold mkFrameSp; unfold cohFrame at -1.
+  rewrite rew_map with (P := fun x ⇒ (C.(PaintingPrev).(painting') x).(Dom))
+                       (f := fun x ⇒ rew <- [id] C.(eqFrameSp') in x).
+  repeat rewrite rew_compose.
+  set (FEQ := f_equal _ _); simpl in FEQ; clearbody FEQ.
+  repeat rewrite <- eq_trans_assoc.
+  now rewrite eq_trans_sym_inv_l, eq_trans_refl_r.
+Qed.
+ +
+
+ +
+Build a PaintingBlock n.+1 using what we just defined +
+
+#[local]
+Instance mkPainting {n} {C: νType n}:
+  PaintingBlock n.+1 mkprefix mkPaintingPrev mkFrame.
+  unshelve esplit; intros p.
+  - intros *; now exact mkpainting.
+  - intros q Hpq Hq ε d; now exact mkRestrPainting.
+  - intros ×. revert d c. pattern p, Hpr. apply le_induction''.
+    + now exact mkCohPainting_base.
+    + clear p Hpr; unfold mkPaintingPrev, restrPainting'; cbv beta iota;
+      intros p Hpr IHP d c; invert_le Hpr; invert_le Hrq.
+      now exact (mkCohPainting_step (IHP := IHP)).
+Defined.
+ +
+
+ +
+The base case of a ν-parametric set (truncated at dimension 0) +
+
+ +
+#[local]
+Instance mkνType0: νType 0.
+  unshelve esplit.
+  - now exact hunit.
+  - unshelve esplit.
+    × intros p Hp; now apply leY_contra in Hp.
+    × intros p Hp; now apply leY_contra in Hp.
+    × intros *; exfalso; now apply leY_contra in Hq.
+  - unshelve esplit.
+    × intros Hp _; now exact hunit.
+    × intros *; exfalso; now apply leY_contra in Hq.
+    × intros *; exfalso; clear -Hq; now apply leY_contra in Hq.
+  - unshelve esplit; intros ×.
+    × exfalso; now apply leY_contra in Hp.
+    × exfalso; now apply leY_contra in Hp.
+    × exfalso; clear -Hq; now apply leY_contra in Hq.
+  - unshelve esplit.
+    × intros p Hp D E d. now exact (E d).
+    × simpl; intros *; exfalso; now apply leY_contra in Hq.
+    × simpl; intros *; exfalso; now apply leY_contra in Hq.
+  - now intros ×.
+  - intros *; exfalso; now apply leY_contra in len1.
+  - intros *; exfalso; now apply leY_contra in Hp.
+  - intros *; exfalso; now apply leY_contra in Hp.
+  - intros *; exfalso; clear -Hq; now apply leY_contra in Hq.
+  - intros *; exfalso; clear -Hp; now apply leY_contra in Hp.
+  - intros *; exfalso; clear -Hp; now apply leY_contra in Hp.
+  - intros *; exfalso; now apply leY_contra in Hq.
+  - intros *; exfalso; clear -Hp; now apply leY_contra in Hp.
+  - intros *; exfalso; clear -Hq; now apply leY_contra in Hq.
+Defined.
+ +
+
+ +
+We are now ready to build an νType n.+1 from an νType n +
+
+#[local]
+Instance mkνTypeSn {n} (C: νType n): νType n.+1 :=
+{|
+    prefix := mkprefix;
+    FramePrev := mkFramePrev;
+    Frame := mkFrame;
+    PaintingPrev := mkPaintingPrev;
+    Painting := mkPainting;
+    eqFrame0 := ltac:(now intros *);
+    eqFrame0' := ltac:(intros *; now apply C.(eqFrame0));
+    eqFrameSp := ltac:(now intros *);
+    eqFrameSp' := ltac:(intros *; now refine C.(eqFrameSp));
+    eqRestrFrame0 := ltac:(now intros *);
+    eqRestrFrameSp := ltac:(now intros *);
+    eqPaintingSp := ltac:(intros *; simpl; now refine mkpainting_computes);
+    eqPaintingSp' := ltac:(intros *; now refine C.(eqPaintingSp));
+    eqRestrPainting0 := ltac:(intros *;
+      change (fun _ (_: leR _ ?q) ⇒ _) with (♢ q); simpl;
+      now rewrite mkRestrPainting_base_computes, rew_rew');
+    eqRestrPaintingSp := ltac:(intros *; simpl;
+      now rewrite mkRestrPainting_step_computes, rew_rew');
+|}.
+ +
+
+ +
+An νType truncated up to dimension n +
+
+Fixpoint νTypeAt n : νType n :=
+  match n with
+  | O ⇒ mkνType0
+  | n.+1 ⇒ mkνTypeSn (νTypeAt n)
+  end.
+ +
+
+ +
+The coinductive suffix of an νType beyond level n +
+
+CoInductive νTypeFrom n (X: (νTypeAt n).(prefix)): Type@{m'} := cons {
+  this: (νTypeAt n).(Frame).(frame) (♢ n) X → HSet@{m};
+  : νTypeFrom n.+1 (X; this);
+}.
+ +
+
+ +
+The final construction +
+
+Definition νTypes := νTypeFrom 0 tt.
+End νType.
+ +
+Definition AugmentedSemiSimplicial := νTypes hunit.
+Definition SemiSimplicial := νTypeFrom hunit 1 (tt; fun _ ⇒ hunit).
+Definition SemiCubical := νTypes hbool.
+ +
+
+ +
+Some examples +
+
+ +
+Notation "{ x : A && P }" := (sigT (A := A) (fun x ⇒ P)): type_scope.
+ +
+Example SemiSimplicial2 := Eval lazy -[projT2] in
+ (νTypeAt hunit 2).(prefix _).
+Print SemiSimplicial2.
+ +
+Example SemiCubical2 := Eval lazy -[projT2] in
+ (νTypeAt hbool 2).(prefix _).
+Print SemiCubical2.
+
+
+ + + +
+ + + \ No newline at end of file diff --git a/docs/coqdoc.css b/docs/coqdoc.css new file mode 100644 index 0000000..48096e5 --- /dev/null +++ b/docs/coqdoc.css @@ -0,0 +1,338 @@ +body { padding: 0px 0px; + margin: 0px 0px; + background-color: white } + +#page { display: block; + padding: 0px; + margin: 0px; + padding-bottom: 10px; } + +#header { display: block; + position: relative; + padding: 0; + margin: 0; + vertical-align: middle; + border-bottom-style: solid; + border-width: thin } + +#header h1 { padding: 0; + margin: 0;} + + +/* Contents */ + +#main{ display: block; + padding: 10px; + font-family: sans-serif; + font-size: 100%; + line-height: 100% } + +#main h1 { line-height: 95% } /* allow for multi-line headers */ + +#main a.idref:visited {color : #416DFF; text-decoration : none; } +#main a.idref:link {color : #416DFF; text-decoration : none; } +#main a.idref:hover {text-decoration : none; } +#main a.idref:active {text-decoration : none; } + +#main a.modref:visited {color : #416DFF; text-decoration : none; } +#main a.modref:link {color : #416DFF; text-decoration : none; } +#main a.modref:hover {text-decoration : none; } +#main a.modref:active {text-decoration : none; } + +#main .keyword { color : #cf1d1d } +#main { color: black } + +.section { background-color: rgb(60%,60%,100%); + padding-top: 13px; + padding-bottom: 13px; + padding-left: 3px; + margin-top: 5px; + margin-bottom: 5px; + font-size : 175% } + +h2.section { background-color: rgb(80%,80%,100%); + padding-left: 3px; + padding-top: 12px; + padding-bottom: 10px; + font-size : 130% } + +h3.section { background-color: rgb(90%,90%,100%); + padding-left: 3px; + padding-top: 7px; + padding-bottom: 7px; + font-size : 115% } + +h4.section { +/* + background-color: rgb(80%,80%,80%); + max-width: 20em; + padding-left: 5px; + padding-top: 5px; + padding-bottom: 5px; +*/ + background-color: white; + padding-left: 0px; + padding-top: 0px; + padding-bottom: 0px; + font-size : 100%; + font-weight : bold; + text-decoration : underline; + } + +#main .doc { margin: 0px; + font-family: sans-serif; + font-size: 100%; + line-height: 125%; + max-width: 40em; + color: black; + padding: 10px; + background-color: #90bdff } + +.inlinecode { + display: inline; +/* font-size: 125%; */ + color: #666666; + font-family: monospace } + +.doc .inlinecode { + display: inline; + font-size: 120%; + color: rgb(30%,30%,70%); + font-family: monospace } + +.doc .inlinecode .id { + color: rgb(30%,30%,70%); +} + +.inlinecodenm { + display: inline; + color: #444444; +} + +.doc .code { + display: inline; + font-size: 120%; + color: rgb(30%,30%,70%); + font-family: monospace } + +.comment { + display: inline; + font-family: monospace; + color: rgb(50%,50%,80%); +} + +.code { + display: block; +/* padding-left: 15px; */ + font-size: 110%; + font-family: monospace; + } + +table.infrule { + border: 0px; + margin-left: 50px; + margin-top: 10px; + margin-bottom: 10px; +} + +td.infrule { + font-family: monospace; + text-align: center; +/* color: rgb(35%,35%,70%); */ + padding: 0px; + line-height: 100%; +} + +tr.infrulemiddle hr { + margin: 1px 0 1px 0; +} + +.infrulenamecol { + color: rgb(60%,60%,60%); + font-size: 80%; + padding-left: 1em; + padding-bottom: 0.1em +} + +/* Pied de page */ + +#footer { font-size: 65%; + font-family: sans-serif; } + +/* Identifiers: ) */ + +.id { display: inline; } + +.id[title="constructor"] { + color: rgb(60%,0%,0%); +} + +.id[title="var"] { + color: rgb(40%,0%,40%); +} + +.id[title="variable"] { + color: rgb(40%,0%,40%); +} + +.id[title="definition"] { + color: rgb(0%,40%,0%); +} + +.id[title="abbreviation"] { + color: rgb(0%,40%,0%); +} + +.id[title="lemma"] { + color: rgb(0%,40%,0%); +} + +.id[title="instance"] { + color: rgb(0%,40%,0%); +} + +.id[title="projection"] { + color: rgb(0%,40%,0%); +} + +.id[title="method"] { + color: rgb(0%,40%,0%); +} + +.id[title="inductive"] { + color: rgb(0%,0%,80%); +} + +.id[title="record"] { + color: rgb(0%,0%,80%); +} + +.id[title="class"] { + color: rgb(0%,0%,80%); +} + +.id[title="keyword"] { + color : #cf1d1d; +/* color: black; */ +} + +/* Deprecated rules using the 'type' attribute of (not xhtml valid) */ + +.id[type="constructor"] { + color: rgb(60%,0%,0%); +} + +.id[type="var"] { + color: rgb(40%,0%,40%); +} + +.id[type="variable"] { + color: rgb(40%,0%,40%); +} + +.id[title="binder"] { + color: rgb(40%,0%,40%); +} + +.id[type="definition"] { + color: rgb(0%,40%,0%); +} + +.id[type="abbreviation"] { + color: rgb(0%,40%,0%); +} + +.id[type="lemma"] { + color: rgb(0%,40%,0%); +} + +.id[type="instance"] { + color: rgb(0%,40%,0%); +} + +.id[type="projection"] { + color: rgb(0%,40%,0%); +} + +.id[type="method"] { + color: rgb(0%,40%,0%); +} + +.id[type="inductive"] { + color: rgb(0%,0%,80%); +} + +.id[type="record"] { + color: rgb(0%,0%,80%); +} + +.id[type="class"] { + color: rgb(0%,0%,80%); +} + +.id[type="keyword"] { + color : #cf1d1d; +/* color: black; */ +} + +.inlinecode .id { + color: rgb(0%,0%,0%); +} + + +/* TOC */ + +#toc h2 { + padding: 10px; + background-color: rgb(60%,60%,100%); +} + +#toc li { + padding-bottom: 8px; +} + +/* Index */ + +#index { + margin: 0; + padding: 0; + width: 100%; +} + +#index #frontispiece { + margin: 1em auto; + padding: 1em; + width: 60%; +} + +.booktitle { font-size : 140% } +.authors { font-size : 90%; + line-height: 115%; } +.moreauthors { font-size : 60% } + +#index #entrance { + text-align: center; +} + +#index #entrance .spacer { + margin: 0 30px 0 30px; +} + +#index #footer { + position: absolute; + bottom: 0; +} + +.paragraph { + height: 0.75em; +} + +ul.doclist { + margin-top: 0em; + margin-bottom: 0em; +} + +.code :target { + border: 2px solid #D4D4D4; + background-color: #e5eecc; +} diff --git a/docs/index.html b/docs/index.html new file mode 100644 index 0000000..6d9c522 --- /dev/null +++ b/docs/index.html @@ -0,0 +1,1258 @@ + + + + + +Bonak + + + + +
+ + + +
+ +

Bonak

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
Global IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(188 entries)
Notation IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(26 entries)
Variable IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(1 entry)
Library IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(6 entries)
Lemma IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(48 entries)
Constructor IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(6 entries)
Projection IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(34 entries)
Inductive IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(5 entries)
Instance IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(7 entries)
Section IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(1 entry)
Definition IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(47 entries)
Record IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(7 entries)
+
+

Global Index

+

A

+AugmentedSemiSimplicial [definition, in Bonak.νType.νType]
+

B

+bool_UIP [lemma, in Bonak.νType.HSet]
+

C

+cohFrame [projection, in Bonak.νType.νType]
+cohPainting [projection, in Bonak.νType.νType]
+

D

+Dom [projection, in Bonak.νType.HSet]
+

E

+eqFrameSp [projection, in Bonak.νType.νType]
+eqFrameSp' [projection, in Bonak.νType.νType]
+eqFrame0 [projection, in Bonak.νType.νType]
+eqFrame0' [projection, in Bonak.νType.νType]
+eqPaintingSp [projection, in Bonak.νType.νType]
+eqPaintingSp' [projection, in Bonak.νType.νType]
+eqRestrFrameSp [projection, in Bonak.νType.νType]
+eqRestrFrame0 [projection, in Bonak.νType.νType]
+eqRestrPaintingSp [projection, in Bonak.νType.νType]
+eqRestrPainting0 [projection, in Bonak.νType.νType]
+eqsprop [inductive, in Bonak.νType.LeYoneda]
+eqsprop_sind [definition, in Bonak.νType.LeYoneda]
+eqsprop_rec [definition, in Bonak.νType.LeYoneda]
+eqsprop_ind [definition, in Bonak.νType.LeYoneda]
+eqsprop_rect [definition, in Bonak.νType.LeYoneda]
+eqsprop_refl [constructor, in Bonak.νType.LeYoneda]
+eq_ind_r_refl [lemma, in Bonak.νType.RewLemmas]
+

F

+Frame [projection, in Bonak.νType.νType]
+frame [projection, in Bonak.νType.νType]
+FrameBlock [record, in Bonak.νType.νType]
+FrameBlockPrev [record, in Bonak.νType.νType]
+FramePrev [projection, in Bonak.νType.νType]
+frame' [projection, in Bonak.νType.νType]
+frame'' [projection, in Bonak.νType.νType]
+

H

+hbool [definition, in Bonak.νType.HSet]
+hpiT [definition, in Bonak.νType.HSet]
+hpiT_UIP [definition, in Bonak.νType.HSet]
+hpiT_decompose [lemma, in Bonak.νType.HSet]
+HSet [record, in Bonak.νType.HSet]
+HSet [library]
+hsigT [definition, in Bonak.νType.HSet]
+hunit [definition, in Bonak.νType.HSet]
+

L

+Layer [projection, in Bonak.νType.νType]
+Layer' [projection, in Bonak.νType.νType]
+leI [inductive, in Bonak.νType.LeInductive]
+LeInductive [library]
+leI_down_morphism [lemma, in Bonak.νType.LeYoneda]
+leI_refl_morphism [lemma, in Bonak.νType.LeYoneda]
+leI_of_leY [lemma, in Bonak.νType.LeYoneda]
+leI_raise_both [lemma, in Bonak.νType.LeInductive]
+leI_lower_both [lemma, in Bonak.νType.LeInductive]
+leI_0 [lemma, in Bonak.νType.LeInductive]
+leI_up [lemma, in Bonak.νType.LeInductive]
+leI_sind [definition, in Bonak.νType.LeInductive]
+leI_rec [definition, in Bonak.νType.LeInductive]
+leI_ind [definition, in Bonak.νType.LeInductive]
+leI_rect [definition, in Bonak.νType.LeInductive]
+leI_down [constructor, in Bonak.νType.LeInductive]
+leI_refl [constructor, in Bonak.νType.LeInductive]
+leR [definition, in Bonak.νType.LeYoneda]
+leR_raise_both [lemma, in Bonak.νType.LeYoneda]
+leR_lower_both [lemma, in Bonak.νType.LeYoneda]
+leR_down [lemma, in Bonak.νType.LeYoneda]
+leR_up [lemma, in Bonak.νType.LeYoneda]
+leR_0 [lemma, in Bonak.νType.LeYoneda]
+leR_contra [lemma, in Bonak.νType.LeYoneda]
+leR_refl [lemma, in Bonak.νType.LeYoneda]
+leY [definition, in Bonak.νType.LeYoneda]
+leYind [inductive, in Bonak.νType.LeYoneda]
+leYind_construct [lemma, in Bonak.νType.LeYoneda]
+leYind_sind [definition, in Bonak.νType.LeYoneda]
+leYind_rec [definition, in Bonak.νType.LeYoneda]
+leYind_ind [definition, in Bonak.νType.LeYoneda]
+leYind_rect [definition, in Bonak.νType.LeYoneda]
+leYind_down [constructor, in Bonak.νType.LeYoneda]
+leYind_refl [constructor, in Bonak.νType.LeYoneda]
+LeYoneda [library]
+leY_of_leI [lemma, in Bonak.νType.LeYoneda]
+leY_raise_both [lemma, in Bonak.νType.LeYoneda]
+leY_lower_both [lemma, in Bonak.νType.LeYoneda]
+leY_down [lemma, in Bonak.νType.LeYoneda]
+leY_up [lemma, in Bonak.νType.LeYoneda]
+leY_trans [definition, in Bonak.νType.LeYoneda]
+leY_refl [definition, in Bonak.νType.LeYoneda]
+leY_0 [lemma, in Bonak.νType.LeYoneda]
+leY_contra [lemma, in Bonak.νType.LeYoneda]
+leY_irrelevance [lemma, in Bonak.νType.LeYoneda]
+le_induction'_step_computes [definition, in Bonak.νType.LeYoneda]
+le_induction'_base_computes [definition, in Bonak.νType.LeYoneda]
+le_induction'' [definition, in Bonak.νType.LeYoneda]
+le_induction' [definition, in Bonak.νType.LeYoneda]
+le_induction_step_computes [lemma, in Bonak.νType.LeYoneda]
+le_induction_base_computes [lemma, in Bonak.νType.LeYoneda]
+le_induction [lemma, in Bonak.νType.LeYoneda]
+

M

+map_subst_app [lemma, in Bonak.νType.RewLemmas]
+mkCohLayer [definition, in Bonak.νType.νType]
+mkCohPaintingHyp [definition, in Bonak.νType.νType]
+mkCohPainting_step [definition, in Bonak.νType.νType]
+mkCohPainting_base [definition, in Bonak.νType.νType]
+mkFrame [instance, in Bonak.νType.νType]
+mkFramePrev [definition, in Bonak.νType.νType]
+mkFrameSp [instance, in Bonak.νType.νType]
+mkFrame0 [instance, in Bonak.νType.νType]
+mkLayer [definition, in Bonak.νType.νType]
+mkPainting [instance, in Bonak.νType.νType]
+mkpainting [definition, in Bonak.νType.νType]
+mkPaintingPrev [instance, in Bonak.νType.νType]
+mkpainting_computes [lemma, in Bonak.νType.νType]
+mkprefix [definition, in Bonak.νType.νType]
+mkRestrLayer [definition, in Bonak.νType.νType]
+mkRestrPainting [definition, in Bonak.νType.νType]
+mkRestrPainting_step_computes [lemma, in Bonak.νType.νType]
+mkRestrPainting_base_computes [lemma, in Bonak.νType.νType]
+mkνTypeSn [instance, in Bonak.νType.νType]
+mkνType0 [instance, in Bonak.νType.νType]
+

N

+next [projection, in Bonak.νType.νType]
+Notation [library]
+

P

+Painting [projection, in Bonak.νType.νType]
+painting [projection, in Bonak.νType.νType]
+PaintingBlock [record, in Bonak.νType.νType]
+PaintingBlockPrev [record, in Bonak.νType.νType]
+PaintingPrev [projection, in Bonak.νType.νType]
+painting' [projection, in Bonak.νType.νType]
+painting'' [projection, in Bonak.νType.νType]
+prefix [projection, in Bonak.νType.νType]
+

R

+restrFrame [projection, in Bonak.νType.νType]
+restrFrame' [projection, in Bonak.νType.νType]
+RestrLayer [projection, in Bonak.νType.νType]
+restrPainting [projection, in Bonak.νType.νType]
+restrPainting' [projection, in Bonak.νType.νType]
+RewLemmas [library]
+rew_app [lemma, in Bonak.νType.RewLemmas]
+rew_swap [lemma, in Bonak.νType.RewLemmas]
+rew_permute' [lemma, in Bonak.νType.RewLemmas]
+rew_permute [lemma, in Bonak.νType.RewLemmas]
+rew_existT_curried [lemma, in Bonak.νType.RewLemmas]
+rew_sigT [lemma, in Bonak.νType.RewLemmas]
+rew_pair [lemma, in Bonak.νType.RewLemmas]
+rew_context [lemma, in Bonak.νType.RewLemmas]
+rew_rew' [lemma, in Bonak.νType.RewLemmas]
+rew_rew [lemma, in Bonak.νType.RewLemmas]
+

S

+SemiCubical [definition, in Bonak.νType.νType]
+SemiCubical2 [definition, in Bonak.νType.νType]
+SemiSimplicial [definition, in Bonak.νType.νType]
+SemiSimplicial2 [definition, in Bonak.νType.νType]
+SFalse [inductive, in Bonak.νType.LeYoneda]
+SFalse_sind [definition, in Bonak.νType.LeYoneda]
+SFalse_rec [definition, in Bonak.νType.LeYoneda]
+SFalse_ind [definition, in Bonak.νType.LeYoneda]
+SFalse_rect [definition, in Bonak.νType.LeYoneda]
+sI [constructor, in Bonak.νType.LeYoneda]
+sigT_UIP [lemma, in Bonak.νType.HSet]
+sigT_decompose [lemma, in Bonak.νType.HSet]
+sigT_decompose_eq [lemma, in Bonak.νType.HSet]
+sigT_eq [lemma, in Bonak.νType.HSet]
+STrue [inductive, in Bonak.νType.LeYoneda]
+STrue_sind [definition, in Bonak.νType.LeYoneda]
+

T

+this [projection, in Bonak.νType.νType]
+

U

+UIP [projection, in Bonak.νType.HSet]
+unit_UIP [lemma, in Bonak.νType.HSet]
+

other

+_ <= _ (nat_scope) [notation, in Bonak.νType.LeYoneda]
+_ <~ _ (nat_scope) [notation, in Bonak.νType.LeInductive]
+{ _ : _ && _ } (type_scope) [notation, in Bonak.νType.νType]
+_ =S _ (type_scope) [notation, in Bonak.νType.LeYoneda]
+hforall _ : _ , _ (type_scope) [notation, in Bonak.νType.HSet]
+hforall _ , _ (type_scope) [notation, in Bonak.νType.HSet]
+{ _ : _ & _ } (type_scope) [notation, in Bonak.νType.HSet]
+{ _ & _ } (type_scope) [notation, in Bonak.νType.HSet]
+_ ↕ _ [notation, in Bonak.νType.LeYoneda]
+_ ^ [notation, in Bonak.νType.Notation]
+_ • _ [notation, in Bonak.νType.Notation]
+_ .+3 [notation, in Bonak.νType.Notation]
+_ .+2 [notation, in Bonak.νType.Notation]
+_ .+1 [notation, in Bonak.νType.Notation]
+_ .2 [notation, in Bonak.νType.Notation]
+_ .1 [notation, in Bonak.νType.Notation]
+rew <- [ _ ] _ in _ [notation, in Bonak.νType.Notation]
+rew [ _ ] _ in _ [notation, in Bonak.νType.Notation]
+( _ ; _ ) [notation, in Bonak.νType.Notation]
+(= _ ; _ ) [notation, in Bonak.νType.Notation]
+[ _ ⇒ _ ] _ [notation, in Bonak.νType.Notation]
+↑ _ [notation, in Bonak.νType.LeYoneda]
+↓ _ [notation, in Bonak.νType.LeYoneda]
+⇑ _ [notation, in Bonak.νType.LeYoneda]
+⇓ _ [notation, in Bonak.νType.LeYoneda]
+♢ [notation, in Bonak.νType.LeYoneda]
+νType [record, in Bonak.νType.νType]
+νType [section, in Bonak.νType.νType]
+νType [library]
+νTypeAt [definition, in Bonak.νType.νType]
+νTypeFrom [record, in Bonak.νType.νType]
+νTypes [definition, in Bonak.νType.νType]
+νType.arity [variable, in Bonak.νType.νType]
+

+

Notation Index

+

other

+_ <= _ (nat_scope) [in Bonak.νType.LeYoneda]
+_ <~ _ (nat_scope) [in Bonak.νType.LeInductive]
+{ _ : _ && _ } (type_scope) [in Bonak.νType.νType]
+_ =S _ (type_scope) [in Bonak.νType.LeYoneda]
+hforall _ : _ , _ (type_scope) [in Bonak.νType.HSet]
+hforall _ , _ (type_scope) [in Bonak.νType.HSet]
+{ _ : _ & _ } (type_scope) [in Bonak.νType.HSet]
+{ _ & _ } (type_scope) [in Bonak.νType.HSet]
+_ ↕ _ [in Bonak.νType.LeYoneda]
+_ ^ [in Bonak.νType.Notation]
+_ • _ [in Bonak.νType.Notation]
+_ .+3 [in Bonak.νType.Notation]
+_ .+2 [in Bonak.νType.Notation]
+_ .+1 [in Bonak.νType.Notation]
+_ .2 [in Bonak.νType.Notation]
+_ .1 [in Bonak.νType.Notation]
+rew <- [ _ ] _ in _ [in Bonak.νType.Notation]
+rew [ _ ] _ in _ [in Bonak.νType.Notation]
+( _ ; _ ) [in Bonak.νType.Notation]
+(= _ ; _ ) [in Bonak.νType.Notation]
+[ _ ⇒ _ ] _ [in Bonak.νType.Notation]
+↑ _ [in Bonak.νType.LeYoneda]
+↓ _ [in Bonak.νType.LeYoneda]
+⇑ _ [in Bonak.νType.LeYoneda]
+⇓ _ [in Bonak.νType.LeYoneda]
+♢ [in Bonak.νType.LeYoneda]
+

+

Variable Index

+

other

+νType.arity [in Bonak.νType.νType]
+

+

Library Index

+

H

+HSet
+

L

+LeInductive
+LeYoneda
+

N

+Notation
+

R

+RewLemmas
+

other

+νType
+

+

Lemma Index

+

B

+bool_UIP [in Bonak.νType.HSet]
+

E

+eq_ind_r_refl [in Bonak.νType.RewLemmas]
+

H

+hpiT_decompose [in Bonak.νType.HSet]
+

L

+leI_down_morphism [in Bonak.νType.LeYoneda]
+leI_refl_morphism [in Bonak.νType.LeYoneda]
+leI_of_leY [in Bonak.νType.LeYoneda]
+leI_raise_both [in Bonak.νType.LeInductive]
+leI_lower_both [in Bonak.νType.LeInductive]
+leI_0 [in Bonak.νType.LeInductive]
+leI_up [in Bonak.νType.LeInductive]
+leR_raise_both [in Bonak.νType.LeYoneda]
+leR_lower_both [in Bonak.νType.LeYoneda]
+leR_down [in Bonak.νType.LeYoneda]
+leR_up [in Bonak.νType.LeYoneda]
+leR_0 [in Bonak.νType.LeYoneda]
+leR_contra [in Bonak.νType.LeYoneda]
+leR_refl [in Bonak.νType.LeYoneda]
+leYind_construct [in Bonak.νType.LeYoneda]
+leY_of_leI [in Bonak.νType.LeYoneda]
+leY_raise_both [in Bonak.νType.LeYoneda]
+leY_lower_both [in Bonak.νType.LeYoneda]
+leY_down [in Bonak.νType.LeYoneda]
+leY_up [in Bonak.νType.LeYoneda]
+leY_0 [in Bonak.νType.LeYoneda]
+leY_contra [in Bonak.νType.LeYoneda]
+leY_irrelevance [in Bonak.νType.LeYoneda]
+le_induction_step_computes [in Bonak.νType.LeYoneda]
+le_induction_base_computes [in Bonak.νType.LeYoneda]
+le_induction [in Bonak.νType.LeYoneda]
+

M

+map_subst_app [in Bonak.νType.RewLemmas]
+mkpainting_computes [in Bonak.νType.νType]
+mkRestrPainting_step_computes [in Bonak.νType.νType]
+mkRestrPainting_base_computes [in Bonak.νType.νType]
+

R

+rew_app [in Bonak.νType.RewLemmas]
+rew_swap [in Bonak.νType.RewLemmas]
+rew_permute' [in Bonak.νType.RewLemmas]
+rew_permute [in Bonak.νType.RewLemmas]
+rew_existT_curried [in Bonak.νType.RewLemmas]
+rew_sigT [in Bonak.νType.RewLemmas]
+rew_pair [in Bonak.νType.RewLemmas]
+rew_context [in Bonak.νType.RewLemmas]
+rew_rew' [in Bonak.νType.RewLemmas]
+rew_rew [in Bonak.νType.RewLemmas]
+

S

+sigT_UIP [in Bonak.νType.HSet]
+sigT_decompose [in Bonak.νType.HSet]
+sigT_decompose_eq [in Bonak.νType.HSet]
+sigT_eq [in Bonak.νType.HSet]
+

U

+unit_UIP [in Bonak.νType.HSet]
+

+

Constructor Index

+

E

+eqsprop_refl [in Bonak.νType.LeYoneda]
+

L

+leI_down [in Bonak.νType.LeInductive]
+leI_refl [in Bonak.νType.LeInductive]
+leYind_down [in Bonak.νType.LeYoneda]
+leYind_refl [in Bonak.νType.LeYoneda]
+

S

+sI [in Bonak.νType.LeYoneda]
+

+

Projection Index

+

C

+cohFrame [in Bonak.νType.νType]
+cohPainting [in Bonak.νType.νType]
+

D

+Dom [in Bonak.νType.HSet]
+

E

+eqFrameSp [in Bonak.νType.νType]
+eqFrameSp' [in Bonak.νType.νType]
+eqFrame0 [in Bonak.νType.νType]
+eqFrame0' [in Bonak.νType.νType]
+eqPaintingSp [in Bonak.νType.νType]
+eqPaintingSp' [in Bonak.νType.νType]
+eqRestrFrameSp [in Bonak.νType.νType]
+eqRestrFrame0 [in Bonak.νType.νType]
+eqRestrPaintingSp [in Bonak.νType.νType]
+eqRestrPainting0 [in Bonak.νType.νType]
+

F

+Frame [in Bonak.νType.νType]
+frame [in Bonak.νType.νType]
+FramePrev [in Bonak.νType.νType]
+frame' [in Bonak.νType.νType]
+frame'' [in Bonak.νType.νType]
+

L

+Layer [in Bonak.νType.νType]
+Layer' [in Bonak.νType.νType]
+

N

+next [in Bonak.νType.νType]
+

P

+Painting [in Bonak.νType.νType]
+painting [in Bonak.νType.νType]
+PaintingPrev [in Bonak.νType.νType]
+painting' [in Bonak.νType.νType]
+painting'' [in Bonak.νType.νType]
+prefix [in Bonak.νType.νType]
+

R

+restrFrame [in Bonak.νType.νType]
+restrFrame' [in Bonak.νType.νType]
+RestrLayer [in Bonak.νType.νType]
+restrPainting [in Bonak.νType.νType]
+restrPainting' [in Bonak.νType.νType]
+

T

+this [in Bonak.νType.νType]
+

U

+UIP [in Bonak.νType.HSet]
+

+

Inductive Index

+

E

+eqsprop [in Bonak.νType.LeYoneda]
+

L

+leI [in Bonak.νType.LeInductive]
+leYind [in Bonak.νType.LeYoneda]
+

S

+SFalse [in Bonak.νType.LeYoneda]
+STrue [in Bonak.νType.LeYoneda]
+

+

Instance Index

+

M

+mkFrame [in Bonak.νType.νType]
+mkFrameSp [in Bonak.νType.νType]
+mkFrame0 [in Bonak.νType.νType]
+mkPainting [in Bonak.νType.νType]
+mkPaintingPrev [in Bonak.νType.νType]
+mkνTypeSn [in Bonak.νType.νType]
+mkνType0 [in Bonak.νType.νType]
+

+

Section Index

+

other

+νType [in Bonak.νType.νType]
+

+

Definition Index

+

A

+AugmentedSemiSimplicial [in Bonak.νType.νType]
+

E

+eqsprop_sind [in Bonak.νType.LeYoneda]
+eqsprop_rec [in Bonak.νType.LeYoneda]
+eqsprop_ind [in Bonak.νType.LeYoneda]
+eqsprop_rect [in Bonak.νType.LeYoneda]
+

H

+hbool [in Bonak.νType.HSet]
+hpiT [in Bonak.νType.HSet]
+hpiT_UIP [in Bonak.νType.HSet]
+hsigT [in Bonak.νType.HSet]
+hunit [in Bonak.νType.HSet]
+

L

+leI_sind [in Bonak.νType.LeInductive]
+leI_rec [in Bonak.νType.LeInductive]
+leI_ind [in Bonak.νType.LeInductive]
+leI_rect [in Bonak.νType.LeInductive]
+leR [in Bonak.νType.LeYoneda]
+leY [in Bonak.νType.LeYoneda]
+leYind_sind [in Bonak.νType.LeYoneda]
+leYind_rec [in Bonak.νType.LeYoneda]
+leYind_ind [in Bonak.νType.LeYoneda]
+leYind_rect [in Bonak.νType.LeYoneda]
+leY_trans [in Bonak.νType.LeYoneda]
+leY_refl [in Bonak.νType.LeYoneda]
+le_induction'_step_computes [in Bonak.νType.LeYoneda]
+le_induction'_base_computes [in Bonak.νType.LeYoneda]
+le_induction'' [in Bonak.νType.LeYoneda]
+le_induction' [in Bonak.νType.LeYoneda]
+

M

+mkCohLayer [in Bonak.νType.νType]
+mkCohPaintingHyp [in Bonak.νType.νType]
+mkCohPainting_step [in Bonak.νType.νType]
+mkCohPainting_base [in Bonak.νType.νType]
+mkFramePrev [in Bonak.νType.νType]
+mkLayer [in Bonak.νType.νType]
+mkpainting [in Bonak.νType.νType]
+mkprefix [in Bonak.νType.νType]
+mkRestrLayer [in Bonak.νType.νType]
+mkRestrPainting [in Bonak.νType.νType]
+

S

+SemiCubical [in Bonak.νType.νType]
+SemiCubical2 [in Bonak.νType.νType]
+SemiSimplicial [in Bonak.νType.νType]
+SemiSimplicial2 [in Bonak.νType.νType]
+SFalse_sind [in Bonak.νType.LeYoneda]
+SFalse_rec [in Bonak.νType.LeYoneda]
+SFalse_ind [in Bonak.νType.LeYoneda]
+SFalse_rect [in Bonak.νType.LeYoneda]
+STrue_sind [in Bonak.νType.LeYoneda]
+

other

+νTypeAt [in Bonak.νType.νType]
+νTypes [in Bonak.νType.νType]
+

+

Record Index

+

F

+FrameBlock [in Bonak.νType.νType]
+FrameBlockPrev [in Bonak.νType.νType]
+

H

+HSet [in Bonak.νType.HSet]
+

P

+PaintingBlock [in Bonak.νType.νType]
+PaintingBlockPrev [in Bonak.νType.νType]
+

other

+νType [in Bonak.νType.νType]
+νTypeFrom [in Bonak.νType.νType]
+

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
Global IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(188 entries)
Notation IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(26 entries)
Variable IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(1 entry)
Library IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(6 entries)
Lemma IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(48 entries)
Constructor IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(6 entries)
Projection IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(34 entries)
Inductive IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(5 entries)
Instance IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(7 entries)
Section IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(1 entry)
Definition IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(47 entries)
Record IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(7 entries)
+
This page has been generated by coqdoc +
+ +
+ + + \ No newline at end of file