module Algebra.Prelude where

open import Cat.Instances.Shape.Terminal public
open import Cat.Functor.FullSubcategory public
open import Cat.Instances.Product public
open import Cat.Instances.Functor public
open import Cat.Instances.Comma public
open import Cat.Instances.Slice public
open import Cat.Functor.Adjoint public
open import Cat.Functor.Base public
open import Cat.Functor.Hom public
open import Cat.Univalent public
open import Cat.Prelude hiding (_+_ ; _-_ ; _*_) public

open import Cat.Diagram.Coequaliser public
open import Cat.Diagram.Coproduct public
open import Cat.Diagram.Equaliser public
open import Cat.Diagram.Pullback public
open import Cat.Diagram.Terminal public
open import Cat.Diagram.Initial public
open import Cat.Diagram.Pushout public
open import Cat.Diagram.Product public
open import Cat.Diagram.Image public
open import Cat.Diagram.Zero public

import Cat.Reasoning

open import Cat.Displayed.Univalence.Thin public

module Cat {o ℓ} (C : Precategory o ℓ) where
  open Cat.Reasoning C public