open import Cat.Functor.Hom.Displayed
open import Cat.Instances.Functor
open import Cat.Instances.Product
open import Cat.Displayed.Fibre
open import Cat.Displayed.Base
open import Cat.Functor.Hom
open import Cat.Prelude

import Cat.Displayed.Cartesian.Indexing as Indexing
import Cat.Displayed.Fibre.Reasoning as FibR
import Cat.Displayed.Cartesian as Cart
import Cat.Displayed.Reasoning as DR
import Cat.Displayed.Morphism as DM
import Cat.Reasoning as CR

module Cat.Displayed.Cartesian.Weak
{o β o' β'}
{β¬ : Precategory o β}
(β° : Displayed β¬ o' β')
where

open CR β¬
open Displayed β°
open Cart β°
open DR β°
open DM β°
open Functor
open Functor
private module Fib = FibR β°


Weak cartesian morphismsπ

Some authors use a weaker notion of cartesian morphism when defining fibrations, referred to as a βweak cartesianβ or βhypocartesianβ morphism. Such morphisms only allow for the construction of universal maps when the morphism to be factored is displayed over the same morphism as the weak cartesian map. This situation is best understood graphically.

record is-weak-cartesian
{a b a' b'} (f : Hom a b) (f' : Hom[ f ] a' b')
: Type (o β β β o' β β')
where
no-eta-equality
field
universal : β {x'} β (g' : Hom[ f ] x' b') β Hom[ id ] x' a'
commutes  : β {x'} β (g' : Hom[ f ] x' b') β f' β' universal g' β‘[ idr _ ] g'
unique    : β {x'} {g' : Hom[ f ] x' b'}
β (h' : Hom[ id ] x' a')
β f' β' h' β‘[ idr _ ] g'
β h' β‘ universal g'

open is-weak-cartesian


Like their stronger counterparts, weak cartesian lifts are unique up to vertical isomorphism.

weak-cartesian-domain-unique
: β {x y} {f : Hom x y}
β β {x' x'' y'} {f' : Hom[ f ] x' y'} {f'' : Hom[ f ] x'' y'}
β is-weak-cartesian f f'
β is-weak-cartesian f f''
β x' ββ x''
weak-cartesian-domain-unique {f' = f'} {f'' = f''} f'-weak f''-weak =
make-iso[ _ ] to* from*
(to-pathp $unique f''-weak _ invl* β (sym$ unique f''-weak _ (idr' f'')))
(to-pathp $unique f'-weak _ invr* β (sym$ unique f'-weak _ (idr' f')))
where
open is-weak-cartesian

to* = universal f''-weak f'
from* = universal f'-weak f''

invl* : f'' β' hom[] (to* β' from*) β‘[ idr _ ] f''
invl* = to-pathp $hom[] (f'' β' hom[] (to* β' from*)) β‘β¨ smashr _ _ β©β‘ hom[] (f'' β' to* β' from*) β‘β¨ reviveβ {p = ap (_ β_) (idl _)} (pulll' (idr _) (f''-weak .commutes f')) β©β‘ hom[] (f' β' from*) β‘β¨ reviveβ (f'-weak .commutes f'') β©β‘ hom[] f'' β‘β¨ liberate _ β©β‘ f'' β invr* : f' β' hom[] (from* β' to*) β‘[ idr _ ] f' invr* = to-pathp$
hom[] (f' β' hom[] (from* β' to*)) β‘β¨ smashr _ _ β©β‘
hom[] (f' β' from* β' to*)         β‘β¨ reviveβ {p = ap (_ β_) (idl _)} (pulll' (idr _) (f'-weak .commutes f'')) β©β‘
hom[] (f'' β' to*)                  β‘β¨ reviveβ (f''-weak .commutes f') β©β‘
hom[] f'                           β‘β¨ liberate _ β©β‘
f' β


As one would expect, cartesian maps are always weakly cartesian. Proving this does involve a bit of cubical yoga, as the maps we want to factorize arenβt definitionally composites, but we can use the generalized versions of the functions from Cartesian to get the job done.

cartesianβweak-cartesian : β {x y x' y'} {f : Hom x y} {f' : Hom[ f ] x' y'}
β is-cartesian f f'
β is-weak-cartesian f f'
cartesianβweak-cartesian {f = f} {f' = f'} cart = weak-cart where
open is-cartesian cart

weak-cart : is-weak-cartesian f f'
weak-cart .universal g' = universalv g'
weak-cart .commutes g' = commutesv g'
weak-cart .unique h' p = uniquev h' p


Furthermore, if is a fibration, weakly cartesian morphisms are also cartesian. To see this, we note that the lift of is cartesian, and thus also a weak cartesian morphism. This implies that there is an isomorphism between their codomains, which allows us to invoke cartesian-vert-retraction-stable to show that must also be cartesian.

weak-cartesianβcartesian
: β {x y x' y'} {f : Hom x y} {f' : Hom[ f ] x' y'}
β (fib : Cartesian-fibration)
β is-weak-cartesian f f'
β is-cartesian f f'
weak-cartesianβcartesian {x = x} {y' = y'} {f = f} {f' = f'} fib f-weak = f-cart where
open Cartesian-fibration fib
module f-weak = is-weak-cartesian f-weak

x* : Ob[ x ]
x* = has-lift.x' f y'

f* : Hom[ f ] x* y'
f* = has-lift.lifting f y'

f*-cart : is-cartesian f f*
f*-cart = has-lift.cartesian f y'

f*-weak : is-weak-cartesian f f*
f*-weak = cartesianβweak-cartesian f*-cart

f-cart : is-cartesian f f'
f-cart =
cartesian-vertical-retraction-stable f*-cart
(iso[]βto-has-section[] (weak-cartesian-domain-unique f*-weak f-weak))
(f-weak.commutes f*)


is a weak cartesian morphism if and only if postcomposition of onto vertical maps is an equivalence.

postcompose-equivβweak-cartesian
: β {x y x' y'} {f : Hom x y}
β (f' : Hom[ f ] x' y')
β (β {x''} β is-equiv {A = Hom[ id ] x'' x'} (f' β'_))
β is-weak-cartesian f f'
postcompose-equivβweak-cartesian f' eqv .universal h' =
equivβinverse eqv (hom[ idr _ ]β» h')
postcompose-equivβweak-cartesian f' eqv .commutes h' =
to-pathpβ» (equivβcounit eqv (hom[ idr _ ]β» h'))
postcompose-equivβweak-cartesian f' eqv .unique m' p =
(sym $equivβunit eqv m') β ap (equivβinverse eqv) (from-pathpβ» p) weak-cartesianβpostcompose-equiv : β {x y x' x'' y'} {f : Hom x y} {f' : Hom[ f ] x' y'} β is-weak-cartesian f f' β is-equiv {A = Hom[ id ] x'' x'} (f' β'_) weak-cartesianβpostcompose-equiv wcart = is-isoβis-equiv$
iso (Ξ» h' β wcart .universal (hom[ idr _ ] h'))
(Ξ» h' β from-pathpβ» (wcart .commutes _) Β·Β· hom[]-β _ _ Β·Β· liberate _)
(Ξ» h' β sym $wcart .unique _ (to-pathp refl))  Weak cartesian liftsπ We can also define a notion of weak cartesian lifts, much like we can with their stronger cousins. record Weak-cartesian-lift {x y} (f : Hom x y) (y' : Ob[ y ]) : Type (o β β β o' β β') where no-eta-equality field {x'} : Ob[ x ] lifting : Hom[ f ] x' y' weak-cartesian : is-weak-cartesian f lifting open is-weak-cartesian weak-cartesian public  A displayed category that has weak cartesian lifts for all morphisms in the base is called a weak cartesian fibration, though we will often use the term weak fibration. Other authors call weak fibrations prefibred categories, though we avoid this name as it conflicts with the precategory/category distinction. record is-weak-cartesian-fibration : Type (o β β β o' β β') where no-eta-equality field weak-lift : β {x y} β (f : Hom x y) β (y' : Ob[ y ]) β Weak-cartesian-lift f y' module weak-lift {x y} (f : Hom x y) (y' : Ob[ y ]) = Weak-cartesian-lift (weak-lift f y')  Note that if is a weak fibration, we can define an operation that allows us to move vertical morphisms between fibres. This is actually enough to define base change functors, though they are not well behaved unless is a fibration.  rebase : β {x y y' y''} β (f : Hom x y) β Hom[ id ] y' y'' β Hom[ id ] (weak-lift.x' f y') (weak-lift.x' f y'') rebase f vert = weak-lift.universal f _ (hom[ idl _ ] (vert β' weak-lift.lifting f _))  Every fibration is a weak fibration. cartesian-liftβweak-cartesian-lift : β {x y} {f : Hom x y} {y' : Ob[ y ]} β Cartesian-lift f y' β Weak-cartesian-lift f y' fibrationβweak-fibration : Cartesian-fibration β is-weak-cartesian-fibration  The proofs of these facts are just shuffling around data, so we omit them. cartesian-liftβweak-cartesian-lift cart .Weak-cartesian-lift.x' = Cartesian-lift.x' cart cartesian-liftβweak-cartesian-lift cart .Weak-cartesian-lift.lifting = Cartesian-lift.lifting cart cartesian-liftβweak-cartesian-lift cart .Weak-cartesian-lift.weak-cartesian = cartesianβweak-cartesian (Cartesian-lift.cartesian cart) fibrationβweak-fibration fib .is-weak-cartesian-fibration.weak-lift x y' = cartesian-liftβweak-cartesian-lift (Cartesian-fibration.has-lift fib x y')  Notably, weak fibrations are fibrations when weak cartesian morphisms are closed under composition. module _ where open Cartesian-fibration open is-cartesian weak-fibrationβfibration : is-weak-cartesian-fibration β (β {x y z x' y' z'} {f : Hom y z} {g : Hom x y} β {f' : Hom[ f ] y' z'} {g' : Hom[ g ] x' y'} β is-weak-cartesian f f' β is-weak-cartesian g g' β is-weak-cartesian (f β g) (f' β' g')) β Cartesian-fibration weak-fibrationβfibration weak-fib weak-β .has-lift {x = x} f y' = f-lift where open is-weak-cartesian-fibration weak-fib module weak-β {x y z} (f : Hom y z) (g : Hom x y) (z' : Ob[ z ]) = is-weak-cartesian (weak-β (weak-lift.weak-cartesian f z') (weak-lift.weak-cartesian g _))  To show that has a cartesian lift, we begin by taking the weak cartesian lift of  x* : Ob[ x ] x* = weak-lift.x' f y' f* : Hom[ f ] x* y' f* = weak-lift.lifting f y' f*-weak-cartesian : is-weak-cartesian f f* f*-weak-cartesian = weak-lift.weak-cartesian f y' module f* = is-weak-cartesian (f*-weak-cartesian)  We must now show that the weak cartesian morphism is actually cartesian. To do this, we must construct the following unique universal map: To do this, we shall first take the weak cartesian lift of Both and are weak cartesian, which means that their composite is also weak cartesian by our hypothesis. We can then factor through to obtain a vertical morphism which we can then compose with to obtain the requisite map.  module Morphisms {u : Ob} {u' : Ob[ u ]} (m : Hom u x) (h' : Hom[ f β m ] u' y') where u* : Ob[ u ] u* = weak-lift.x' m _ m* : Hom[ m ] u* x* m* = weak-lift.lifting m _ m*-weak-cartesian : is-weak-cartesian m m* m*-weak-cartesian = weak-lift.weak-cartesian m x* module m* = is-weak-cartesian m*-weak-cartesian module f*βm* = is-weak-cartesian (weak-β f*-weak-cartesian m*-weak-cartesian)   f*-cartesian : is-cartesian f f* f*-cartesian .universal {u = u} {u' = u'} m h' = hom[ idr m ] (m* β' f*βm*.universal h') where open Morphisms m h'  Showing that this commutes is mostly an exercise in cubical yoga; the only real mathematical content is that the factorisation of via commutes.  f*-cartesian .commutes {u = u} {u' = u'} m h' = path where open Morphisms m h' abstract path : f* β' hom[ idr m ] (m* β' f*βm*.universal h') β‘ h' path = f* β' hom[] (m* β' f*βm*.universal h') β‘β¨ whisker-r _ β©β‘ hom[] (f* β' m* β' f*βm*.universal h') β‘β¨ assoc[] {q = idr _} β©β‘ hom[] ((f* β' m*) β' f*βm*.universal h') β‘β¨ hom[]β©β¨ from-pathpβ» (f*βm*.commutes h') β©β‘ hom[] (hom[] h') β‘β¨ hom[]-β _ _ β liberate _ β©β‘ h' β  Uniqueness follows similarly as some cubical yoga, followed by the fact that both and are weak cartesian maps.  f*-cartesian .unique {u = u} {u' = u'} {m = m} {h' = h'} m' p = path where open Morphisms m h' abstract universal-path : (f* β' m*) β' m*.universal m' β‘[ idr (f β m) ] h' universal-path = to-pathp$
hom[] ((f* β' m*) β' m*.universal m') β‘Λβ¨ assoc[] {p = ap (f β_) (idr m)} β©β‘Λ
hom[] (f* β' (m* β' m*.universal m')) β‘β¨ hom[]β©β¨ ap (f* β'_) (from-pathpβ» (m*.commutes m')) β©β‘
hom[] (f* β' hom[] m')                β‘β¨ smashr _ _ β liberate _ β©β‘
f* β' m'                              β‘β¨ p β©β‘
h' β

path : m' β‘ hom[ idr m ] (m* β' f*βm*.universal h')
path =
m'                               β‘Λβ¨ from-pathp (m*.commutes m') β©β‘Λ
hom[] (m* β' m*.universal m')    β‘β¨ reindex _ (idr m) β©β‘
hom[] (m* β' m*.universal m')    β‘β¨ hom[]β©β¨ ap (m* β'_) (f*βm*.unique _ universal-path) β©β‘
hom[] (m* β' f*βm*.universal h') β


Putting this all together, we can finally deduce that is a cartesian lift of

    f-lift : Cartesian-lift f y'
f-lift .Cartesian-lift.x' = x*
f-lift .Cartesian-lift.lifting = f*
f-lift .Cartesian-lift.cartesian = f*-cartesian


Factorisations in weak fibrationsπ

If is a weak fibration, then every morphism factorizes into a vertical morphism followed by a weak cartesian morphism.

record weak-cartesian-factorisation
{x y x' y'} {f : Hom x y}
(f' : Hom[ f ] x' y')
: Type (o β β β o' β β')
where
no-eta-equality
field
{x''} : Ob[ x ]
vertical : Hom[ id ] x' x''
weak-cart : Hom[ f ] x'' y'
has-weak-cartesian : is-weak-cartesian f weak-cart
factors : f' β‘[ sym (idr _) ] weak-cart β' vertical

weak-fibrationβweak-cartesian-factors
: β {x y x' y'} {f : Hom x y}
β is-weak-cartesian-fibration
β (f' : Hom[ f ] x' y')
β weak-cartesian-factorisation f'


Because is a weak fibration, every morphism in has a weak cartesian lift. This allows us to take the lift of which will form the weak cartesian component of the factorisation. The vertical component can be obtained by taking the universal factorisation of by the lift of

weak-fibrationβweak-cartesian-factors {y' = y'} {f = f} wfib f' = weak-factor where
open is-weak-cartesian-fibration wfib
module f-lift = weak-lift f y'
open weak-cartesian-factorisation

weak-factor : weak-cartesian-factorisation f'
weak-factor .x'' = f-lift.x'
weak-factor .vertical = f-lift.universal f'
weak-factor .weak-cart = f-lift.lifting
weak-factor .has-weak-cartesian = f-lift.weak-cartesian
weak-factor .factors = symP $f-lift.commutes f'  Weak fibrations and equivalence of Hom setsπ If is a weak fibration, then the hom sets and are equivalent, where is the domain of the lift of along To go from to we use the vertical component of the factorisation of this forms an equivalence, as this factorisation is unique. module _ (wfib : is-weak-cartesian-fibration) where open is-weak-cartesian-fibration wfib weak-fibrationβuniversal-is-equiv : β {x y x' y'} β (f : Hom x y) β is-equiv (weak-lift.universal f y' {x'}) weak-fibrationβuniversal-is-equiv {y' = y'} f = is-isoβis-equiv$
iso (Ξ» f' β hom[ idr f ] (weak-lift.lifting f y' β' f') )
(Ξ» f' β sym $weak-lift.unique f y' f' (to-pathp refl)) (Ξ» f' β cancel _ _ (weak-lift.commutes f y' f')) weak-fibrationβvertical-equiv : β {x y x' y'} β (f : Hom x y) β Hom[ f ] x' y' β Hom[ id ] x' (weak-lift.x' f y') weak-fibrationβvertical-equiv {y' = y'} f = weak-lift.universal f y' , weak-fibrationβuniversal-is-equiv f  Furthermore, this equivalence can be extended into a natural isomorphism between and  weak-fibrationβhom-iso-into : β {x y y'} (u : Hom x y) β Hom-over-into β° u y' β βΏ Hom-into (Fibre β° x) (weak-lift.x' u y') weak-fibrationβhom-iso-into {x} {y} {y'} u = to-natural-iso mi where open make-natural-iso u*y' : Ob[ x ] u*y' = weak-lift.x' u y' mi : make-natural-iso (Hom-over-into β° u y') (Hom-into (Fibre β° x) u*y') mi .eta x u' = weak-lift.universal u y' u' mi .inv x v' = hom[ idr u ] (weak-lift.lifting u y' β' v') mi .etaβinv x = funext Ξ» v' β sym$ weak-lift.unique u _ _ (to-pathp refl)
mi .invβeta x = funext Ξ» u' β
from-pathp (weak-lift.commutes u _ _)
mi .natural x y v' = funext Ξ» u' β
weak-lift.unique u _ _ $to-pathp$
smashr _ _
β weave _ (ap (u β_) (idl id)) _ (pulll' _ (weak-lift.commutes _ _ _))


An extremely useful fact is that the converse is true: if there is some lifting of objects for every morphism in along with a natural equivalence of homs as above, then is a weak fibration.

This result is the primary reason to care about weak fibrations, as we already have a toolkit for constructing natural equivalences of hom sets! Most notably, this allows us to use the theory of adjuncts to construct weak fibrations.

module _ (_*β_ : β {x y} β Hom x y β Ob[ y ] β Ob[ x ]) where
open is-weak-cartesian-fibration
open Weak-cartesian-lift
open is-weak-cartesian

private
vertical-equiv-iso-natural
: (β {x y x' y'} {f : Hom x y} β Hom[ f ] x' y' β Hom[ id ] x' (f *β y'))
β Type _
vertical-equiv-iso-natural to =
β {x y x' x'' y'} {f : Hom x y}
β (f' : Hom[ f ] x'' y') (g' : Hom[ id ] x' x'')
β to (hom[ idr _ ] (f' β' g')) β‘[ sym (idl id) ] to f' β' g'

vertical-equivβweak-fibration
: (to* : β {x y x' y'} {f : Hom x y} β Hom[ f ] x' y' β Hom[ id ] x' (f *β y'))
β (β {x y x' y'} {f : Hom x y} β is-equiv (to* {x} {y} {x'} {y'} {f}))
β vertical-equiv-iso-natural to*
β is-weak-cartesian-fibration
vertical-equivβweak-fibration to* to-eqv natural .weak-lift f y' = f-lift where


To start, we note that the inverse portion of the equivalence is also natural.

    from* : β {x y x' y'} {f : Hom x y} β Hom[ id ] x' (f *β y') β Hom[ f ] x' y'
from* = equivβinverse to-eqv

from*-natural
: β {x y} {f : Hom x y} {x' x'' : Ob[ x ]} {y' : Ob[ y ]}
β (f' : Hom[ id ] x'' (f *β y')) (g' : Hom[ id ] x' x'')
β from* (hom[ idl id ] (f' β' g')) β‘[ sym (idr f) ] from* f' β' g'
from*-natural {f = f} f' g' =
to-pathpβ» $ap fst$ is-contrβis-prop (to-eqv .is-eqv (hom[ idl id ] (f' β' g')))
(from* (hom[ idl id ] (f' β' g')) , equivβcounit to-eqv _)
(hom[ idr f ] (from* f' β' g') , from-pathpβ» (natural (from* f') g') β
(hom[]β©β¨ ap (_β' g') (equivβcounit to-eqv _)))


We then proceed to construct a weak lift of We can use our object lifting function to construct the domain of the lift, apply the inverse direction of the equivalence to to obtain the required lifting

    f-lift : Weak-cartesian-lift f y'
f-lift .x' = f *β y'
f-lift .lifting = from* id'


Now, we must show that the constructed lifting is weakly cartesian. We can use the forward direction of the equivalence to construct the universal map; the remaining properties follow from the fact that the equivalence is natural.

    f-lift .weak-cartesian .universal g' = to* g'
f-lift .weak-cartesian .commutes g' = to-pathp $hom[] (from* id' β' to* g') β‘Λβ¨ from-pathpβ» (from*-natural id' (to* g')) β© from* (hom[] (id' β' to* g')) β‘β¨ ap from* idl[] β© from* (to* g') β‘β¨ equivβunit to-eqv g' β© g' β f-lift .weak-cartesian .unique {g' = g'} h' p = h' β‘Λβ¨ idl[] {p = idl id} β© hom[] (id' β' h') β‘Λβ¨ hom[]β©β¨ ap (_β' h') (equivβcounit to-eqv id') β© hom[] (to* (from* id') β' h') β‘Λβ¨ from-pathpβ» (natural (from* id') h') β© to* (hom[] (from* id' β' h')) β‘β¨ ap to* (from-pathp p) β© to* g' β  module _ (U : β {x y} β Hom x y β Functor (Fibre β° y) (Fibre β° x)) where open Functor open _=>_ hom-isoβweak-fibration : (β {x y y'} (u : Hom x y) β Hom-over-into β° u y' β βΏ Hom-into (Fibre β° x) (U u .Fβ y')) β is-weak-cartesian-fibration hom-isoβweak-fibration hom-iso = vertical-equivβweak-fibration (Ξ» u β U u .Fβ) (Ξ» u' β IsoβΏ.to (hom-iso _) .Ξ· _ u') (natural-iso-to-is-equiv (hom-iso _) _) Ξ» f' g' β to-pathpβ»$
happly (IsoβΏ.to (hom-iso _) .is-natural _ _ g') f'


Note that this result does not extend to fibrations; the equivalence of homs can only get us weak cartesian lifts. To make the final step to a fibration, we need to use other means.

However, we do obtain a natural isomorphism between and

module _ (fib : Cartesian-fibration) where
open Cartesian-fibration fib
open Indexing β° fib

fibrationβhom-iso-from
: β {x y x'} (u : Hom x y)
β Hom-over-from β° u x' ββΏ Hom-from (Fibre β° x) x' Fβ base-change u
fibrationβhom-iso-from {x} {y} {x'} u = to-natural-iso mi where
open make-natural-iso

mi : make-natural-iso
(Hom-over-from β° u x')
(Hom-from (Fibre β° x) x' Fβ base-change u)
mi .eta x u' = has-lift.universalv u x u'
mi .inv x v' = hom[ idr u ] (has-lift.lifting u x β' v')
mi .etaβinv x = funext Ξ» v' β
sym $has-lift.uniquev u _ _ (to-pathp refl) mi .invβeta x = funext Ξ» u' β from-pathp (has-lift.commutesv u _ _) mi .natural _ _ v' = funext Ξ» u' β has-lift.uniquep u _ _ _ _ _$
Fib.pulllf (has-lift.commutesp u _ id-comm _)
β[] pullr[] _ (has-lift.commutesv u _ _)
β[] to-pathp refl

  fibrationβuniversal-is-equiv
: β {x y x' y'}
β (f : Hom x y)
β is-equiv (has-lift.universalv f y' {x'})
fibrationβuniversal-is-equiv f =
weak-fibrationβuniversal-is-equiv (fibrationβweak-fibration fib) f

fibrationβvertical-equiv
: β {x y x' y'}
β (f : Hom x y)
β Hom[ f ] x' y' β Hom[ id ] x' (has-lift.x' f y')
fibrationβvertical-equiv f =
weak-fibrationβvertical-equiv (fibrationβweak-fibration fib) f

fibrationβhom-iso-into
: β {x y y'} (u : Hom x y)
β Hom-over-into β° u y' ββΏ Hom-into (Fibre β° x) (has-lift.x' u y')
fibrationβhom-iso-into u =
weak-fibrationβhom-iso-into (fibrationβweak-fibration fib) u


If we combine this with weak-fibrationβhom-iso-into, we obtain a natural iso between and

  fibrationβhom-iso
: β {x y} (u : Hom x y)
β Hom-over β° u ββΏ Hom[-,-] (Fibre β° x) Fβ (Id FΓ base-change u)
fibrationβhom-iso {x = x} u = to-natural-iso mi where
open make-natural-iso
open _=>_

module into-iso {y'} = IsoβΏ (fibrationβhom-iso-into {y' = y'} u)
module from-iso {x'} = IsoβΏ (fibrationβhom-iso-from {x' = x'} u)

mi : make-natural-iso (Hom-over β° u) (Hom[-,-] (Fibre β° x) Fβ (Id FΓ base-change u))
mi .eta x u' = has-lift.universalv u _ u'
mi .inv x v' = hom[ idr u ] (has-lift.lifting u _ β' v')
mi .etaβinv x = funext Ξ» v' β
sym \$ has-lift.uniquev u _ _ (to-pathp refl)
mi .invβeta x = funext Ξ» u' β
from-pathp (has-lift.commutesv u _ _)
mi .natural _ _ (vβ' , vβ') = funext Ξ» u' β
sym (apr' (happly (into-iso.to .is-natural _ _ vβ') u'))
Β·Β· sym (happly (from-iso.to .is-natural _ _ vβ') (hom[ idr _ ] (u' β' vβ')))
Β·Β· ap (into-iso.to .Ξ· _) (smashr _ _ β reindex _ _ )