open import Cat.Functor.Hom.Displayed open import Cat.Functor.Hom.Displayed open import Cat.Instances.Functor open import Cat.Instances.Functor open import Cat.Instances.Product 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.Cartesian.Indexing as Indexing 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

# 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
$\mathcal{E}$
is a fibration, weakly cartesian morphisms are also cartesian. To see
this, we note that the lift of
$f$
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
$f'$
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*)

$f' : x' \to_{f} y'$ is a weak cartesian morphism if and only if postcomposition of $f'$ 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 $\mathcal{E}$ 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 $\mathcal{E}$ 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 $f$ has a cartesian lift, we begin by taking the weak cartesian lift $f^{*}$ of $f$.

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 $f^{*}$ 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 $m^{*}$ of $m$. Both $f^{*}$ and $m^{*}$ are weak cartesian, which means that their composite is also weak cartesian by our hypothesis. We can then factor $h'$ through $f^{*} \cdot m^{*}$ to obtain a vertical morphism $u' \to u^{*}$, which we can then compose with $m^{*}$ 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 factorization of $h'$ via $f^{*} \cdot m^{*}$ 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 $m^{*}$ and $f^{*} \cdot m^{*}$ 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 $f^{*}$ is a cartesian lift of $f$.

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 $\mathcal{E}$ 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 $\mathcal{E}$ is a weak fibration, every morphism in $\mathcal{B}$ has a weak cartesian lift. This allows us to take the lift of $f$, which will form the weak cartesian component of the factorisation. The vertical component can be obtained by taking the universal factorisation of $f'$ by the lift of $f$.

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 $\mathcal{E}$ is a weak fibration, then the hom sets $x' \to_f y'$ and $x' \to_{id} f^{*}(y')$ are equivalent, where $f^{*}(y')$ is the domain of the lift of $f$ along $y'$. To go from $f' : x' \to_u y'$ to $x' \to_{id} f^{*}(y')$, we use the vertical component of the factorisation of $f'$; 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 $\mathcal{E}_{u}(-,y')$ and $\mathcal{E}_{x}(-,u^{*}(y'))$.

weak-fibration→hom-iso-into : ∀ {x y y′} (u : Hom x y) → natural-iso (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
$\mathcal{E}_{y} \to \mathcal{E}_{x}$
for every morphism
$f : x \to y$
in
$\mathcal{B}$,
along with a natural equivalence of homs as above, then
$\mathcal{E}$
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 $f$. We can use our object lifting function to construct the domain of the lift, apply the inverse direction of the equivalence to $id' : f^{*}(y') \to f^{*}(y')$ to obtain the required lifting $x' \to_{f} f^{*}(y')$.

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′ ∎

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 $\mathcal{E}_{u}(x',-)$ and $cE_{y}(x',u^{*}(-))$.

module _ (fib : Cartesian-fibration) where open Cartesian-fibration fib open Indexing ℰ fib fibration→hom-iso-from : ∀ {x y x′} (u : Hom x y) → natural-iso (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.unique u _ _ $ to-pathp $ smashr _ _ ·· revive₁ (pulll[] _ (has-lift.commutesv u _ _)) ·· smashl _ _ ·· weave _ (pullr (idr u)) _ (pullr[] _ (has-lift.commutesv u _ _)) ·· duplicate id-comm-sym _ (idl u)

If we combine this with weak-fibration→hom-iso-into, we obtain a natural iso between $\mathcal{E}_{u}(-,-)$ and $\mathcal{E}_{id}(-,u^{*}(-))$.

fibration→hom-iso : ∀ {x y} (u : Hom x y) → natural-iso (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′} = natural-iso (fibration→hom-iso-into {y′ = y′} u) module from-iso {x′} = natural-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 _ _ )