{-# OPTIONS --cubical #-}
open import 1Lab.Counterexamples.IsIso -- (text page)
open import 1Lab.Counterexamples.Russell -- (text page)
open import 1Lab.Counterexamples.Sigma -- (text page)
open import 1Lab.Equiv -- (text page)
open import 1Lab.Equiv.Biinv -- (text page)
open import 1Lab.Equiv.Embedding -- (text page)
open import 1Lab.Equiv.Fibrewise -- (text page)
open import 1Lab.Equiv.FromPath -- (text page)
open import 1Lab.Equiv.HalfAdjoint -- (text page)
open import 1Lab.HIT.S1 -- (text page)
open import 1Lab.HIT.Sinfty -- (text page)
open import 1Lab.HIT.Sphere -- (text page)
open import 1Lab.HIT.Suspension -- (text page)
open import 1Lab.HIT.Torus -- (text page)
open import 1Lab.HIT.Truncation -- (text page)
open import 1Lab.HLevel -- (text page)
open import 1Lab.HLevel.Retracts -- (text page)
open import 1Lab.HLevel.Sets -- (text page)
open import 1Lab.HLevel.Universe -- (text page)
open import 1Lab.Path -- (text page)
open import 1Lab.Path.Groupoid -- (text page)
open import 1Lab.Prelude -- (code only)
open import 1Lab.Reflection -- (code only)
open import 1Lab.Reflection.Record -- (code only)
open import 1Lab.Rewrite -- (code only)
open import 1Lab.Type -- (text page)
open import 1Lab.Type.Dec -- (text page)
open import 1Lab.Type.Pi -- (text page)
open import 1Lab.Type.Prop -- (text page)
open import 1Lab.Type.Sigma -- (text page)
open import 1Lab.Univalence -- (text page)
open import 1Lab.Univalence.SIP -- (text page)
open import 1Lab.Univalence.SIP.Auto -- (code only)
open import 1Lab.Univalence.SIP.Record -- (code only)
open import 1Lab.Univalence.SIP.Record.Base -- (code only)
open import 1Lab.Univalence.SIP.Record.Parse -- (code only)
open import 1Lab.Univalence.SIP.Record.Prop -- (code only)
open import 1Lab.intro -- (text page)
open import Algebra.Group -- (text page)
open import Algebra.Group.Ab -- (text page)
open import Algebra.Group.Ab.Free -- (text page)
open import Algebra.Group.Cat.Base -- (text page)
open import Algebra.Group.Cat.FinitelyComplete -- (text page)
open import Algebra.Group.Cayley -- (text page)
open import Algebra.Group.Free -- (text page)
open import Algebra.Group.Homotopy -- (text page)
open import Algebra.Group.Homotopy.BAut -- (text page)
open import Algebra.Group.Subgroup -- (text page)
open import Algebra.Lattice -- (text page)
open import Algebra.Magma -- (text page)
open import Algebra.Magma.Unital -- (text page)
open import Algebra.Magma.Unital.EckmannHilton -- (text page)
open import Algebra.Monoid -- (text page)
open import Algebra.Monoid.Category -- (text page)
open import Algebra.Prelude -- (code only)
open import Algebra.Ring.Base -- (text page)
open import Algebra.Semigroup -- (text page)
open import Algebra.Semilattice -- (text page)
open import Authors -- (text page)
open import Cat.Abelian.Base -- (text page)
open import Cat.Abelian.Images -- (text page)
open import Cat.Abelian.Limits -- (text page)
open import Cat.Base -- (text page)
open import Cat.CartesianClosed.Base -- (text page)
open import Cat.CartesianClosed.Instances.PSh -- (code only)
open import Cat.CartesianClosed.Locally -- (text page)
open import Cat.Diagram.Coequaliser -- (text page)
open import Cat.Diagram.Coequaliser.RegularEpi -- (text page)
open import Cat.Diagram.Colimit.Base -- (text page)
open import Cat.Diagram.Congruence -- (text page)
open import Cat.Diagram.Coproduct -- (text page)
open import Cat.Diagram.Coproduct.Indexed -- (text page)
open import Cat.Diagram.Duals -- (text page)
open import Cat.Diagram.End -- (text page)
open import Cat.Diagram.Equaliser -- (text page)
open import Cat.Diagram.Equaliser.Kernel -- (text page)
open import Cat.Diagram.Equaliser.RegularMono -- (text page)
open import Cat.Diagram.Everything -- (code only)
open import Cat.Diagram.Idempotent -- (text page)
open import Cat.Diagram.Image -- (text page)
open import Cat.Diagram.Initial -- (text page)
open import Cat.Diagram.Limit.Base -- (text page)
open import Cat.Diagram.Limit.Equaliser -- (text page)
open import Cat.Diagram.Limit.Finite -- (text page)
open import Cat.Diagram.Limit.Product -- (text page)
open import Cat.Diagram.Limit.Pullback -- (text page)
open import Cat.Diagram.Monad -- (text page)
open import Cat.Diagram.Monad.Limits -- (text page)
open import Cat.Diagram.Product -- (text page)
open import Cat.Diagram.Product.Indexed -- (text page)
open import Cat.Diagram.Pullback -- (text page)
open import Cat.Diagram.Pullback.Properties -- (text page)
open import Cat.Diagram.Pushout -- (text page)
open import Cat.Diagram.Sieve -- (text page)
open import Cat.Diagram.Terminal -- (text page)
open import Cat.Diagram.Zero -- (text page)
open import Cat.Displayed.Base -- (text page)
open import Cat.Displayed.Cartesian -- (text page)
open import Cat.Displayed.Instances.Family -- (text page)
open import Cat.Displayed.Instances.Slice -- (text page)
open import Cat.Displayed.Total -- (text page)
open import Cat.Functor.Adjoint -- (text page)
open import Cat.Functor.Adjoint.Compose -- (text page)
open import Cat.Functor.Adjoint.Continuous -- (text page)
open import Cat.Functor.Adjoint.Hom -- (text page)
open import Cat.Functor.Adjoint.Monad -- (text page)
open import Cat.Functor.Adjoint.Monadic -- (text page)
open import Cat.Functor.Adjoint.Reflective -- (text page)
open import Cat.Functor.Amnestic -- (text page)
open import Cat.Functor.Base -- (text page)
open import Cat.Functor.Bifunctor -- (text page)
open import Cat.Functor.Conservative -- (text page)
open import Cat.Functor.Equivalence -- (text page)
open import Cat.Functor.Equivalence.Complete -- (text page)
open import Cat.Functor.Everything -- (code only)
open import Cat.Functor.FullSubcategory -- (text page)
open import Cat.Functor.Hom -- (text page)
open import Cat.Functor.Kan -- (text page)
open import Cat.Functor.Kan.Nerve -- (text page)
open import Cat.Functor.Pullback -- (text page)
open import Cat.Functor.Reasoning -- (text page)
open import Cat.Functor.Slice -- (text page)
open import Cat.Instances.Comma -- (text page)
open import Cat.Instances.Comma.Univalent -- (text page)
open import Cat.Instances.Delooping -- (text page)
open import Cat.Instances.Discrete -- (text page)
open import Cat.Instances.Elements -- (text page)
open import Cat.Instances.FinSet -- (text page)
open import Cat.Instances.Functor -- (text page)
open import Cat.Instances.Functor.Duality -- (text page)
open import Cat.Instances.Functor.Limits -- (text page)
open import Cat.Instances.Karoubi -- (text page)
open import Cat.Instances.Lift -- (text page)
open import Cat.Instances.Product -- (text page)
open import Cat.Instances.Sets -- (text page)
open import Cat.Instances.Sets.CartesianClosed -- (text page)
open import Cat.Instances.Sets.Cocomplete -- (text page)
open import Cat.Instances.Sets.Complete -- (text page)
open import Cat.Instances.Sets.Congruences -- (text page)
open import Cat.Instances.Shape.Cospan -- (text page)
open import Cat.Instances.Shape.Interval -- (text page)
open import Cat.Instances.Shape.Join -- (text page)
open import Cat.Instances.Shape.Parallel -- (text page)
open import Cat.Instances.Shape.Terminal -- (text page)
open import Cat.Instances.Slice -- (text page)
open import Cat.Instances.Slice.Presheaf -- (text page)
open import Cat.Instances.StrictCat -- (text page)
open import Cat.Instances.StrictCat.Cohesive -- (text page)
open import Cat.Morphism -- (text page)
open import Cat.Prelude -- (code only)
open import Cat.Reasoning -- (text page)
open import Cat.Solver -- (text page)
open import Cat.Thin -- (text page)
open import Cat.Thin.Completion -- (text page)
open import Cat.Thin.Instances.Sub -- (text page)
open import Cat.Thin.Limits -- (text page)
open import Cat.Univalent -- (text page)
open import Cat.Univalent.Instances.Algebra -- (text page)
open import Cat.Univalent.Rezk -- (text page)
open import Data.Bool -- (text page)
open import Data.Fin -- (text page)
open import Data.Fin.Base -- (text page)
open import Data.Fin.Closure -- (text page)
open import Data.Fin.Properties -- (text page)
open import Data.Int -- (text page)
open import Data.Int.Inductive -- (text page)
open import Data.List -- (text page)
open import Data.Nat -- (text page)
open import Data.Nat.Base -- (text page)
open import Data.Nat.Properties -- (text page)
open import Data.Power -- (text page)
open import Data.Power.Lattice -- (text page)
open import Data.Set.Coequaliser -- (text page)
open import Data.Set.Truncation -- (text page)
open import Data.Sum -- (text page)
open import Relation.Order -- (text page)
open import Relation.Order.Lexicographic -- (text page)
open import Topoi.Base -- (text page)
open import Topoi.Classifying.Diaconescu -- (text page)
open import Topoi.Reasoning -- (text page)
open import index -- (text page)
open import wip.arity -- (code only)
open import wip.artin -- (code only)
open import wip.exact -- (code only)
open import wip.flat -- (code only)
open import wip.giraud -- (code only)
open import wip.image -- (code only)
open import wip.inst -- (code only)
open import wip.obj -- (code only)
open import wip.site -- (code only)
open import wip.slice -- (code only)
open import wip.test -- (code only)
open import wip.test2 -- (code only)
open import wip.test3 -- (code only)
open import wip.test4 -- (code only)
open import wip.test6 -- (code only)
open import wip.test7 -- (code only)
import Agda.Builtin.Bool -- (builtin)
import Agda.Builtin.Char -- (builtin)
import Agda.Builtin.Cubical.HCompU -- (builtin)
import Agda.Builtin.Cubical.Path -- (builtin)
import Agda.Builtin.Cubical.Sub -- (builtin)
import Agda.Builtin.Float -- (builtin)
import Agda.Builtin.FromNat -- (builtin)
import Agda.Builtin.FromNeg -- (builtin)
import Agda.Builtin.Int -- (builtin)
import Agda.Builtin.List -- (builtin)
import Agda.Builtin.Maybe -- (builtin)
import Agda.Builtin.Nat -- (builtin)
import Agda.Builtin.Reflection -- (builtin)
import Agda.Builtin.Sigma -- (builtin)
import Agda.Builtin.String -- (builtin)
import Agda.Builtin.Unit -- (builtin)
import Agda.Builtin.Word -- (builtin)
import Agda.Primitive.Cubical -- (builtin)
import Agda.Primitive -- (builtin)