Agda-2.3.2.2: examples/outdated-and-incorrect/univ/Example.agda

module Example where

open import Base
open import Nat
open import univ

-- Application

_#_ : {A : S}{F : El A -> S}{pF : Map _==_ _=S_ F} ->
      El (pi A F pF) -> (x : El A) -> El (F x)
el < f , pf > # x = f x

-- Projection

π₀ : {A : S}{F : El A -> S}{pF : Map _==_ _=S_ F} ->
     El (sigma A F pF) -> El A
π₀ (el < x , Fx >) = x

π₁ : {A : S}{F : El A -> S}{pF : Map _==_ _=S_ F} ->
     (p : El (sigma A F pF)) -> El (F (π₀ p))
π₁ (el < x , Fx >) = Fx