per

module sample do

def quot : U := U

-- def S¹ (X : U ) : U := | base : S¹ ; loop : Equ S¹ base base |
-- def L¹ (A : U) := | nil : L¹ A ; cons : (x: A, xs: L¹ A) L¹ A |

-- def quot2 (X: U) (R : M -> A -> U) : U
--  := |
--       quotient : (a : A), quot A R ;
--       identification : (a b: A) (r: R a b) (e: Equ A a b) quot A R
--     |