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

open import Data.Bool.Order
open import Data.Bool.Base

open import Order.Base
open import Order.Cat

import Cat.Reasoning as 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, or walking arrow, 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 ${0 \leq 1} .$ 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 $⊥ \leq ⊤ .$

open Precategory

Bool-poset : Poset lzero lzero
Bool-poset .Poset.Ob        = Bool
Bool-poset .Poset._≤_       = _≤_
Bool-poset .Poset.≤-thin    = hlevel 1
Bool-poset .Poset.≤-refl    = ≤-refl
Bool-poset .Poset.≤-trans   = ≤-trans
Bool-poset .Poset.≤-antisym = ≤-antisym

The interval category is the category underlying the poset of booleans:

0≤1 : Precategory lzero lzero
0≤1 = poset→category Bool-poset

0≤1-connected : is-connected-cat 0≤1
0≤1-connected = mk-connected-cat false λ _ → zig _ []

Meets🔗

Note that the category ${0 \leq 1}$ 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 = _
0≤1-top .has⊤ false .paths _ = refl

0≤1-top .has⊤ true  .centre = _
0≤1-top .has⊤ true  .paths _ = refl

0≤1-products : ∀ A B → Product 0≤1 A B
0≤1-products A B .apex = and A B
0≤1-products A B .π₁   = and-≤l A B
0≤1-products A B .π₂   = and-≤r A B
0≤1-products A B .has-is-product .⟨_,_⟩ = and-univ _ A B
0≤1-products A B .has-is-product .π₁∘⟨⟩ = prop!
0≤1-products A B .has-is-product .π₂∘⟨⟩ = prop!
0≤1-products A B .has-is-product .unique _ _ = prop!

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 univalent category it is a groupoid, and for a poset it is a set.

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

private variable
  o ℓ : Level

Arrow : Precategory o ℓ → Type (o ⊔ ℓ)
Arrow 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 → Arrow C
  Hom→Arrow f = _ , _ , f

  Arrow-path
    : {a b : Arrow 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
  Arrow-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 $Arr (C),$ as defined above, and the space of functors $[{0 \leq 1}, C] .$

module _ {C : Precategory o ℓ} where
  import Cat.Reasoning C as C

  arrow→functor : Arrow 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} _ = C.id
    fun .F₁ {false} {true}  _ = f
    fun .F₁ {true}  {true}  _ = C.id

    fun .F-id {false} = refl
    fun .F-id {true} = refl
    fun .F-∘ {false} {false} {false} _ _ = sym (C.idl _)
    fun .F-∘ {false} {false} {true}  _ _ = sym (C.idr _)
    fun .F-∘ {false} {true}  {true}  _ _ = sym (C.idl _)
    fun .F-∘ {true}  {true}  {true}  _ _ = 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 $0 \leq 1$ maps to, and type inference can fill in the domain/codomain.

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

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} _ → sym (F-id F)
           ; {false} {true}  _ → refl
           ; {true}  {true}  _ → sym (F-id F) })

    linv : is-left-inverse functor→arrow arrow→functor
    linv x = refl

Correspondingly, we could define the arrow category $Arr (C)$ as the functor category $[{0 \leq 1}, C],$ but we prefer a definition in components for usability reasons.

module _ {o ℓ} (C : Precategory o ℓ) where
  private
    module C = Precategory C
    variable a b x y : ⌞ C ⌟

  record Homᵃ (f : C.Hom a b) (g : C.Hom x y) : Type ℓ where
    no-eta-equality

    field
      top : C.Hom a x
      bot : C.Hom b y
      com : g C.∘ top ≡ bot C.∘ f

{-# INLINE Homᵃ.constructor #-}
private unquoteDecl eqv = declare-record-iso eqv (quote Homᵃ)
open Homᵃ public

module _ {o ℓ} {C : Precategory o ℓ} {a b x y : ⌞ C ⌟} {f : C .Hom a b} {g : C .Hom x y} where instance
  H-Level-Homᵃ : ∀ {n} → H-Level (Homᵃ C f g) (2 + n)
  H-Level-Homᵃ = basic-instance 2 $ Iso→is-hlevel 2 eqv (hlevel 2)

  Extensional-Homᵃ
    : ∀ {ℓr} ⦃ sab : Extensional (C .Hom a x × C .Hom b y) ℓr ⦄
    → Extensional (Homᵃ C f g) ℓr
  Extensional-Homᵃ ⦃ sab ⦄ =
    injection→extensional!
      (λ { p i .top → p i .fst
         ; p i .bot → p i .snd
         ; {x} {y} p i .com → is-prop→pathp (λ i → C .Hom-set _ _ (C ._∘_ g (p i .fst)) (C ._∘_ (p i .snd) f)) (x .com) (y .com) i })
      sab

Arr : Precategory o ℓ → Precategory (o ⊔ ℓ) ℓ
Arr C .Ob                          = Arrow C
Arr C .Hom (_ , _ , f) (_ , _ , g) = Homᵃ C f g
Arr C .Hom-set _ _ = hlevel 2
Arr C .id  = record
  { top = C .id
  ; bot = C .id
  ; com = C .idr _ ∙ sym (C .idl _)
  }
Arr C ._∘_ sa sb = record where
  module C = Cat C

  top = sa .top C.∘ sb .top
  bot = sa .bot C.∘ sb .bot
  com = C.extendl (sa .com) ∙ C.pushr (sb .com)
Arr C .idr   f     = ext (C .idr _       ,ₚ C .idr _)
Arr C .idl   f     = ext (C .idl _       ,ₚ C .idl _)
Arr C .assoc f g h = ext (C .assoc _ _ _ ,ₚ C .assoc _ _ _)