{-# OPTIONS --postfix-projections --rewriting --prop #-}

open Agda.Primitive

infix    _⁻¹
infixl   _∙_
infixr  _,_
infixr  _×_

-- Lift

record LiftP {i} (A : Prop i) : Set i where
  constructor lift
  field lower : A
open LiftP public

-- Unit type
record ⊤ {j} : Set j where
  constructor tt
open ⊤ public

record ⊤p {j} : Prop j where
  constructor tt
open ⊤p public

-- Σ-types
record Σ {i j} (A : Set i) (B : A → Set j) : Set (i ⊔ j) where
  constructor _,_
  field fst : A
        snd : B fst
open Σ public

_×_ : ∀ {i j} (A : Set i) (B : Set j) → Set (i ⊔ j)
A × B = Σ A λ _ → B

-- Equality types
data _≡_ {i} {A : Set i} (x : A) : A → Set i where refl : x ≡ x
{-# BUILTIN REWRITE _≡_ #-}

_⁻¹ : ∀ {i} {A : Set i} {x y : A} → x ≡ y → y ≡ x
refl ⁻¹ = refl

_∙_ : ∀ {i} {A : Set i} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
refl ∙ refl = refl