Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?

["Licata, Dan" <dlicata@wesleyan.edu>]

For inductive families, one thing you can do is to think of them in terms of the translation to parametrized inductive types and identity types, so

>    data Foo (A : Set) : Set where
>      bar : Id U A UnaryNat -> Foo A 

in which case bar applied to the Id U BinaryNat UnaryNat that you get from univalence gives a Foo BinaryNat.

A related perspective is to think of some transports as additional constructors for inductive families; see e.g. this approach to inductive families in cubical type theory https://www.cs.cmu.edu/~ecavallo/works/popl19.pdf

-Dan

> On Nov 5, 2019, at 7:06 PM, Stefan Monnier <monnier@iro.umontreal.ca> wrote:
> 
>> members of this list. The constructivity of univalence was an open problem 
>> for a number of year, and I would say that, even if it is solved via the 
>> cubical model, it is far from being fully understood.
> 
> In my case, I still find it odd in a situation such as:
> 
>    data Foo : Set -> Set where
>      bar : Foo UnaryNat
> 
> since transport supposedly allows us to take a proof of equivalence
> between UnaryNat and BinaryNat and turn a `bar` into something of type
> `Foo BinaryNat` although I can't see any way to directly construct an
> object of this type.
> 
> 
>        Stefan
> 

-- 
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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/0CC0B8D7-3D66-42AD-A2D7-3B897A432B36%40wesleyan.edu.