{-# OPTIONS --safe --without-K #-}

open import Relation.Binary.Definitions           using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_)

module Context (Ty : Set) (Ty-Decidable : Decidable (_≡_ {A = Ty})) where

open import Context.Base       Ty              public
open import Context.Properties Ty Ty-Decidable public

Generated from commit 2fd14c996b195ef101dff8919e837907ca0a08aa.