[Agda] general question

[Martin Escardo]

Thanks for the clarifications, everybody.

What I was really after was bounded universal quantification
forall n < m -> A n. I tried several things, all of which work, some of 
which gave me a lot of headaches (like using the data type Fin of finite 
sets). The best, headache free, definition I have so far is

  syntax bounded-∀ (λ n → a) m = ∀⟨ n < m ⟩→ a

  data bounded-∀ (A : ℕ → Set) : ℕ → Set where
    bounded-∀-intro₀ :
      ∀⟨ O < O ⟩→ A O

    bounded-∀-intro₁ :
     {m : ℕ} → A m → (∀⟨ n < m ⟩→ A n) → ∀⟨ n < succ m ⟩→ A n

I used (dependent) vectors terminology/notation in the original message 
because perhaps they look more familiar (but of course they amount to 
the same thing). Now you see why I wanted to flip A and m.

I'd appreciate further ideas you may have had regarding the definition 
of bounded universal quantification in Agda.

Martin


On 03/05/11 12:23, Peter Dybjer wrote:
> Yes, let me just confirm Ondrej's answer Martin's question. The distinction between parameters and indices go back to my old papers on schemata for inductive families (and to an analogous distinction in CIC). See
>
> @article{dybjer:facs,
> author  = "Peter Dybjer",
> title   = "Inductive Families",
> journal = "Formal Aspects of Computing",
> volume  = 6,
> pages   = "440-465",
> year    = 1994}
>
> @incollection{DybjerP:indsfm,
> author  = "Peter Dybjer",
> booktitle = "Logical Frameworks",
> title   = "Inductive sets and families in {Martin-L{\"o}f's} Type Theory
>         and their set-theoretic semantics",
> year    = 1991,
> publisher = "Cambridge University Press",
> editor  = "Gerard Huet and Gordon Plotkin",
> pages   = "280-306"}
>
> The set-theoretic semantics in the latter paper makes use this distinction. Agda does not implement exactly these schemata, but something more general.
>
> Peter
>
> ________________________________________
> From: agda-bounces at lists.chalmers.se [agda-bounces at lists.chalmers.se] On Behalf Of Ondrej Rypacek [ondrej.rypacek at gmail.com]
> Sent: Tuesday, May 03, 2011 1:13 PM
> To: Martin Escardo; Agda mailing list
> Cc: Dominique Devriese
> Subject: Re: [Agda] general question
>
> Hi Martin,
>
> I think the difference is semantical rather then just syntactical.
> Although it is true that
>
> Vec : (A : ℕ → Set) →  ℕ → Set
>
> is the type of  matrices of Sets, indexed by (ℕ → Set) x ℕ, the definition
>
> data Vec (A : ℕ → Set) : ℕ → Set where
>   [] : Vec A O
>   _::_ : {n : ℕ} → A n → Vec A n → Vec A (succ n)
>
>
> defines one column in it for each A fixed throughout the definition.
> data Vec (n : ℕ) :  (ℕ → Set) → Set where
> ...
>
> would define one line, for each n: N and (ℕ → Set) variable. None of
> these alone define the whole matrix, thus you cannot flip at will and
> turn a parameter into a index. You'd need to define
>
> data Vec : (A : ℕ → Set) →  ℕ → Set where
> ....
>
>
> or an A ->  Nat indexed collection of the former, or an Nat indexed
> collection of the latter to make the situation symmetrical.
>
>
> Hope this helps.
> Best,
> Ondrej
>
>
> On 3 May 2011 11:58, Dominique Devriese
> <dominique.devriese at cs.kuleuven.be>  wrote:
>> Martin,
>>
>> 2011/5/3 Martin Escardo<m.escardo at cs.bham.ac.uk>:
>>> Dominuqe, thanks. Yes, I can do this.
>>>
>>> But what is, in the syntax of the data declaration, forcing me to have A
>>> first? And why?
>>
>> I guess this is related to the distinction between data type indices
>> and parameters in Agda data definitions. I don't immediately find a
>> good reference, but other people on this list will be able to explain
>> this, I think.
>>
>> Dominique
>> _______________________________________________
>> 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