Prelude.Irrelevance

Source code on Github
{-# OPTIONS --with-K #-}
module Prelude.Irrelevance where

open import Prelude.Irrelevance.Core public
open import Prelude.Irrelevance.WithK public
open import Prelude.Irrelevance.Empty public
open import Prelude.Irrelevance.Product public
open import Prelude.Irrelevance.List public
open import Prelude.Irrelevance.Nat public
open import Prelude.Irrelevance.Int public