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

module lib.types.EilenbergMacLane1 where

open import lib.types.EilenbergMacLane1.Core public
open import lib.types.EilenbergMacLane1.Recursion public
open import lib.types.EilenbergMacLane1.DoubleElim public
open import lib.types.EilenbergMacLane1.DoublePathElim public
open import lib.types.EilenbergMacLane1.FunElim public