[Agda] list of types

[Altenkirch Thorsten]

Thank you, Twan.

Actually "All" is the "vertical" List functor.

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.

(by equivalence I mean an isomorphism upto isomorphism).

Hence given a P : A -> Set, we obtain (X , f) : Sigma[ X : Set ] X -> A
and applying List/map we get (List X, map f) : Sigma[ X : Set ] List X ->
List A
and now going back along the equivalence we get List A -> Set which is
equivalent to All P.

One useful consequence of this observation is that it gives you a way to
do All for any functor.
Given P : A -> Set we obtain All_F : F A -> Set. Would it make sense to
implement the generic version
in the library?

Thorsten


On 15/04/2013 11:50, "Twan van Laarhoven" <twanvl at gmail.com> wrote:

>There is a type for this in the standard library, under Data.List.All:
>
>     open import Data.List.All
>     EachPositive : List ℕ → Set
>     EachPositive xs = All (\n → n > 0) xs
>
>It has the constructors [] and _∷_ that you would expect.
>
>
>Twan
>
>On 15/04/13 16:58, Altenkirch Thorsten wrote:
>> Actually, I think the type you have in mind is
>>
>> data EachPositive (xs : List Nat) : Set where
>> 	[] : EachPositive []
>> 	_::_ : forall {n} (n > 0) -> (EachPositive xs) -> EachPositive (n ::
>>xs)
>>
>> which isn't the same same as "map (\ n -> n > 0) xs" which is just a
>>list
>> of types.
>>
>> Another way would be to (fold \times \top) on this list to get a type
>> (replacing nil by \top and :: by \times. But I think the dependent type
>> given above is preferable.
>>
>> Thorsten
>>
>> P.S. Some errors corrected. Apologies fro filling up people's mailboxes.
>>
>>
>>
>> On 15/04/2013 10:24, "Altenkirch Thorsten"
>> <psztxa at exmail.nottingham.ac.uk> wrote:
>>
>>> Indeed, what would be an element of "EachPositive xs"?
>>>
>>> On 15/04/2013 06:17, "Andreas Abel" <andreas.abel at ifi.lmu.de> wrote:
>>>
>>>> On 15.04.2013 11:44, Serge D. Mechveliani wrote:
>>>>> Andreas Abel responded recently
>>>>>
>>>>>> A list of types is not a type.
>>>>>
>>>>> But why
>>>>>          EachPositive : List Nat -> List (Set _)
>>>>>          EachPositive xs =  map (\ n -> n > 0) xs
>>>>>
>>>>> is type-checked?
>>>>
>>>> This is fine, "List Set" is a type, but "EachPositive xs" is a list,
>>>>and
>>>> cannot be used as a type, as in,
>>>>
>>>>    -> EachPositive xs -> ...
>>>>
>>>>
>>>>
>>>>
>>>> --
>>>> Andreas Abel  <><      Du bist der geliebte Mensch.
>>>>
>>>> Theoretical Computer Science, University of Munich
>>>> Oettingenstr. 67, D-80538 Munich, GERMANY
>>>>
>>>> andreas.abel at ifi.lmu.de
>>>> http://www2.tcs.ifi.lmu.de/~abel/
>>>> _______________________________________________
>>>> Agda mailing list
>>>> Agda at lists.chalmers.se
>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>> 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 send it back to me, and immediately delete it.
>>>Please
>>> do not use, copy or disclose the information contained in this message
>>>or
>>> in any attachment.  Any views or opinions expressed by the author of
>>>this
>>> email do not necessarily reflect the views of the University of
>>> Nottingham.
>>>
>>> This message has been checked for viruses but the contents of an
>>> attachment
>>> may still contain software viruses which could damage your computer
>>> system:
>>> you are advised to perform your own checks. Email communications with
>>>the
>>> University of Nottingham may be monitored as permitted by UK
>>>legislation.
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>> 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 send it back to me, and immediately delete it.
>> Please do not use, copy or disclose the information contained in this
>>message or in any attachment.  Any views or opinions expressed by the
>>author of this email do not necessarily reflect the views of the
>>University of Nottingham.
>>
>> This message has been checked for viruses but the contents of an
>>attachment
>> may still contain software viruses which could damage your computer
>>system:
>> you are advised to perform your own checks. Email communications with
>>the
>> University of Nottingham may be monitored as permitted by UK
>>legislation.
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
>_______________________________________________
>Agda mailing list
>Agda at lists.chalmers.se
>https://lists.chalmers.se/mailman/listinfo/agda