[Agda] list of types

Bas Spitters spitters at cs.ru.nl
Mon Apr 15 20:50:20 CEST 2013


On Mon, Apr 15, 2013 at 5:59 PM, Altenkirch Thorsten
<psztxa at exmail.nottingham.ac.uk> wrote:
> What I mean is the following: there is an equivalence between
>         A -> Set
> and
>         Sigma[ X : Set ] X -> A
>
> this is a trivial instance of the Grothendieck construction between
> families and fibrations.

I used UA to prove this, did you see a simpler construction?


More information about the Agda mailing list