module Cat.Displayed.Fibre.Reasoning
  {o β„“ o' β„“'} {B : Precategory o β„“}
  (E : Displayed B o' β„“')
  where

Reasoning in fibre categoriesπŸ”—

This module defines some helpers to help formalisation go smoother when we’re working with fibre categories. Mathematically, it’s not very interesting: it’s pure engineering.

private variable
  a b c d x y z : B.Ob
  x' x'' y' z' z'' : Ob[ x ]
  a' b' c' d' : Ob[ a ]
  f g h i j k : B.Hom x y
  f' g' h' i' j' k' : Hom[ f ] x' y'
  p : f ≑ g

opaque
  to-fibre
    : f' ∘' g' ≑[ B.idl _ ] f' Fib.∘ g'
  to-fibre = to-pathp refl

  over-fibre
    : f' ∘' g' ≑[ p ] h' ∘' i'
    β†’ f' Fib.∘ g' ≑ h' Fib.∘ i'
  over-fibre p' = ap hom[] (cast[] p')

opaque
  pullrf
    : g' ∘' h' ≑[ p ] i'
    β†’ (f' Fib.∘ g') ∘' h' ≑[ p βˆ™ sym (B.idl _) ] f' ∘' i'
  pullrf p' = cast[] $ to-pathp⁻ (whisker-l (B.idl _)) βˆ™[] pullr[] _ p'

opaque
  pulllf
    : f' ∘' g' ≑[ p ] i'
    β†’ f' ∘' (g' Fib.∘ h') ≑[ p βˆ™ sym (B.idr _) ] i' ∘' h'
  pulllf p' = cast[] $ to-pathp⁻ (whisker-r (B.idl _)) βˆ™[] pulll[] _ p'

opaque
  pushrf
    : {p : i ≑ B.id B.∘ h}
    β†’ i' ≑[ p ] g' ∘' h'
    β†’ f' ∘' i' ≑[ B.idl _ βˆ™ p ] (f' Fib.∘ g') ∘' h'
  pushrf {h = h} p' =
    cast[] $ pushr[] _ p'
    βˆ™[] to-pathp (unwhisker-l (ap (B._∘ h) (B.idl _)) (B.idl _))

opaque
  pushlf
    : {p : i ≑ f B.∘ B.id}
    β†’ i' ≑[ p ] f' ∘' g'
    β†’ i' ∘' h' ≑[ B.idr _ βˆ™ p ] f' ∘' (g' Fib.∘ h')
  pushlf {f = f} p' =
    cast[] $ pushl[] _ p'
    βˆ™[] to-pathp (unwhisker-r (ap (f B.∘_) (B.idl _)) (B.idl _))

opaque
  extendrf
    : {p : B.id B.∘ i ≑ B.id B.∘ k}
    β†’ g' ∘' i' ≑[ p ] h' ∘' k'
    β†’ (f' Fib.∘ g') ∘' i' ≑[ p ] (f' Fib.∘ h') ∘' k'
  extendrf {k = k} p' = cast[] $
    to-pathp⁻ (whisker-l (B.idl _))
    βˆ™[] extendr[] _ p'
    βˆ™[] to-pathp (unwhisker-l (ap (B._∘ k) (B.idl _)) (B.idl _))

opaque
  extendlf
    : {p : f B.∘ B.id ≑ g B.∘ B.id}
    β†’ f' ∘' h' ≑[ p ] g' ∘' k'
    β†’ f' ∘' (h' Fib.∘ i') ≑[ p ] g' ∘' (k' Fib.∘ i')
  extendlf {g = g} p' = cast[] $
    to-pathp⁻ (whisker-r (B.idl _))
    βˆ™[] extendl[] _ p'
    βˆ™[] to-pathp (unwhisker-r (ap (g B.∘_) (B.idl _)) (B.idl _))

opaque
  cancellf
    : {p : f B.∘ B.id ≑ B.id}
    β†’ f' ∘' g' ≑[ p ] id'
    β†’ f' ∘' (g' Fib.∘ h') ≑[ p ] h'
  cancellf p' = cast[] $ to-pathp⁻ (whisker-r (B.idl _)) βˆ™[] cancell[] _ p'

opaque
  cancelrf
    : {p : B.id B.∘ h ≑ B.id}
    β†’ g' ∘' h' ≑[ p ] id'
    β†’ (f' Fib.∘ g') ∘' h' ≑[ p ] f'
  cancelrf p' = cast[] $ to-pathp⁻ (whisker-l (B.idl _)) βˆ™[] cancelr[] _ p'