open import Cat.Displayed.Fibre
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Displayed.Reasoning
import Cat.Reasoning

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

private
module B = Cat.Reasoning B
open Displayed E
open Cat.Displayed.Reasoning E
module Fib {x} = Cat.Reasoning (Fibre E x)

open Fib public


## 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'