open import Cat.Diagram.Limit.Finite open import Cat.Instances.Functor open import Cat.Diagram.Terminal open import Cat.Diagram.Product open import Cat.Prelude open import Cat.Thin open import Data.Bool module Cat.Instances.Shape.Interval where

# Interval category🔗

The interval category is the category with two points, called (as a form of endearment) $0$ and $1$, and a single arrow between them. Correspondingly, in shorthand this category is referred to as $\intcat$. Since it has a single (non-trivial) arrow, it is a preorder; In fact, it is the preorder generated by the type of booleans and the natural ordering on them, with $\bot \le \top$.

open Precategory Bool-poset : Poset lzero lzero Bool-poset = make-poset {R = R} Rrefl Rtrans Rantisym Rprop where R : Bool → Bool → Type R false false = ⊤ R false true = ⊤ R true false = ⊥ R true true = ⊤

**Note**: We define the relation by recursion, rather
than by induction, to avoid the issues with computational behaviour with
indexed inductive types in Cubical Agda. The interval category is the
category underlying the poset of booleans:

0≤1 : Precategory lzero lzero 0≤1 = Bool-poset .Poset.underlying

## Meets🔗

Note that the category $\intcat$ is finitely complete (i.e. it is bounded, and has binary meets for every pair of elements): The top element is $\top$ (go figure), and meets are given by the boolean “and” function”.

0≤1-top : Terminal 0≤1 0≤1-top .top = true 0≤1-top .has⊤ false .centre = tt 0≤1-top .has⊤ false .paths tt = refl 0≤1-top .has⊤ true .centre = tt 0≤1-top .has⊤ true .paths tt = refl 0≤1-products : ∀ A B → Product 0≤1 A B 0≤1-products A B .apex = and A B

## A ridiculous amount of trivial pattern matching is needed to establish that this cone is universal, but fortunately, we can appeal to thinness to establish commutativity and uniqueness.

0≤1-products false false .π₁ = tt 0≤1-products false true .π₁ = tt 0≤1-products true false .π₁ = tt 0≤1-products true true .π₁ = tt 0≤1-products false false .π₂ = tt 0≤1-products false true .π₂ = tt 0≤1-products true false .π₂ = tt 0≤1-products true true .π₂ = tt 0≤1-products A B .has-is-product .⟨_,_⟩ = meet _ _ _ where meet : ∀ A B Q (p : Hom 0≤1 Q A) (q : Hom 0≤1 Q B) → Hom 0≤1 Q (and A B) meet false false false tt tt = tt meet false false true () () meet false true false tt tt = tt meet false true true () tt meet true false false tt tt = tt meet true false true tt () meet true true false tt tt = tt meet true true true tt tt = tt

0≤1-products A B .has-is-product .π₁∘factor = Bool-poset .Poset.Hom-is-prop _ _ _ _ 0≤1-products A B .has-is-product .π₂∘factor = Bool-poset .Poset.Hom-is-prop _ _ _ _ 0≤1-products A B .has-is-product .unique _ _ _ = Bool-poset .Poset.Hom-is-prop _ _ _ _ 0≤1-finitely-complete : Finitely-complete 0≤1 0≤1-finitely-complete = with-top-and-meets 0≤1 (Bool-poset .Poset.has-is-thin) 0≤1-top 0≤1-products

# The space of arrows🔗

The total space of the $\hom$ family of a precategory is referred to as its “space of arrows”. A point in this space is a “free-standing arrow”: it comes equipped with its own domain and codomain. We note that, since a precategory has no upper bound on the h-level of its space of objects, its space of arrows also need not be particularly truncated. However, for a thin category it is a set, and for a univalent category it is a groupoid.

An equivalent description of the space of arrows is as the collection of functors $[ \intcat, \ca{C} ]$: a functor out of $\intcat$ corresponds rather directly to picking out an arrow in $\ca{C}$. Its domain is the object that $\bot$ maps to, and is codomain is the object that $\top$ maps to.

Arrows : Precategory o ℓ → Type (o ⊔ ℓ) Arrows C = Σ[ A ∈ C.Ob ] Σ[ B ∈ C.Ob ] (C.Hom A B) where module C = Precategory C

We now fix a category and prove the correspondence between the space of arrows $\Arr{\ca{C}}$, as defined above, and the space of functors $[ \intcat, \ca{C} ]$.

module _ {C : Precategory o ℓ} where import Cat.Reasoning C as C arrow→functor : Arrows C → Functor 0≤1 C arrow→functor (A , B , f) = fun where fun : Functor _ _ fun .F₀ false = A fun .F₀ true = B fun .F₁ {false} {false} tt = C.id fun .F₁ {false} {true} tt = f fun .F₁ {true} {false} () fun .F₁ {true} {true} tt = C.id

The other direction, turning a functor into an object of Arr, is mostly immediate: we can extract the non-trivial arrow by seeing what the non-trivial arrow $0 \le 1$ maps to, and the domain/codomain can be inferred by Agda.

functor→arrow : Functor 0≤1 C → Arrows C functor→arrow F = _ , _ , F₁ F {false} {true} tt

That this function is an equivalence is also straightforward: The only non-trivial step is appealing to functoriality of $F$, specifically that it must preserve identity arrows. The converse direction (going functor → arrow → functor) is definitionally the identity.

arrow≃functor : is-equiv arrow→functor arrow≃functor = is-iso→is-equiv (iso functor→arrow rinv linv) where rinv : is-right-inverse functor→arrow arrow→functor rinv F = Functor-path (λ { true → refl ; false → refl }) (λ { {false} {false} tt → sym (F-id F) ; {false} {true} tt → refl ; {true} {false} () ; {true} {true} tt → sym (F-id F) }) linv : is-left-inverse functor→arrow arrow→functor linv x = refl

Correspondingly, we *define* the arrow category
$\Arr{\ca{C}}$
as the functor category
$[ \intcat, \ca{C} ]$.

Arr : Precategory o ℓ → Precategory (o ⊔ ℓ) ℓ Arr C = Cat[ 0≤1 , C ]