Thanks for the links. Looking at

constructing terms then prove some of them are well-typed.

except for dependent type itself(i.e. the strongest calculus of the cube).

type, I'm expecting anything that is at least as strong as λP.

You can represent the syntax of pretty much every dependent and

impredicative theory in Agda. However, that does not settle whether a

particular proof or construction using a syntax is a) possible in base Agda

b) feasible or convenient in base Agda.

System F and F-omega syntax is easy to represent in Agda, in either

intrinsic or extrinsic manner. Showing consistency or normalization would

require an impredicative universe in Agda, so that's not possible without

postulating stuff, but even without that there are many interesting things

which you could do with the syntax.

Predicative dependent type theories can be represented and proven

consistent; this is <http://www.cse.chalmers.se/~abela/popl18.pdf> the most

advanced development I know of which only uses native Agda features (in

this case, induction-recursion). Note though that formal handling of

dependent types tends to be highly technically challenging.

For dependent type itself, I do not think it's possible, due to Goedel's

Gödel doesn't enter the picture in any of the developments I know of,

because the metatheories are stronger than object theories, due to having

inductive families and/or induction/recursion. Also, Gödel would only

prevent consistency proofs, but doesn't preclude representing the syntax or

doing a number of interesting things with it which don't imply consistency.

is Prop type in Coq is impredicative, and therefore the calculus underneath

*Post by Jason -Zhong Sheng- Hu*(caculus of inductive constructions, CIC) is stronger than calculus of

constructions(CoC)

CoC has impredicative base Set.

*Post by Jason -Zhong Sheng- Hu*my intuition was there is nothing special about system F, and all terms

and types should be just able to fit into Set along. and indeed, someone

has done the work: https://github.com/sstucki/system-f-agda

regarding stronger calculus, i do not see why they are not possible,

except for dependent type itself(i.e. the strongest calculus of the cube).

https://github.com/plclub/metalib/tree/master/Fsub

The modelling calculus of Scala, (dependent object types, DOT), for

example, has type dependent types, type dependent values, and a weak form

of value dependent types, which can also be proved with terms and types in

Set: https://github.com/samuelgruetter/dot-calculus ht

tps://github.com/amaurremi/dot-calculus

Though in Coq, the terms and types are defined in Set, which roughly

corresponds to Set in Agda, and that hopefully means you won't need to go

above Set 2 to prove it's sound.

For dependent type itself, I do not think it's possible, due to Goedel's

incompleteness theorem. However, someone did it in Coq (which i've not

checked, but, well, it's there) https://github.com/coq-contribs/coq-in-coq .

The reason why it might be doable in Coq, is Prop type in Coq is

impredicative, and therefore the calculus underneath (caculus of inductive

constructions, CIC) is stronger than calculus of constructions(CoC).

Indeed, the author represents typ to be Prop because he had no choice.

https://github.com/coq-contribs/coq-in-coq/blob/master/Types.v

Hope that helps.

*Sincerely Yours, *

* Jason Hu*

------------------------------

*Sent:* April 4, 2018 10:36:21 PM

*Subject:* [Agda] Encoding higher lambda calculus in agda

Hi,

There are numerous implementations of untyped lambda calculus and

simply typed lambda calculus in Agda online. However, I can't find any

mention of encoding of other "higher" lambda calculus in the lambda

cube like λ2 or λP in Agda. Is it because they are inherently

impredicative and can't be represented in Agda?

Thanks,

Si Yu

_______________________________________________

Agda mailing list

https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________

Agda mailing list

https://lists.chalmers.se/mailman/listinfo/agda