Re: [HoTT] Re: Bishop's work on type theory

[Michael Shulman <shu...@sandiego.edu>]

You mean something like "if t:A and A==B then t:B"?  You're right; I'm
not even sure how to phrase such a rule with Bishop's setup where
"the" type of a term is an *operation* T(t) == A, whereas things like
beta-reduction are expressed only propositionally in terms of Leibniz
equality.

On 5/9/18, Matt Oliveri <atm...@gmail.com> wrote:
> There doesn't seem to be anything like a conversion rule. I suspect that a
> lot of the math examples developed in the system don't actually type check.
>
> If they do, it would seem to be luck. Or maybe not; does anyone know some
> key intuition behind this system that I'm missing?
>
> On Friday, May 4, 2018 at 5:01:53 PM UTC-4, Martín Hötzel Escardó wrote:
>>
>> This week I learned two interesting things that seem to be kept as a
>> guarded secret:
>>
>> (1) Errett Bishop reinvented type theory.
>> (2) He also explained how to compile it to Algol.
>>
>> I am adding a link to these two manuscripts. A nice quote from the second
>>
>> paper (Algol.pdf) is this, in my opinion, because it foresees things such
>>
>> as Agda, Coq, NuPrl, ...
>>
>> "The possibility of such a compilation demonstrates the existence of a new
>>
>> type of programming language, one that contains theorems, proofs,
>> quantifications, and implications, in addition to the more conventional
>> facilities for specifying algorithms"
>>
>> This was in the late 1960's (or correct me). Here is a link to both
>> manuscripts: http://www.cs.bham.ac.uk/~mhe/Bishop/
>>
>> Greetings from Bonn.
>> Martin
>>
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>