David Corfield elements

The type of elements, Type^\widehat{Type}, is such that it contains as elements (A,a)(A, a) where AA is a type and a:Aa: A. Say we want to distinguish between a kind of activity and instances of that kind – running and occasions/instances of running.

Running: Activity, El(Running).

X:Achievement,x:Xt(x):Time,l(x):LocationX:Achievement, x: X \vdash t(x): Time, l(x): Location

u:Time,v:locationRain(u,v):Propu: Time, v: location \vdash Rain(u, v): Prop

x:Person,y:Objectxlity:Achievementx: Person, y: Object \vdash x\; lit\, y: Achievement

Johnlitacigarette:AchievementJohn\; lit\; a\; cigarette: Achievement

z:Johnlitacigarettet(z):Time;l(z):Locationz: John\; lit\; a\; cigarette \vdash t(z): Time; l(z): Location

z:JohnlitacigaretteRain(t(z),l(z))\prod_{z: John\; lit\; a\; cigarette} Rain(t(z), l(z))

Last revised on April 8, 2020 at 11:01:49. See the history of this page for a list of all contributions to it.