<p>Consider the following <em>div</em> function written in Coq. It takes in a proof that the divider is non-zero.</p>

<pre><code>Definition div (n d:nat) (pf: ~(d = 0)) := n/d.
</code></pre>

<p>Focus on <code>~(d = 0)</code>: Is this a term or a type? My understanding is that this is a term of type <code>Prop</code>. <code>Check</code> gives the same.</p>

<pre><code>Check (forall d:nat, ~(d = 0))
  forall d : nat, d &lt;&gt; 0 : Prop
</code></pre>

<p>So, is <code>pf</code> a member of the term <code>~(d = 0)</code>? This is confusing. Should I now think of <code>~(d = 0)</code> as a type? Note that I am familiar with dependent types (though not expert) and am being pedantic here. </p>

<p>A term by itself cannot be a type unless <code>pf : ~(d = 0)</code> is a syntactic sugar for something along the lines of <code>pf: Proof ~(d = 0)</code> where <code>Proof</code> is a type of kind <span class="math-container">$\Pi x:Prop. \star$</span>. That is, it takes a prop term and returns a new type. </p>

<p>What is going on here? I think I am missing the calculus part here.</p>

CC BY-SA 4.0
2019-12-02T18:46:18.387Z
`Prop` is a *universe*, i.e., a type whose terms are types, a bit like `Type`, which is also a universe whose terms are types. Also, this question belongs on cs.stackexchange.com because it's not research-level.
Andrej Bauer
CC BY-SA 4.0
2019-12-02T19:24:35.103Z
@AndrejBauer As commented in my other post, coq.inria.fr/community says to post questions in TCS stackexchange. Hence I took it to here since this is about the theory of Coq (The calculus discussed there is of Calculus of Constructions). If appropriate, I have no issues moving the question to cs.stackexchange.com but I want to make sure that I understand the etiquette before doing so.
Ram
CC BY-SA 4.0
2019-12-02T21:00:44.653Z
This forum has a voting system. If I am the only one who votes to close, then the community thinks it is ok to post here. If your question gets closed, then the community thinks you should ask elsewhere. In my opinion your question is very basic, i.e., you're trying to make out what is what in Calculus of Constructions. That's not research-level.
Andrej Bauer
CC BY-SA 4.0
2019-12-02T22:23:43.800Z
@AndrejBauer, fair enough. Do I have to delete the question and repost it in cs forum? or is there a better way.

Also, thanks for your comment on the universe. I am a digging a bit more into that. But all I find is http://adam.chlipala.net/cpdt/html/Universes.html. It is not clear to me if this issue is related to the impredicativity of Prop. If you can either elaborate or point to a reference, that will help me.
Ram
CC BY-SA 4.0
2019-12-02T22:51:49.847Z
I'd wait a bit to see if there's going to be an answer or more votes to close. Although, on cs.stackexchange.com I would answer, rather than just post a short comment. (And doesn't the comment answer your question? Do you know about universes in type theory?)
Andrej Bauer
CC BY-SA 4.0
2019-12-03T15:55:45.843Z
@AndrejBauer I have some intuition on universes and type hierarchy. However, I would like to use some (hopefully canonical) reference on this w.r.t Coq Props settling it once for all.
Ram
CC BY-SA 4.0
2019-12-03T21:58:52.597Z
I can recommend [this introduction to CIC](https://hal.inria.fr/hal-01094195/document). Note that there "universes" are called "sorts".
Andrej Bauer
<pl.programming-languages><type-theory><dependent-type><coq><calculus-of-constructions>
Proposition terms vs types in Coq
Ram
# Proposition terms vs types in Coq

(Asked by: username_0 on 2019-12-02)

Consider the following div function written in Coq. It takes in a proof that the divider is non-zero.
Definition div (n d:nat) (pf: ~(d = 0)) := n/d.

Focus on ~(d = 0): Is this a term or a type? My understanding is that this is a term of type Prop. Check gives the same.
Check (forall d:nat, ~(d = 0))
  forall d : nat, d <> 0 : Prop

So, is pf a member of the term ~(d = 0)? This is confusing. Should I now think of ~(d = 0) as a type? Note that I am familiar with dependent types (though not expert) and am being pedantic here. 
A term by itself cannot be a type unless pf : ~(d = 0) is a syntactic sugar for something along the lines of pf: Proof ~(d = 0) where Proof is a type of kind $\Pi x:Prop. \star$. That is, it takes a prop term and returns a new type. 
What is going on here? I think I am missing the calculus part here.

**Tags:** pl.programming-languages, type-theory, dependent-type, coq, calculus-of-constructions
> **Comments:**
> **username_1**: `Prop` is a *universe*, i.e., a type whose terms are types, a bit like `Type`, which is also a universe whose terms are types. Also, this question belongs on cs.stackexchange.com because it's not research-level.  
> **username_0**: @AndrejBauer As commented in my other post, coq.inria.fr/community says to post questions in TCS stackexchange. Hence I took it to here since this is about the theory of Coq (The calculus discussed there is of Calculus of Constructions). If appropriate, I have no issues moving the question to cs.stackexchange.com but I want to make sure that I understand the etiquette before doing so.  
> **username_1**: This forum has a voting system. If I am the only one who votes to close, then the community thinks it is ok to post here. If your question gets closed, then the community thinks you should ask elsewhere. In my opinion your question is very basic, i.e., you're trying to make out what is what in Calculus of Constructions. That's not research-level.  
> **username_0**: @AndrejBauer, fair enough. Do I have to delete the question and repost it in cs forum? or is there a better way.  Also, thanks for your comment on the universe. I am a digging a bit more into that. But all I find is http://adam.chlipala.net/cpdt/html/Universes.html. It is not clear to me if this issue is related to the impredicativity of Prop. If you can either elaborate or point to a reference, that will help me.  
> **username_1**: I'd wait a bit to see if there's going to be an answer or more votes to close. Although, on cs.stackexchange.com I would answer, rather than just post a short comment. (And doesn't the comment answer your question? Do you know about universes in type theory?)  
> **username_0**: @AndrejBauer I have some intuition on universes and type hierarchy. However, I would like to use some (hopefully canonical) reference on this w.r.t Coq Props settling it once for all.  
> **username_1**: I can recommend [this introduction to CIC](https://hal.inria.fr/hal-01094195/document). Note that there "universes" are called "sorts".  

---

## 0 answers

