Index

ΓY:UΓ,n:YA(n):UΓΠ(n:Y).A(n):U \frac { \Gamma \vdash Y : \mathcal U \qquad \Gamma, n : Y \vdash A(n) : \mathcal U }{ \Gamma \vdash \Pi (n : Y) . A(n) : \mathcal U } Γ,n:Ya:A(n)Γ(λn.a):Π(n:Y).A(n) \frac { \Gamma , n : Y \vdash a : A(n) }{ \Gamma \vdash (\lambda n . a) : \Pi (n : Y) . A(n) } ΓY:UΓ,n:YA(n):UΓΣ(n:Y).A(n):U \frac { \Gamma \vdash Y : \mathcal U \qquad \Gamma, n : Y \vdash A(n) : \mathcal U }{ \Gamma \vdash \Sigma (n : Y) . A(n) : \mathcal U } Γn:YΓa:A(n)Γ(n,a):Σ(n:Y).A(n) \frac { \Gamma \vdash n : Y \qquad \Gamma \vdash a : A(n) }{ \Gamma \vdash (n , a) : \Sigma (n : Y) . A(n) } ΓY:UΓ,n:Y,a:Yn=Ya:U \frac { \Gamma \vdash Y : \mathcal U }{ \Gamma , n : Y , a : Y \vdash n =_Y a : \mathcal U } Γn:YΓrefln:n=Yn \frac { \Gamma \vdash n : Y }{ \Gamma \vdash {\sf refl}_n : n =_Y n }