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'