{-# OPTIONS --without-K --safe #-}
module Cats.Category where

import Cats.Category.Base as Base
import Cats.Category.Constructions.CCC as CCC
import Cats.Category.Constructions.Epi as Epi
import Cats.Category.Constructions.Equalizer as Equalizer
import Cats.Category.Constructions.Exponential as Exponential
import Cats.Category.Constructions.Iso as Iso
import Cats.Category.Constructions.Initial as Initial
import Cats.Category.Constructions.Mono as Mono
import Cats.Category.Constructions.Product as Product
import Cats.Category.Constructions.Terminal as Terminal
import Cats.Category.Constructions.Thin as Thin
import Cats.Category.Constructions.Unique as Unique
import Cats.Limit as Limit


Category = Base.Category


module Category {lo la l≈} (Cat : Base.Category lo la l≈) where

  open Base.Category Cat public
  open Epi.Build Cat public
  open Equalizer.Build Cat public
  open Exponential.Build Cat public
  open Initial.Build Cat public
  open Iso.Build Cat public
  open Mono.Build Cat public
  open Product.Build Cat public
  open Terminal.Build Cat public
  open Unique.Build Cat public


open CCC public using (IsCCC)
open Exponential public using (HasExponentials)
open Initial public using (HasInitial)
open Limit public using (_HasLimitsOf_ ; Complete)
open Product public using
  ( HasProducts ; HasBinaryProducts ; HasFiniteProducts
  ; HasProducts→HasBinaryProducts
  ; HasProducts→HasTerminal )
open Terminal public using (HasTerminal)
open Thin public using (Thin ; StronglyThin ; StronglyThin→Thin)