The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

I meant wit only -> not unit!

 

From: <coq-club-request AT inria.fr> on behalf of Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Saturday, 5 October 2019 at 15:27
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] STLC versus CCC

 

Hi,

 

If you have products and unit type, you need to add extra eta rules: x = () for x:1 and x = (fst x,snd x) for x : AxB.

 

However, you can also use STLC with only unit to construct the initial CCC by using context concatenation for products. In this case the product laws follow from the properties of substitution.

 

Thorsten

 

From: <coq-club-request AT inria.fr> on behalf of Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Friday, 4 October 2019 at 17:02
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] STLC versus CCC

 

Hi all,

 

I am stuck in thinking about the correspondence between simply typed lambda calculus (STLC) and cartesian closed category (CCC) but I am confused at some point. Since it is well-known, I appreciate any reference that makes every detail explicit.

 

By STLC, let's agree that it is defined by a unit type *, products _x_, and simple function spaces _->_. Its terms are defined in the typical way. Consider terms in STLC equivalent up to beta-eta reduction. Thus STLC forms a category with types as objects and functions between types as morphisms, and axioms are checked.

 

Now it remains to show that such STLC with beta-eta equivalence is a CCC. Consider a proof showing the unit type * is a/the terminal object of the category. It is required to show that there is a unique morphism/function from any type to * up to beta-eta equivalence. Consider the following two functions from * to *:

 

\x : *. x

 

and

 

\x : *. {}

 

It is clear that both definitions have type * -> *, but how on earth these two types are beta-eta equivalent? From all of the literature I checked, there is no reduction rule associated with terms of type *, while to actually make this two functions equivalent by beta-eta reduction, it seems to suggest the following rule:

 

G |- t : * => t ~~> {}

 

That is to add a beta rule which imposes the reduction of any term of type * to the unit element {} in one step. However, this doesn't make sense to me.

 

An alternative way to think about it is to assume functional extensionality and say that these two functions are extensionally equal. This feels much better, but that simply means the equivalence of morphisms/functions in STLC is no longer beta-eta equivalence but beta-eta equivalence + functional extensionality. It is more confusing if we think about type checkers, as it is clear that in that context we only consider reductions. Does that mean we tend to be more permissive when we try to think in a more mathematical setting?

 

How does this work? Is there any reference about the full details of this correspondence or I am just thinking about something weird?

 

Thanks,

Jason Hu

https://hustmphrrr.github.io/

This message and any attachment are intended solely for the addressee

and may contain confidential information. If you have received this

message in error, please contact the sender and delete the email and

attachment. 

Any views or opinions expressed by the author of this email do not

necessarily reflect the views of the University of Nottingham. Email

communications with the University of Nottingham may be monitored 

where permitted by law.

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.