Thank you for your work! I finally proved this simple sentence

[refparo]

Commit: 77e6676

I'm teaching myself formal semantics and trying to reimplement it in modern type theories.

This model used Neo-Davidsonian event semantics, although event semantics won't be of much use until I move on to more complex sentences. The sentence is “John runs”. As a by-product, I also proved “It rains”.

-- *** Prelude

prim I
prim left
prim right
prim arcoe
struct Path (A : I -> Type) (a : A left) (b : A right) : Type
 | at (i : I) : A i {
   | left => a
   | right => b
 }
def path {A : I -> Type} (p : Pi (i : I) -> A i)
  => new Path A (p left) (p right) { | at i => p i }
def `=` Eq {A : Type} (a b : A) : Type => Path (\ i => A) a b
def idp {A : Type} (a : A) : a = a => path (\ i => a)
def coe {a b : Type} (eq : a = b) (x : a) (i : I) : eq.at i
  => arcoe eq.at x i

bind = looser application


def the (A : Type) (x : A) : A => x


open data Unit : Type 0 | unit


-- *** Types

struct EventT : Type 1
  | agentT : Type 0

def getAgentT (t : EventT) : Type 0 => t.agentT
def setAgentT (x : Type 0) (t : EventT) : EventT
  => new EventT { | agentT => x }
def agentT-inv (t : EventT) (u : Type 0) : u = getAgentT (setAgentT u t)
  => idp u


struct Event (t : EventT) : Type 2
  | agent : t.agentT

def getAgent (t : EventT) (e : Event t) : t.agentT => e.agent


def Quantifier (t : Type 3) : Type 4 => (t -> Type 3) -> Type 3

def mkConstQ {t : Type 3} (x : t) : Quantifier t
  => \f => f x


def Verb (t : EventT) : Type 4 => Quantifier (Event t)

def mkVerb {t : EventT} (p : Event t -> Type 3) : Verb t
  => \f => Sig (e : Event t) ** (Sig (p e) ** (f e))


def Theta (setT : Type 0 -> EventT -> EventT) : Type 4
  => Pi {u : Type 0} {t : EventT}
  -> ((u -> Type 3) -> Type 3)
  -> ((Event (setT u t) -> Type 3) -> Type 3)
  -> (Event (setT u t) -> Type 3) -> Type 3

def mkTheta
  (getT : EventT -> Type 0)
  (get : Pi (t : EventT) -> Event t -> getT t)
  (setT : Type 0 -> EventT -> EventT)
  (invariant : Pi (t : EventT) (u : Type 0) -> u = getT (setT u t))
  : Theta setT
  => \{u} {t} => \q p => \f =>
    q (\x => p (\e => Sig (get (setT u t) e = coe (invariant t u) x right) ** (f e)))

def agent : Theta setAgentT
  => \{u} {t} => mkTheta getAgentT getAgent setAgentT agentT-inv {u} {t}


def Sentence : Type 4 => Type 3

def mkSentence {t : EventT} (p : Quantifier (Event t)) : Type 3
  => p (\x => Unit)


-- *** World

open data Entity : Type
  | johnImpl

def john : Quantifier Entity
  => mkConstQ johnImpl


open data RainImpl : Type
  | rain1

def Rain (e : Event (new EventT { | agentT => Unit })) : Type
  => RainImpl

def rain : Verb (new EventT { | agentT => Unit })
  => mkVerb {new EventT { | agentT => Unit }} Rain


open data RunImpl (ag : Entity) : Type
  | johnImpl => run1

def Run (e : Event (new EventT { | agentT => Entity })) : Type
  => RunImpl e.agent

def run : Verb (new EventT { | agentT => Entity })
  => mkVerb {new EventT { | agentT => Entity }} Run


-- *** Sentences & Proofs

def rains : Sentence =>
  mkSentence {new EventT { | agentT => Unit }} rain

def proof-rains-event : Event (new EventT { | agentT => Unit })
  => new Event (new EventT { | agentT => Unit }) { | agent => unit }

def proof-rains : rains
  => (proof-rains-event, (rain1, unit))

def john-runs : Sentence =>
  mkSentence {new EventT { | agentT => Entity }}
    (agent {Entity} {new EventT { | agentT => Unit }} john run)

def proof-john-runs-event : Event (new EventT { | agentT => Entity })
  => new Event (new EventT { | agentT => Entity }) { | agent => johnImpl }

def proof-john-runs : john-runs
  => (proof-john-runs-event, (run1, (idp johnImpl, unit)))

[ice1000]

tql

[ice1000]

Somehow I think I should implement explicit level parameters, but I'm unsure about this. Agda did it because the level system in Agda is noisy (but looks quite solid). Maybe Aya has a better way around

[refparo]

An updated version with universe polymorphism and implicit arguments omitted as much as possible:

(assuming that base/src/test/resources/success/common is added as a dependency)

Model.aya:

public open import Paths

public open data Unit | unit
def coe {a b : Type} (eq : a = b) (x : a) (i : I) : eq.at i
  => arcoe eq.at x i
def idpath {A : Type} (a : A) : a = a => idp {A} {a}

-- *** Types

universe u

struct EventT : Type (lsuc u)
  | AgentT : Type u => Unit

def getAgentT (T : EventT) : Type u => T.AgentT
def setAgentT (A : Type u) (T : EventT) : EventT
  => new EventT { | AgentT => A }
def AgentT-inv (A : Type u) (T : EventT) : A = getAgentT (setAgentT A T)
  => idpath A


struct Event (T : EventT {universe u}) : Type (lsuc u)
  | agent : T.AgentT

def getAgent (T : EventT) (e : Event T) : T.AgentT => e.agent


universe v

def Quantifier (A : Type u) : Type (lmax u (lsuc v)) => (A -> Type v) -> Type v

def mkConstQ {A : Type u} (x : A) : Quantifier A
  => \f => f x


def Verb (T : EventT {universe u}) : Type (lmax (lsuc u) (lsuc v))
  => Quantifier (Event T) {universe (lsuc u), v}

def mkVerb {T : EventT} (p : Event T -> Type) : Verb T
  => \f => Sig (e : Event T) ** (Sig (p e) ** (f e))

def VP (T : EventT {universe u}) : Type (lmax (lsuc u) (lsuc v))
  => Quantifier (Event T) {universe (lsuc u), v}


def BNP (A : Type u) : Type (lmax u (lsuc v)) => Quantifier A {universe u, v}

def GNP (setT : Type u -> EventT -> EventT) (A : Type u)
  : Type (lmax (lsuc u) (lsuc v))
  => Pi {T : EventT} -> VP (setT A T) -> VP (setT A T)

def NP (A : Type u) : Type (lmax (lsuc u) (lsuc v))
  => GNP setAgentT A {universe u, v}


def Theta (setT : Type u -> EventT -> EventT) : Type (lmax (lsuc u) (lsuc v))
  => Pi {A : Type u}
  -> BNP A {universe u, v}
  -> GNP setT A {universe u, v}

def mkTheta
  (getT : EventT -> Type u)
  (get : Pi (T : EventT) -> Event T -> getT T)
  (setT : Type u -> EventT -> EventT)
  (T-inv : Pi (A : Type u) (T : EventT) -> A = getT (setT A T))
  : Theta setT
  => \{A} => \q => \{T} => \p => \f => q (\x => p (\e =>
    Sig (get (setT A T) e = coe (T-inv A T) x right) ** (f e)))

def agent : Theta setAgentT
  => \{A} => mkTheta getAgentT getAgent setAgentT AgentT-inv {A}


def mkConstNP {A : Type u} (x : A) : NP A
  => \{T} p => \f => p (\e => Sig (e.agent = x) ** (f e))


def Sentence : Type (lsuc u) => Type u

def mkSentence {T : EventT} (p : Quantifier (Event T)) : Sentence
  => p (\x => Unit)

Test.aya:

open import Model

-- *** World

open data Entity : Type
  | johnImpl

def john : Quantifier Entity
  => mkConstQ johnImpl


open data RainImpl : Type
  | rain1

def Rain (e : Event (new EventT {})) : Type
  => RainImpl

def rain : Verb (new EventT {})
  => mkVerb {new EventT {}} Rain


open data RunImpl (ag : Entity) : Type
  | johnImpl => run1

def Run (e : Event (new EventT { | AgentT => Entity })) : Type
  => RunImpl e.agent

def run : Verb (new EventT { | AgentT => Entity })
  => mkVerb {new EventT { | AgentT => Entity }} Run


-- *** Sentence & Proof

def rains : Sentence =>
  mkSentence rain

def proof-rains-event : Event (new EventT {})
  => new Event (new EventT {}) { | agent => unit }

def proof-rains : rains
  => (proof-rains-event, (rain1, unit))

def john-runs : Sentence =>
  mkSentence (agent john {new EventT {}} run)

def proof-john-runs-event : Event (new EventT { | AgentT => Entity })
  => new Event (new EventT { | AgentT => Entity }) { | agent => johnImpl }

def proof-john-runs : john-runs
  => (proof-john-runs-event, (run1, (idpath johnImpl, unit)))

[ice1000]

Where did the error go?

[ice1000]

I mean #57

[refparo]

@ice1000 It seems the code in #57 lacks some explicit universe levels…

[ice1000]

@ice1000 It seems the code in #57 lacks some explicit universe levels…

Nah. Surely the solver is buggy. It's on me, don't worry.

[ice1000]

bors r+

[refparo]

@ice1000 Updated version with compressed universe levels:

open import Paths

public open data Unit | unit

def coe {a b : Type} (eq : a ↑ = b) (x : a) : b
  => ↑ arcoe eq.at x right


-- *** Types

public open struct EventT : Type 1
  | AgentT : Type 0 => Unit

def GetterT => EventT -> Type 0
def SetterT => Type 0 -> EventT -> EventT
def Invariant (GetT : GetterT) (SetT : SetterT)
  => Pi (T : EventT) (E : Type 0) -> E ↑ = GetT (SetT E T)

-- wish these getter/setters could be generated automatically
def GetAgentT (T : EventT) => T.AgentT
def SetAgentT (E : Type 0) (T : EventT) : EventT
  => new EventT { | AgentT => E }
def AgentT-inv : Invariant GetAgentT SetAgentT
  => \T E => ↑ idp

public open struct Event (T : EventT) : Type 0
  | agent : T.AgentT

def Getter (GetT : GetterT) => Pi {T : EventT} (Event T) -> GetT T

def getAgent {T : EventT} (e : Event T) : T.AgentT => e.agent


def Quantifier (E : Type 0) : Type 1
  => (E -> Type 0) -> Type 0

def mkConstQ {E : Type 0} (x : E) : (E -> Type 0) -> Type 0
  => \f => f x


-- verbs are event quantifiers
def Verb (T : EventT) : Type 1
  => (Event T -> Type 0) -> Type 0

def mkVerb {T : EventT} (p : Event T -> Type 0) : Verb T
  => \f => Sig (e : Event T) (p e) ** (f e)


-- VPs (verb phrases) behave just like verbs
def VP (T : EventT) => Verb T


-- bare DPs (determiner phrases) are just entity quantifiers
def BDP (E : Type 0) => Quantifier E

def DP (SetT : SetterT) (E : Type 0)
  => Pi {T : EventT} -> VP (SetT E T) -> VP (SetT E T)


-- thetas transform a BDP into a DP with that thematic role
def Theta (SetT : SetterT) : Type 1
  => Pi {E : Type 0} -> BDP E -> DP SetT E

def mkTheta (GetT : GetterT)
  (get : Getter GetT)
  (SetT : SetterT)
  (inv : Invariant GetT SetT)
  : Theta SetT
  => \{E : Type 0} (q : BDP E) -- from Theta
  => \{T : EventT} (p : VP (SetT E T)) -- from DP
  => \(f : Event (SetT E T) -> Type 0) -- from VP
  => q (\(x : E) => p (\(e : Event (SetT E T))
    => Sig (get e = coe (inv T E) x) ** (f e)))

def agentDef : Theta SetAgentT
  => \{E} => mkTheta GetAgentT (\{T} => getAgent {T}) SetAgentT AgentT-inv {E}


def Sentence => Type 0

def mkSentence {T : EventT} (p : VP T) : Sentence => p (\x => Unit)