{-# OPTIONS --without-K --exact-split --rewriting #-}

module Pi.UFin.UFin where

open import Pi.UFin.Base public
open import Pi.UFin.BAut public
open import Pi.UFin.Univ public
open import Pi.UFin.Monoidal public