open import Cat.Instances.Functor
open import Cat.Diagram.Terminal
open import Cat.Diagram.Product
open import Cat.Prelude

open import Data.Bool

open import Order.Base
open import Order.Cat

import Order.Reasoning as Poset

module Cat.Instances.Shape.Interval where

open is-product
open Terminal
open Product
open Functor


# Interval categoryπ

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

open Precategory

Bool-poset : Poset lzero lzero
Bool-poset = po 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:

  Rrefl : β {x} β R x x
Rrefl {false} = tt
Rrefl {true} = tt

Rtrans : β {x y z} β R x y β R y z β R x z
Rtrans {false} {false} {false} tt tt = tt
Rtrans {false} {false} {true}  tt tt = tt
Rtrans {false} {true}  {false} tt ()
Rtrans {false} {true}  {true}  tt tt = tt
Rtrans {true}  {false} {false} () tt
Rtrans {true}  {false} {true}  () tt
Rtrans {true}  {true}  {false} tt ()
Rtrans {true}  {true}  {true}  tt tt = tt

Rantisym : β {x y} β R x y β R y x β x β‘ y
Rantisym {false} {false} tt tt = refl
Rantisym {false} {true}  tt ()
Rantisym {true}  {false} () tt
Rantisym {true}  {true}  tt tt = refl

Rprop : β {x y} (p q : R x y) β p β‘ q
Rprop {false} {false} tt tt = refl
Rprop {false} {true}  tt tt = refl
Rprop {true}  {false} () ()
Rprop {true}  {true}  tt tt = refl

po : Poset _ _
po .Poset.Ob = Bool
po .Poset._β€_ = R
po .Poset.β€-thin = Rprop
po .Poset.β€-refl = Rrefl
po .Poset.β€-trans = Rtrans
po .Poset.β€-antisym = Rantisym

0β€1 : Precategory lzero lzero
0β€1 = posetβcategory Bool-poset


## Meetsπ

Note that the category is finitely complete (i.e.Β it is bounded, and has binary meets for every pair of elements): The top element is (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 = Poset.β€-thin Bool-poset _ _
0β€1-products A B .has-is-product .Οββfactor = Poset.β€-thin Bool-poset _ _
0β€1-products A B .has-is-product .unique _ _ _ = Poset.β€-thin Bool-poset _ _


# The space of arrowsπ

The total space of the 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 a functor out of corresponds rather directly to picking out an arrow in Its domain is the object that maps to, and is codomain is the object that maps to.

private variable
o β : Level

Arrows : Precategory o β β Type (o β β)
Arrows C = Ξ£[ A β C ] Ξ£[ B β C ] (C.Hom A B)
where module C = Precategory C

module _ (C : Precategory o β) where
HomβArrow : {a b : Ob C} β Hom C a b β Arrows C
HomβArrow f = _ , _ , f

Arrows-path
: {a b : Arrows C}
β (p : a .fst β‘ b .fst)
β (q : a .snd .fst β‘ b .snd .fst)
β PathP (Ξ» i β Hom C (p i) (q i)) (a .snd .snd) (b .snd .snd)
β a β‘ b
Arrows-path p q r i = p i , q i , r i


We now fix a category and prove the correspondence between the space of arrows as defined above, and the space of functors

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

    fun .F-id {false} = refl
fun .F-id {true} = refl
fun .F-β {false} {false} {false} tt tt = sym (C.idl _)
fun .F-β {false} {false} {true}  tt tt = sym (C.idr _)
fun .F-β {false} {true}  {false} () g
fun .F-β {false} {true}  {true}  tt tt = sym (C.idl _)
fun .F-β {true}  {false} {false} tt ()
fun .F-β {true}  {false} {true}  tt ()
fun .F-β {true}  {true}  {false} () g
fun .F-β {true}  {true}  {true}  tt tt = sym (C.idr _)


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 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 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 as the functor category

Arr : Precategory o β β Precategory (o β β) β
Arr C = Cat[ 0β€1 , C ]