5
$\begingroup$

In the HOTT book, p. 433 (Appendix A.2.2), we have a congruence rule with the three following premises:

  1. $\Gamma \vdash A : \mathcal{U}_i$
  2. $\Gamma, x : A \vdash B : \mathcal{U}_i$
  3. $\Gamma, x : A \vdash b \equiv b' : B$

and the following conclusion: $\Gamma \vdash \lambda x. b \equiv \lambda x. b' : \prod_{(x : A)} B$. I am wondering why we have premises 1 and 2 while these premises are absent in the introduction rule of $\Pi$ (p. 434, Appendix A.2.4). I noticed that we have these premises in the formation rule of $\Pi$ (p. 434, Appendix A.2.4) to conclude that $\prod_{(x : A)} B$ has type $\mathcal{U}_i$ but, since they are absent from the introduction rule, I thought that in absence of premises 1 and 2, we would only have $\prod_{(x : A)} B : \mathcal{U}_k$ for some $k$, which would be enough to state the congruence rule in the same manner we are able to state the introduction rule. So, why do we need premises 1 and 2 for the congruence rule and not for the introduction rule?

Improve this question
$\endgroup$
10
  • $\begingroup$ The HoTT book is a bit informal (at least compared to some other type theory presentations). It isn’t designed to implement on a computer as written. I think (1) and (2) can be inferred from (3) and hence stated or not for sake of clarity/brevity. But whether stated or not, (1) and (2) hold if we have (3), otherwise (3) wouldn’t make sense. They even say something to this regard in the last paragraph of A.2.3. $\endgroup$
    – Jason Rute
    Commented Jan 24 at 2:46
  • $\begingroup$ In particular, I think specifically with the intro rule on p 434, $A$ and $B$ have to be the same as in the preceding formation rule since that is the only rule we have to formulate Pi types. I think the authors assumed this was clear from context. $\endgroup$
    – Jason Rute
    Commented Jan 24 at 3:16
  • 1
    $\begingroup$ Page references to HoTT book are not stable, please refer to the relevant section/example/proposition number. $\endgroup$
    – Andrej Bauer
    Commented Jan 24 at 7:20
  • 1
    $\begingroup$ @AndrejBauer Good point. :) I guess I was thinking more about how the user can see the generated code for defined definitions like Sigma, in say Lean, with #print Sigma and #print Sigma.rec. Then they can compare to the presentations in the HoTT book (and notice how Lean includes all the presuppositions like α : Type u). But I do see your point that this isn't really the same as the rules of the type theory, and they also can't see rules for built in types like Pi types and for definitional equality. $\endgroup$
    – Jason Rute
    Commented Jan 25 at 15:01
  • 1
    $\begingroup$ @AndrejBauer Nonetheless, dare accepted. :) MM0 is a meta proof assistant based on MetaMath, which can work with many foundations. lean.mm1 contains Lean's DTT foundations. The code is remarkably readable. The rules most closely related to the examples in this question are axioms ty_lambda, ty_Pi, and conv_lambda. I was surprised to see that the formal presentation in lean.mm1 omits the presuppositions. (Although, I guess there could be bugs since none of the very few examples use these 3 axioms.) $\endgroup$
    – Jason Rute
    Commented Jan 25 at 15:26

1 Answer 1

Reset to default
8
$\begingroup$

The premises 1. and 2. are called presuppositions (although the terminology is not fixed), as they are needed only to ensure that the judgements appearing in the rule are well-formed (more formally, the boundaries of the judgements are well-formed). Depending on how type theory is formulated, the presuppositions may be necessary, removable, or implicit in the way the rules are given. For background see rather lengthy and somewhat philosophical A general definition of dependent type theories, or the abridged technical version in Sections 2 and 3 of Finitary type theories with and without contexts (arXiv).

The HoTT book is informal by design. The formal presentations given in the appendices are likely a bit buggy in inessential ways (many if not most such presentations printed on paper are). For example, the congruence rule you cite arguably requires two additional presuppositions, namely $\Gamma, x {:} A \vdash b : B$ and $\Gamma, x {:} A \vdash b' : B$.

I would recommend not worrying too much about extraneous or missing presuppositions. In the worst case they can always be thrown in, but they detract from the content of the rules.

Improve this answer
$\endgroup$
6
  • $\begingroup$ I did not read yet the references given in the answer, I will. For now, I don't see why presuppositions should be necessary, because, for example, I don't see how to have a derivation of the premise 3. without having $\Gamma, x : A \vdash b : B$ (but, probably, because I have in mind one specific way how type theory is formulated). "many if not most such presentations printed on paper are": this is surprising to me but is consistent with Jason Rute's comment. $\endgroup$
    – Bruno
    Commented Jan 25 at 0:47
  • 1
    $\begingroup$ To see how presuppositivity can fail, suppose we postulate the reflexivity rule just as $\Gamma \vdash t \equiv t : A$ (no premises). Then I can use this rule directly to derive $\vdash 7 \equiv 7 : \mathsf{Bool}$. $\endgroup$
    – Andrej Bauer
    Commented Jan 25 at 8:01
  • $\begingroup$ If we had such a reflexivity rule, adding a presuppositive premise in the congruence rule for $\lambda$ would not prevent the use of this reflexivity rule to derive $\vdash 7 \equiv 7 : Bool$. If we consider this judgment as undesirable then we have to add some premise in the reflexivity rule and then the presuppositive premise becomes unnecessary in the congruence rule. If we accept such a judgment (?!), then I don't see why we should add this presuppositive premise in the congruence rule. $\endgroup$
    – Bruno
    Commented Jan 25 at 13:46
  • $\begingroup$ I do not understand why you're mixing together the reflexivity rule and the congruence rule. I showed the reflexivity rule in the above comment as (an independent) example of how one needs to worry about presuppositivy. And in general, whether or not a type theory is presuppositive depends on the entire type theory, as one has to carry out an induction on all possible derivations. That is, yes there will be interactions between rules. $\endgroup$
    – Andrej Bauer
    Commented Jan 25 at 20:45
  • $\begingroup$ I misunderstood your comment "to see how presuppositivity can fail": I thought you were referring to premises 1 and 2 of the cong. rule since you were replying to my comment "I don't see why presuppositions should be necessary". The refl. rule without any premise doesn't make much sense to me. It seems that you consider the premise $\Gamma \vdash a : A$ of the refl. rule as having the same status ("presuppositive") as the premises 1 and 2 of the congruence rule (I missed it because I see the premise of the refl. rule as necessary in contrast with premises 1 and 2 of the cong. rule). $\endgroup$
    – Bruno
    Commented Jan 25 at 22:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.