KanContractedFamilyLifting.lean`

48 declarations, 0 contain sorry, 0 declared as axioms

Stationary contractions and Kan fibres over finite cubes

def OAI.Thomason.Construction.RealizedCube.finalVertex line 23
Source documentation
The final vertex in every coordinate of the finite simplicial cube.
```
def finalVertex : (n : ℕ) → (obj n) _⦋0⦌
  | 0 => finalSimplexVertex 0
  | n+1 => (finalVertex n, finalSimplexVertex 1)

/-- Simultaneously contract all interval coordinates to their final vertex. -/
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.finalSimplexVertex, OAI.Thomason.Construction.RealizedCube.coordinates
def OAI.Thomason.Construction.RealizedCube.finalContractionMap line 28
Source documentation
Simultaneously contract all interval coordinates to their final vertex.
```
def finalContractionMap (n : ℕ) : obj n ⊗ (Δ[1] : SSet.{0}) ⟶ obj n :=
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj
theorem OAI.Thomason.Construction.RealizedCube.finalContractionMap_zero line 43
theorem OAI.Thomason.Construction.RealizedCube.finalContractionMap_one line 57
def OAI.Thomason.Construction.RealizedCube.finalContraction line 81
Source documentation
The simultaneous contraction is an actual simplicial homotopy.
```
def finalContraction (n : ℕ) : SSet.Homotopy (𝟙 (obj n)) (SSet.const (finalVertex n)) where
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.RealizedCube.finalVertex
theorem OAI.Thomason.Construction.RealizedCube.finalContraction_stationary line 93
Source documentation
The entire constant family at the final vertex stays fixed.
```
theorem finalContraction_stationary (n : ℕ) (K : SSet.{0}) :
    (SSet.const (X := K) (finalVertex n)) ▷ Δ[1] ≫ (finalContraction n).h =
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.finalVertex, OAI.Thomason.Construction.RealizedCube.finalContraction

theorem OAI.Thomason.Construction.RealizedCube.kan_final_fiber_deformation line 119

Source documentation

Every Kan fibration over a finite simplicial cube retracts, by a stationary simplicial homotopy, onto its final-vertex fibre.

theorem kan_final_fiber_deformation {E : SSet.{0}} (n : ℕ)
    (p : E ⟶ obj n) [HomotopicalAlgebra.Fibration p] :
    ∃ r : E ⟶ (simplicialPointFiber p (finalVertex n)).toSSet,
      (simplicialPointFiber p (finalVertex n)).ι ≫ r = 𝟙 _ ∧
      ∃ T : SSet.Homotopy (𝟙 E) (r ≫ (simplicialPointFiber p (finalVertex n)).ι),
        (simplicialPointFiber p (finalVertex n)).ι ▷ Δ[1] ≫ T.h =
          fst (simplicialPointFiber p (finalVertex n)).toSSet Δ[1] ≫
            (simplicialPointFiber p (finalVertex n)).ι ∧
        T.h ≫ p = p ▷ Δ[1] ≫ (finalContraction n).h := by
…

Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.simplicialPointFiber, OAI.Thomason.Construction.RealizedCube.finalVertex, OAI.Thomason.Construction.RealizedCube.finalContraction

theorem OAI.Thomason.Construction.RealizedCube.kan_final_fiber_weak line 133
Source documentation
The final fibre includes by an actual realization weak equivalence.
```
theorem kan_final_fiber_weak {E : SSet.{0}} (n : ℕ)
    (p : E ⟶ obj n) [HomotopicalAlgebra.Fibration p] :
    realizationWeakEquivalences (simplicialPointFiber p (finalVertex n)).ι := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.simplicialPointFiber, OAI.Thomason.Construction.RealizedCube.finalVertex
theorem OAI.Thomason.Construction.RealizedCube.kan_any_fiber_weak line 142
Source documentation
Every vertex fibre of a Kan fibration over a cube includes weakly. The already proved realization component comparison transports the final fibre result to all vertices, without a global fibre-preservation premise.
```
theorem kan_any_fiber_weak {E : SSet.{0}} (n : ℕ)
    (p : E ⟶ obj n) [HomotopicalAlgebra.Fibration p] (b : (obj n) _⦋0⦌) :
    realizationWeakEquivalences (simplicialPointFiber p b).ι := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.simplicialPointFiber
theorem OAI.Thomason.Construction.simplexFinalContraction_initial line 180
Source documentation
The final contraction on the interval, started at zero, is the original interval parameter, in every simplicial degree.
```
theorem simplexFinalContraction_initial (K : SSet.{0}) :
    (SSet.const (X := K) (initialSimplexVertex 1)) ▷ Δ[1] ≫
…
```
Mentions: OAI.Thomason.Construction.initialSimplexVertex

theorem OAI.Thomason.Construction.kan_interval_fiber_transport line 199

Source documentation

A Kan fibration transports its initial fibre to its final fibre along any base edge by an actual simplicial weak equivalence. The transporting homotopy projects exactly onto that edge, with the same interval parameter.

theorem kan_interval_fiber_transport {E B : SSet.{0}} (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] (g : (Δ[1] : SSet.{0}) ⟶ B) :
    ∃ t : (simplicialPointFiber p (g.app _ (initialSimplexVertex 1))).toSSet ⟶
        (simplicialPointFiber p (g.app _ (finalSimplexVertex 1))).toSSet,
      realizationWeakEquivalences t ∧
      ∃ H : SSet.Homotopy (simplicialPointFiber p (g.app _ (initialSimplexVertex 1))).ι
          (t ≫ (simplicialPointFiber p (g.app _ (finalSimplexVertex 1))).ι),
        H.h ≫ p = snd _ (Δ[1] : SSet.{0}) ≫ g := by
…

Mentions: OAI.Thomason.Construction.simplicialPointFiber, OAI.Thomason.Construction.initialSimplexVertex, OAI.Thomason.Construction.finalSimplexVertex, OAI.Thomason.Construction.realizationWeakEquivalences

def OAI.Thomason.Construction.kanSimplexRestriction line 276

Source documentation

The canonical restriction map on total spaces above a simplex map.

def kanSimplexRestriction {E B : SSet.{0}} (p : E ⟶ B) {n m : SimplexCategory}
    (b : SSet.stdSimplex.obj n ⟶ B) (f : m ⟶ n) :
    pullback p (SSet.stdSimplex.map f ≫ b) ⟶ pullback p b :=
…

theorem OAI.Thomason.Construction.kanSimplexRestriction_fst line 283
theorem OAI.Thomason.Construction.kanSimplexRestriction_snd line 290
theorem OAI.Thomason.Construction.kanSimplexRestriction_weak line 299
Source documentation
For an arbitrary Kan fibration, every simplex restriction is a weak homotopy equivalence on the actual realization of its pullback total spaces. Both face and degeneracy maps are included.
```
theorem kanSimplexRestriction_weak {E B : SSet.{0}} (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] {n m : SimplexCategory}
    (b : SSet.stdSimplex.obj n ⟶ B) (f : m ⟶ n) :
    realizationWeakEquivalences (kanSimplexRestriction p b f) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.kanSimplexRestriction
theorem OAI.Thomason.Construction.kan_horn_fiber_weak line 328
Source documentation
The distinguished-vertex fibre of a Kan fibration over a horn is weakly equivalent to its total space. Both homotopies fix that entire fibre.
```
theorem kan_horn_fiber_weak {E : SSet.{0}} (n : ℕ) (i : Fin (n+2))
    (p : E ⟶ (Λ[n+1, i] : SSet.{0})) [HomotopicalAlgebra.Fibration p] :
    realizationWeakEquivalences (simplicialPointFiber p (hornVertex n i)).ι :=
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.simplicialPointFiber, OAI.Thomason.Construction.hornVertex
theorem OAI.Thomason.Construction.kan_horn_baseChange_weak line 338
Source documentation
For a Kan fibration over a standard simplex, the preimage of each horn includes by an actual realization weak equivalence. This is proved directly from local fibre contractions, without acyclic-Kan lifting or right properness.
```
theorem kan_horn_baseChange_weak {E : SSet.{0}} (n : ℕ) (i : Fin (n+2))
    (p : E ⟶ (Δ[n+1] : SSet.{0})) [HomotopicalAlgebra.Fibration p] :
    realizationWeakEquivalences (pullback.fst p (Λ[n+1, i] : SSet.Subcomplex _).ι) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.kan_simplex_horn_restriction_weak line 354

Source documentation

The same comparison in a general base, restricted over a chosen simplex. The actual iterated pullback is retained in the statement.

theorem kan_simplex_horn_restriction_weak {E B : SSet.{0}} (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] (n : ℕ) (i : Fin (n+2))
    (b : (Δ[n+1] : SSet.{0}) ⟶ B) :
    realizationWeakEquivalences
      (pullback.fst (pullback.snd p b) (Λ[n+1, i] : SSet.Subcomplex _).ι) := by
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

def OAI.Thomason.Construction.simplexPullbackMap line 379
theorem OAI.Thomason.Construction.simplexPullbackMap_fst line 387
theorem OAI.Thomason.Construction.simplexPullbackMap_snd line 394
theorem OAI.Thomason.Construction.simplexPullbackMap_weak line 400
abbrev OAI.Thomason.Construction.simplexPullbackDiagram line 416
Source documentation
Pull back the original fibration along every simplex of its base, including degenerate simplices and every ordinal map between them.
```
abbrev simplexPullbackDiagram {E B : SSet.{0}} (p : E ⟶ B) :
    CostructuredArrow SSet.stdSimplex B ⥤ SSet.{0} where
…
```
def OAI.Thomason.Construction.simplexPullbackCocone line 435
Source documentation
The canonical cocone is compatible with the original total space.
```
def simplexPullbackCocone {E B : SSet.{0}} (p : E ⟶ B) :
    Cocone (simplexPullbackDiagram p) where
…
```
Mentions: OAI.Thomason.Construction.simplexPullbackDiagram
theorem OAI.Thomason.Construction.simplexPullbackDiagram_map_weak line 446
Source documentation
Every arrow in this actual pullback diagram is a realization weak equivalence. No homotopy-colimit or global fibre theorem is assumed.
```
theorem simplexPullbackDiagram_map_weak {E B : SSet.{0}} (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] {s t : CostructuredArrow SSet.stdSimplex B}
    (f : s ⟶ t) : realizationWeakEquivalences ((simplexPullbackDiagram p).map f) :=
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.simplexPullbackDiagram
def OAI.Thomason.Construction.productInitialVertex line 470
Source documentation
The initial-vertex inclusion with an arbitrary simplicial parameter.
```
def productInitialVertex (K : SSet.{0}) (n : ℕ) : K ⟶ K ⊗ (Δ[n] : SSet.{0}) :=
…
```
theorem OAI.Thomason.Construction.productInitialVertex_anodyne line 474
Source documentation
The entire parameterized initial face is anodyne.
```
theorem productInitialVertex_anodyne (K : SSet.{0}) (n : ℕ) :
    SSet.anodyneExtensions (productInitialVertex K n) := by
…
```
Mentions: OAI.Thomason.Construction.productInitialVertex

theorem OAI.Thomason.Construction.kan_simplex_fibrewise_trivialization line 492

Source documentation

An actual fibrewise homotopy trivialization over a standard simplex. Both homotopies project to the constant base homotopy, and both maps retain the entire initial fibre exactly. No acyclic lifting or realization preservation of pullbacks is assumed.

theorem kan_simplex_fibrewise_trivialization {E : SSet.{0}} (n : ℕ)
    (p : E ⟶ (Δ[n] : SSet.{0})) [HomotopicalAlgebra.Fibration p] :
    ∃ (q : E ⟶ (simplicialPointFiber p (initialSimplexVertex n)).toSSet ⊗ (Δ[n] : SSet.{0}))
      (s : (simplicialPointFiber p (initialSimplexVertex n)).toSSet ⊗ (Δ[n] : SSet.{0}) ⟶ E),
      q ≫ snd _ _ = p ∧ s ≫ p = snd _ _ ∧
      (simplicialPointFiber p (initialSimplexVertex n)).ι ≫ q = productInitialVertex _ n ∧
      productInitialVertex _ n ≫ s = (simplicialPointFiber p (initialSimplexVertex n)).ι ∧
      ∃ (H : SSet.Homotopy (𝟙 E) (q ≫ s))
        (T : SSet.Homotopy (𝟙 _) (s ≫ q)),
        H.h ≫ p = fst E Δ[1] ≫ p ∧
        T.h ≫ snd _ _ = fst _ Δ[1] ≫ snd _ _ := by
…

Mentions: OAI.Thomason.Construction.simplicialPointFiber, OAI.Thomason.Construction.initialSimplexVertex, OAI.Thomason.Construction.productInitialVertex

theorem OAI.Thomason.Construction.kan_simplex_trivialization_weak line 544

Source documentation

The fibrewise trivialization maps are actual realization weak equivalences, while still commuting exactly with the base projection.

theorem kan_simplex_trivialization_weak {E : SSet.{0}} (n : ℕ)
    (p : E ⟶ (Δ[n] : SSet.{0})) [HomotopicalAlgebra.Fibration p] :
    ∃ (q : E ⟶ (simplicialPointFiber p (initialSimplexVertex n)).toSSet ⊗ (Δ[n] : SSet.{0}))
      (s : (simplicialPointFiber p (initialSimplexVertex n)).toSSet ⊗ (Δ[n] : SSet.{0}) ⟶ E),
      realizationWeakEquivalences q ∧ realizationWeakEquivalences s ∧
      q ≫ snd _ _ = p ∧ s ≫ p = snd _ _ := by
…

Mentions: OAI.Thomason.Construction.simplicialPointFiber, OAI.Thomason.Construction.initialSimplexVertex, OAI.Thomason.Construction.realizationWeakEquivalences

def OAI.Thomason.Construction.contractedVertexInclusion line 573
Source documentation
A chosen vertex as a map from the terminal standard simplex.
```
def contractedVertexInclusion {B : SSet.{0}} (b : B _⦋0⦌) : (Δ[0] : SSet.{0}) ⟶ B :=
…
```
def OAI.Thomason.Construction.productChosenVertex line 577
Source documentation
The product inclusion of that same chosen vertex.
```
def productChosenVertex {B : SSet.{0}} (K : SSet.{0}) (b : B _⦋0⦌) : K ⟶ K ⊗ B :=
…
```
theorem OAI.Thomason.Construction.contractedVertexInclusion_anodyne line 582
Source documentation
An explicit stationary reverse contraction makes the vertex inclusion anodyne by relative cylinder lifting.
```
theorem contractedVertexInclusion_anodyne {B : SSet.{0}} (b : B _⦋0⦌)
    (C : SSet.Homotopy (SSet.const b) (𝟙 B))
    (hC : ∀ K : SSet.{0}, (SSet.const (X := K) b) ▷ Δ[1] ≫ C.h =
…
```
theorem OAI.Thomason.Construction.productChosenVertex_anodyne line 613
theorem OAI.Thomason.Construction.kan_contracted_base_trivialization line 632
Source documentation
The same explicit contraction yields a fibrewise homotopy trivialization of every Kan fibration over that base. The hypotheses specify actual maps and their stationary equation, not a weak or lifting conclusion.
```
theorem kan_contracted_base_trivialization {E B : SSet.{0}} (b : B _⦋0⦌)
    (C : SSet.Homotopy (SSet.const b) (𝟙 B))
    (hC : ∀ L : SSet.{0}, (SSet.const (X := L) b) ▷ Δ[1] ≫ C.h =
…
```
def OAI.Thomason.Construction.RealizedCube.initialVertex line 700
Source documentation
The initial vertex in every coordinate of the finite simplicial cube.
```
def initialVertex : (n : ℕ) → (obj n) _⦋0⦌
  | 0 => initialSimplexVertex 0
  | n+1 => (initialVertex n, initialSimplexVertex 1)

/-- Simultaneously expand all interval coordinates from the initial vertex. -/
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.initialSimplexVertex, OAI.Thomason.Construction.RealizedCube.coordinates
def OAI.Thomason.Construction.RealizedCube.initialContractionMap line 705
Source documentation
Simultaneously expand all interval coordinates from the initial vertex.
```
def initialContractionMap (n : ℕ) : obj n ⊗ (Δ[1] : SSet.{0}) ⟶ obj n :=
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj
theorem OAI.Thomason.Construction.RealizedCube.initialContractionMap_one line 720
theorem OAI.Thomason.Construction.RealizedCube.initialContractionMap_zero line 734
def OAI.Thomason.Construction.RealizedCube.initialContraction line 758
Source documentation
The simultaneous contraction is an actual simplicial homotopy.
```
def initialContraction (n : ℕ) : SSet.Homotopy (SSet.const (initialVertex n)) (𝟙 (obj n)) where
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.initialVertex, OAI.Thomason.Construction.RealizedCube.obj
theorem OAI.Thomason.Construction.RealizedCube.initialContraction_stationary line 770
Source documentation
The entire constant family at the initial vertex stays fixed.
```
theorem initialContraction_stationary (n : ℕ) (K : SSet.{0}) :
    (SSet.const (X := K) (initialVertex n)) ▷ Δ[1] ≫ (initialContraction n).h =
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.initialVertex, OAI.Thomason.Construction.RealizedCube.initialContraction
def OAI.Thomason.Construction.productBaseChangeIso line 815
Source documentation
Pulling back a product projection gives the actual product over the new base. All maps are canonical and preserve the new base coordinate.
```
def productBaseChangeIso (F : SSet.{0}) {A B : SSet.{0}} (g : A ⟶ B) :
    pullback (snd F B) g ≅ F ⊗ A where
…
```
theorem OAI.Thomason.Construction.productBaseChangeIso_hom_snd line 831
theorem OAI.Thomason.Construction.kan_simplex_arbitrary_baseChange_product line 839
Source documentation
For a Kan fibration over a simplex, restriction along ANY simplicial map into that simplex is weakly equivalent, over its actual new base, to the product with the initial fibre. This is not a claim that arbitrary base change preserves all weak equivalences.
```
theorem kan_simplex_arbitrary_baseChange_product {E A : SSet.{0}} (n : ℕ)
    (p : E ⟶ (Δ[n] : SSet.{0})) [HomotopicalAlgebra.Fibration p]
    (g : A ⟶ (Δ[n] : SSet.{0})) :
    ∃ t : pullback p g ⟶ (simplicialPointFiber p (initialSimplexVertex n)).toSSet ⊗ A,
      realizationWeakEquivalences t ∧ t ≫ snd _ A = pullback.snd p g := by
…
```
Mentions: OAI.Thomason.Construction.simplicialPointFiber, OAI.Thomason.Construction.initialSimplexVertex, OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.whisker_initialSimplexVertex line 874
Source documentation
Whiskering the initial vertex is the actual product initial face.
```
@[reassoc] theorem whisker_initialSimplexVertex (K : SSet.{0}) (n : ℕ) :
    K ◁ initialVertexInclusion n = fst K (Δ[0] : SSet.{0}) ≫ productInitialVertex K n := by
…
```
Mentions: OAI.Thomason.Construction.initialVertexInclusion, OAI.Thomason.Construction.productInitialVertex

theorem OAI.Thomason.Construction.exists_kan_simplex_family_lift line 885

Source documentation

A Kan fibration lifts a family parameterized by an arbitrary standard simplex, retaining its initial value and its entire prescribed subfamily. This is the exact higher-parameter version of relative cylinder lifting.

theorem exists_kan_simplex_family_lift {A K E B : SSet.{0}}
    (i : A ⟶ K) [Mono i] (p : E ⟶ B) [HomotopicalAlgebra.Fibration p]
    (n : ℕ) (f : K ⟶ E) (h : A ⊗ (Δ[n] : SSet.{0}) ⟶ E)
    (b : K ⊗ (Δ[n] : SSet.{0}) ⟶ B)
    (h₀ : productInitialVertex A n ≫ h = i ≫ f)
    (hb : h ≫ p = i ▷ (Δ[n] : SSet.{0}) ≫ b)
    (hf : f ≫ p = productInitialVertex K n ≫ b) :
    ∃ e : K ⊗ (Δ[n] : SSet.{0}) ⟶ E,
      productInitialVertex K n ≫ e = f ∧
      i ▷ (Δ[n] : SSet.{0}) ≫ e = h ∧ e ≫ p = b := by
…

Mentions: OAI.Thomason.Construction.productInitialVertex

theorem OAI.Thomason.Construction.finite_kan_simplex_family_lift line 924

Source documentation

With finite source, the entire exact higher family and its two given faces live in a single finite subcomplex of the original total space.

theorem finite_kan_simplex_family_lift {A K E B : SSet.{0}} [K.Finite]
    (i : A ⟶ K) [Mono i] (p : E ⟶ B) [HomotopicalAlgebra.Fibration p]
    (n : ℕ) (f : K ⟶ E) (h : A ⊗ (Δ[n] : SSet.{0}) ⟶ E)
    (b : K ⊗ (Δ[n] : SSet.{0}) ⟶ B)
    (h₀ : productInitialVertex A n ≫ h = i ≫ f)
    (hb : h ≫ p = i ▷ (Δ[n] : SSet.{0}) ≫ b)
    (hf : f ≫ p = productInitialVertex K n ≫ b) :
    ∃ (S : E.Subcomplex) (_ : SSet.Finite S.toSSet)
      (eS : K ⊗ (Δ[n] : SSet.{0}) ⟶ S.toSSet)
      (fS : K ⟶ S.toSSet) (hS : A ⊗ (Δ[n] : SSet.{0}) ⟶ S.toSSet),
      fS ≫ S.ι = f ∧ hS ≫ S.ι = h ∧
      productInitialVertex K n ≫ eS = fS ∧
…

Mentions: OAI.Thomason.Construction.productInitialVertex

theorem OAI.Thomason.Construction.whisker_contractedVertex line 968
Source documentation
Whiskering the initial vertex is the actual product initial face.
```
@[reassoc] theorem whisker_contractedVertex (K : SSet.{0}) {P : SSet.{0}} (v : P _⦋0⦌) :
    K ◁ contractedVertexInclusion v = fst K (Δ[0] : SSet.{0}) ≫ productChosenVertex K v := by
…
```
Mentions: OAI.Thomason.Construction.contractedVertexInclusion, OAI.Thomason.Construction.productChosenVertex
theorem OAI.Thomason.Construction.exists_kan_contracted_family_lift line 979
Source documentation
A Kan fibration lifts a family parameterized by an explicitly contracted simplicial parameter, retaining its initial value and its entire prescribed subfamily. This is the exact higher-parameter version of relative cylinder lifting, including finite cube parameters.
```
theorem exists_kan_contracted_family_lift {A K E B : SSet.{0}}
    (i : A ⟶ K) [Mono i] (p : E ⟶ B) [HomotopicalAlgebra.Fibration p]
    {P : SSet.{0}} (v : P _⦋0⦌)
    (C : SSet.Homotopy (SSet.const v) (𝟙 P))
    (hC : ∀ L : SSet.{0}, (SSet.const (X := L) v) ▷ Δ[1] ≫ C.h =
…
```