1. Geb
  2. Prototypes
  3. LargeIR
  4. Basic
Imports
/- Copyright (c) 2026 Terence Rokop. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Terence Rokop -/ module public import Geb.Prototypes.PresheafIRUniv.Basic meta import GebMeta -- shake: keep; supplies the cite docstring role
set_option doc.verso true

Prototype: slice polynomial functors as presheaf polynomial endofunctors on the walking arrow

Throwaway exploration, not upstream-eligible content. Every declaration here is Classical.­choice-free.

A slice polynomial functor Type/X → Type/Y is given in dependent-type terms by a shape family shape : Y → Type and a direction family dir : (Σ y, shape y) → X → Type. A presheaf polynomial endofunctor on the presheaves over the walking arrow 0 ⟶ 1 — the category Fin 2 as a preorder, whose presheaves are the objects Z 1 → Z 0 of the arrow category of Type, equivalently the free coproduct completion Fam(Type) — is given by a shape presheaf and, for each shape, a direction presheaf. This module transcribes a slice polynomial functor into such an endofunctor, arrowPsh, by placing Y at level 0, the shapes Σ y, shape y at level 1, and giving every shape the constant direction presheaf X at level 0 with the slice functor's own directions at level 1, and then computes what the endofunctor does.

The computation, objEquiv, is the point of the prototype. The value of arrowPsh P at a presheaf Z is not the slice functor's value: its level 0 is Y × (X → Z 0), and its level 1 over a pair (y, f₀) is P applied to the pullback of the family Z 1 → Z 0 along f₀ : X → Z 0. The base map f₀ is free because a presheaf morphism out of a direction presheaf whose level 0 is X carries a component X → Z 0, and a polynomial functor on Fam(Type) sees the base of its argument only through such homs. So arrowPsh P is the left Kan extension of P along the inclusion of the fibre Type/X into Fam(Type), an inclusion that is faithful but not full, and the slice functor is recovered from it only along the section y ↦ (y, id): pullbackIdEquiv identifies the level-1 fibre over (y, id) at an input of base X with the slice functor's value, cmp is the resulting comparison map, map_cmp its naturality, and toLevels_objRestr_cmp that its image restricts to (y, id) along 0 ⟶ 1.

The surviving Σ (f₀ : X → Z 0) is the δ constructor of inductive-recursive codes, ⟦δ A F⟧ (U, T) = Σ (g : A → U), ⟦F (T ∘ g)⟧ (U, T) (

[DybjerSetzer2003]Peter Dybjer, Anton Setzer (2003). “Induction--recursion and initial algebras”. Annals of Pure and Applied Logic 124(1--3), pp. 1–47. https://doi.org/10.1016/S0168-0072(02)00096-9.
, and
[GhaniNordvallForsbergMalatesta2015]Neil Ghani, Fredrik Nordvall Forsberg, Lorenzo Malatesta (2015). “Positive Inductive-Recursive Definitions”. Logical Methods in Computer Science 11(1). https://doi.org/10.2168/LMCS-11(1:13)2015.
for its functorial reading on Fam(C)): read with X the arity and Z 0 the universe, the transcription of a slice polynomial functor is the large-IR code whose continuation is that functor applied to the decoded family, rather than the slice functor itself.

Main definitions

  • arrowSlice — the slice polynomial functor on the objects of the walking arrow underlying the transcription: shapes Y ⊕ P.A, directions X ⊕ fibDir P s.

  • arrowPsh — the presheaf polynomial endofunctor, with the restriction and reindexing maps and their laws.

  • pullbackAlong — the pullback of the family Z 1 → Z 0 along a map X → Z 0, as an object of Type/X.

  • Levels — the value of the transcription computed in dependent-type terms: level 0 is Y × (X → Z 0), level 1 is the sum over f₀ : X → Z 0 of P at the pullback along f₀.

  • objEquiv — the equivalence of (arrowPsh P).obj Z with Levels P Z, through toLevels and ofLevels.

  • ofSlice — an object p : E → X of Type/X as a walking-arrow presheaf; ofSliceHom a morphism over X as a natural transformation.

  • pullbackIdEquiv — the pullback along the identity is the object itself, at the level of the slice functor's values.

  • cmp — the comparison map from the slice functor's value to the transcription's value at ofSlice p: the level-1 element over (y, id).

Main statements

  • isNatural_iff — over the walking arrow, naturality of a direction assignment is its equation along the one non-identity morphism.

  • toLevels_objRestr — restricting a level-1 element over (y, f₀) along 0 ⟶ 1 gives the level-0 element (y, f₀), with y the slice functor's output index.

  • map_cmp — the comparison map is natural in the object of Type/X.

  • toLevels_objRestr_cmp — the comparison map's image restricts to (y, id).

References

Tags

prototype, presheaf, walking arrow, parametric right adjoint, slice polynomial functor, inductive-recursive, free coproduct completion

@[expose] public sectionopen CategoryTheory PresheafIRUnivnamespace GebProto.LargeIRvariable {X Y : Type}

The endofunctor

The level-1 directions of a shape: none for a level-0 shape y, the slice functor's directions for a level-1 shape a.

def fibDir (P : SlicePFunctor.{0, 0, 0, 0} X Y) : Y ⊕ P.A → Type | .inl _ => PEmpty | .inr a => P.B a

The input index in X of a level-1 direction: the slice functor's direction-input map.

def fibR (P : SlicePFunctor.{0, 0, 0, 0} X Y) : (Σ s : Y ⊕ P.A, fibDir P s) → X | ⟨.inl _, e⟩ => PEmpty.elim e | ⟨.inr a, b⟩ => P.r ⟨a, b⟩

The slice polynomial functor on the objects of the walking arrow underlying the transcription: the level-0 shapes are Y, the level-1 shapes are P.A, every shape has the directions X at level 0, and a level-1 shape additionally has the slice functor's directions at level 1.

def arrowSlice (P : SlicePFunctor.{0, 0, 0, 0} X Y) : SlicePFunctor.{0, 0, 0, 0} (Fin 2) (Fin 2) where toPFunctor := ⟨Y ⊕ P.A, fun s ↦ X ⊕ fibDir P s⟩ r := fun d ↦ Sum.elim (fun _ ↦ 0) (fun _ ↦ 1) d.2 q := Sum.elim (fun _ ↦ 0) (fun _ ↦ 1)

The direction restriction to a target index t: a level-0 direction is fixed, and a level-1 direction restricted to level 0 is its input index in X.

def restrDir (P : SlicePFunctor.{0, 0, 0, 0} X Y) (s : Y ⊕ P.A) (t : Fin 2) : X ⊕ fibDir P s → X ⊕ fibDir P s | .inl x => .inl x | .inr b => match t with | 0 => .inl (fibR P ⟨s, b⟩) | 1 => .inr b

The restricted direction lies over the target index.

theorem restrDir_over (P : SlicePFunctor.{0, 0, 0, 0} X Y) (s : Y ⊕ P.A) (t : Fin 2) (d : X ⊕ fibDir P s) {i : Fin 2} (hd : (arrowSlice P).r ⟨s, d⟩ = i) (ht : t ≤ i) : (arrowSlice P).r ⟨s, restrDir P s t d⟩ = t := X:TypeY:TypeP:SlicePFunctor X Ys:Y ⊕ P.At:Fin 2d:X ⊕ fibDir P si:Fin 2hd:(arrowSlice P).r ⟨s, d⟩ = iht:t ≤ i⊢ (arrowSlice P).r ⟨s, restrDir P s t d⟩ = t X:TypeY:TypeP:SlicePFunctor X Ys:Y ⊕ P.At:Fin 2d:X ⊕ fibDir P sht:t ≤ (arrowSlice P).r ⟨s, d⟩⊢ (arrowSlice P).r ⟨s, restrDir P s t d⟩ = t match d, t with X:TypeY:TypeP:SlicePFunctor X Ys:Y ⊕ P.At:Fin 2d:X ⊕ fibDir P sval✝:Xht:0 ≤ (arrowSlice P).r ⟨s, Sum.inl val✝⟩⊢ (arrowSlice P).r ⟨s, restrDir P s 0 (Sum.inl val✝)⟩ = 0 All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Ys:Y ⊕ P.At:Fin 2d:X ⊕ fibDir P sval✝:Xht:1 ≤ (arrowSlice P).r ⟨s, Sum.inl val✝⟩⊢ (arrowSlice P).r ⟨s, restrDir P s 1 (Sum.inl val✝)⟩ = 1 exact absurd ht (X:TypeY:TypeP:SlicePFunctor X Ys:Y ⊕ P.At:Fin 2d:X ⊕ fibDir P sval✝:Xht:1 ≤ (arrowSlice P).r ⟨s, Sum.inl val✝⟩⊢ ¬1 ≤ (arrowSlice P).r ⟨s, Sum.inl val✝⟩ X:TypeY:TypeP:SlicePFunctor X Ys:Y ⊕ P.At:Fin 2d:X ⊕ fibDir P sval✝:Xht:1 ≤ (arrowSlice P).r ⟨s, Sum.inl val✝⟩⊢ ¬1 ≤ 0; All goals completed! 🐙) X:TypeY:TypeP:SlicePFunctor X Ys:Y ⊕ P.At:Fin 2d:X ⊕ fibDir P sval✝:fibDir P sht:0 ≤ (arrowSlice P).r ⟨s, Sum.inr val✝⟩⊢ (arrowSlice P).r ⟨s, restrDir P s 0 (Sum.inr val✝)⟩ = 0 All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Ys:Y ⊕ P.At:Fin 2d:X ⊕ fibDir P sval✝:fibDir P sht:1 ≤ (arrowSlice P).r ⟨s, Sum.inr val✝⟩⊢ (arrowSlice P).r ⟨s, restrDir P s 1 (Sum.inr val✝)⟩ = 1 All goals completed! 🐙

The shape restriction to a target index t: a level-0 shape is fixed, and a level-1 shape restricted to level 0 is its output index in Y.

def restrShape (P : SlicePFunctor.{0, 0, 0, 0} X Y) (t : Fin 2) : Y ⊕ P.A → Y ⊕ P.A | .inl y => .inl y | .inr a => match t with | 0 => .inl (P.q a) | 1 => .inr a

The restricted shape lies over the target index.

theorem restrShape_over (P : SlicePFunctor.{0, 0, 0, 0} X Y) (t : Fin 2) (s : Y ⊕ P.A) {j : Fin 2} (hs : (arrowSlice P).q s = j) (ht : t ≤ j) : (arrowSlice P).q (restrShape P t s) = t := X:TypeY:TypeP:SlicePFunctor X Yt:Fin 2s:Y ⊕ P.Aj:Fin 2hs:(arrowSlice P).q s = jht:t ≤ j⊢ (arrowSlice P).q (restrShape P t s) = t X:TypeY:TypeP:SlicePFunctor X Yt:Fin 2s:Y ⊕ P.Aht:t ≤ (arrowSlice P).q s⊢ (arrowSlice P).q (restrShape P t s) = t match s, t with X:TypeY:TypeP:SlicePFunctor X Yt:Fin 2s:Y ⊕ P.Aval✝:Yht:0 ≤ (arrowSlice P).q (Sum.inl val✝)⊢ (arrowSlice P).q (restrShape P 0 (Sum.inl val✝)) = 0 All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Yt:Fin 2s:Y ⊕ P.Aval✝:Yht:1 ≤ (arrowSlice P).q (Sum.inl val✝)⊢ (arrowSlice P).q (restrShape P 1 (Sum.inl val✝)) = 1 exact absurd ht (X:TypeY:TypeP:SlicePFunctor X Yt:Fin 2s:Y ⊕ P.Aval✝:Yht:1 ≤ (arrowSlice P).q (Sum.inl val✝)⊢ ¬1 ≤ (arrowSlice P).q (Sum.inl val✝) X:TypeY:TypeP:SlicePFunctor X Yt:Fin 2s:Y ⊕ P.Aval✝:Yht:1 ≤ (arrowSlice P).q (Sum.inl val✝)⊢ ¬1 ≤ 0; All goals completed! 🐙) X:TypeY:TypeP:SlicePFunctor X Yt:Fin 2s:Y ⊕ P.Aval✝:P.Aht:0 ≤ (arrowSlice P).q (Sum.inr val✝)⊢ (arrowSlice P).q (restrShape P 0 (Sum.inr val✝)) = 0 All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Yt:Fin 2s:Y ⊕ P.Aval✝:P.Aht:1 ≤ (arrowSlice P).q (Sum.inr val✝)⊢ (arrowSlice P).q (restrShape P 1 (Sum.inr val✝)) = 1 All goals completed! 🐙

The reindexing of level-1 directions along a shape restriction: the identity where the restricted shape has any.

def reindexFib (P : SlicePFunctor.{0, 0, 0, 0} X Y) : (s : Y ⊕ P.A) → (t : Fin 2) → fibDir P (restrShape P t s) → fibDir P s | .inl _, _, e => e | .inr _, 0, e => PEmpty.elim e | .inr _, 1, b => b

The reindexing of directions along a shape restriction: the identity on level-0 directions, reindexFib on level-1 ones.

def reindexDir (P : SlicePFunctor.{0, 0, 0, 0} X Y) (s : Y ⊕ P.A) (t : Fin 2) : X ⊕ fibDir P (restrShape P t s) → X ⊕ fibDir P s | .inl x => .inl x | .inr b => .inr (reindexFib P s t b)

Reindexing preserves the level of a direction.

theorem reindexDir_over (P : SlicePFunctor.{0, 0, 0, 0} X Y) (s : Y ⊕ P.A) (t : Fin 2) (d : X ⊕ fibDir P (restrShape P t s)) : (arrowSlice P).r ⟨s, reindexDir P s t d⟩ = (arrowSlice P).r ⟨restrShape P t s, d⟩ := X:TypeY:TypeP:SlicePFunctor X Ys:Y ⊕ P.At:Fin 2d:X ⊕ fibDir P (restrShape P t s)⊢ (arrowSlice P).r ⟨s, reindexDir P s t d⟩ = (arrowSlice P).r ⟨restrShape P t s, d⟩ X:TypeY:TypeP:SlicePFunctor X Ys:Y ⊕ P.At:Fin 2val✝:X⊢ (arrowSlice P).r ⟨s, reindexDir P s t (Sum.inl val✝)⟩ = (arrowSlice P).r ⟨restrShape P t s, Sum.inl val✝⟩X:TypeY:TypeP:SlicePFunctor X Ys:Y ⊕ P.At:Fin 2val✝:fibDir P (restrShape P t s)⊢ (arrowSlice P).r ⟨s, reindexDir P s t (Sum.inr val✝)⟩ = (arrowSlice P).r ⟨restrShape P t s, Sum.inr val✝⟩ X:TypeY:TypeP:SlicePFunctor X Ys:Y ⊕ P.At:Fin 2val✝:X⊢ (arrowSlice P).r ⟨s, reindexDir P s t (Sum.inl val✝)⟩ = (arrowSlice P).r ⟨restrShape P t s, Sum.inl val✝⟩X:TypeY:TypeP:SlicePFunctor X Ys:Y ⊕ P.At:Fin 2val✝:fibDir P (restrShape P t s)⊢ (arrowSlice P).r ⟨s, reindexDir P s t (Sum.inr val✝)⟩ = (arrowSlice P).r ⟨restrShape P t s, Sum.inr val✝⟩ All goals completed! 🐙

Reindexing preserves the input index of a level-1 direction.

theorem fibR_reindexFib (P : SlicePFunctor.{0, 0, 0, 0} X Y) (s : Y ⊕ P.A) (t : Fin 2) (b : fibDir P (restrShape P t s)) : fibR P ⟨s, reindexFib P s t b⟩ = fibR P ⟨restrShape P t s, b⟩ := X:TypeY:TypeP:SlicePFunctor X Ys:Y ⊕ P.At:Fin 2b:fibDir P (restrShape P t s)⊢ fibR P ⟨s, reindexFib P s t b⟩ = fibR P ⟨restrShape P t s, b⟩ match s, t, b with X:TypeY:TypeP:SlicePFunctor X Ys:Y ⊕ P.At:Fin 2b:fibDir P (restrShape P t s)val✝:Yx✝:Fin 2e:fibDir P (restrShape P x✝ (Sum.inl val✝))⊢ fibR P ⟨Sum.inl val✝, reindexFib P (Sum.inl val✝) x✝ e⟩ = fibR P ⟨restrShape P x✝ (Sum.inl val✝), e⟩ All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Ys:Y ⊕ P.At:Fin 2b:fibDir P (restrShape P t s)val✝:P.Ae:fibDir P (restrShape P 0 (Sum.inr val✝))⊢ fibR P ⟨Sum.inr val✝, reindexFib P (Sum.inr val✝) 0 e⟩ = fibR P ⟨restrShape P 0 (Sum.inr val✝), e⟩ All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Ys:Y ⊕ P.At:Fin 2b:fibDir P (restrShape P t s)val✝:P.Ax✝:fibDir P (restrShape P 1 (Sum.inr val✝))⊢ fibR P ⟨Sum.inr val✝, reindexFib P (Sum.inr val✝) 1 x✝⟩ = fibR P ⟨restrShape P 1 (Sum.inr val✝), x✝⟩ All goals completed! 🐙

The direction restriction along a walking-arrow morphism.

def directionRestr (P : SlicePFunctor.{0, 0, 0, 0} X Y) (s : Y ⊕ P.A) ⦃i i' : Fin 2⦄ (f : i' ⟶ i) (d : (arrowSlice P).Direction s i) : (arrowSlice P).Direction s i' := ⟨restrDir P s i' d.1, restrDir_over P s i' d.1 d.2 (leOfHom f)⟩

The shape restriction along a walking-arrow morphism.

def shapeRestr (P : SlicePFunctor.{0, 0, 0, 0} X Y) ⦃j j' : Fin 2⦄ (g : j' ⟶ j) (s : (arrowSlice P).Shape j) : (arrowSlice P).Shape j' := ⟨restrShape P j' s.1, restrShape_over P j' s.1 s.2 (leOfHom g)⟩

The reindexing of directions along a walking-arrow morphism.

def reindex (P : SlicePFunctor.{0, 0, 0, 0} X Y) ⦃j j' : Fin 2⦄ (g : j' ⟶ j) (s : (arrowSlice P).Shape j) ⦃i : Fin 2⦄ (d : (arrowSlice P).Direction (shapeRestr P g s).1 i) : (arrowSlice P).Direction s.1 i := ⟨reindexDir P s.1 j' d.1, (reindexDir_over P s.1 j' d.1).trans d.2⟩

The operations of the transcription.

def arrowData (P : SlicePFunctor.{0, 0, 0, 0} X Y) : PresheafPFunctorData.{0, 0, 0, 0, 0, 0} (Fin 2) (Fin 2) := { arrowSlice P with directionRestr := directionRestr P shapeRestr := shapeRestr P reindex := reindex P }

Direction restriction along an identity is the identity.

theorem directionRestr_id (P : SlicePFunctor.{0, 0, 0, 0} X Y) : (arrowData P).DirectionRestrId := X:TypeY:TypeP:SlicePFunctor X Y⊢ (arrowData P).DirectionRestrId X:TypeY:TypeP:SlicePFunctor X Ys:(arrowData P).Ai:Fin 2⊢ (arrowData P).directionRestr s (𝟙 i) = id X:TypeY:TypeP:SlicePFunctor X Ys:(arrowData P).Ai:Fin 2d:(arrowData P).Direction s i⊢ (arrowData P).directionRestr s (𝟙 i) d = id d X:TypeY:TypeP:SlicePFunctor X Ys:(arrowData P).Ai:Fin 2d:(arrowData P).B shd:(arrowData P).DirectionOver s i d⊢ (arrowData P).directionRestr s (𝟙 i) ⟨d, hd⟩ = id ⟨d, hd⟩ X:TypeY:TypeP:SlicePFunctor X Ys:(arrowData P).Ai:Fin 2d:(arrowData P).B shd:(arrowData P).DirectionOver s i d⊢ ↑((arrowData P).directionRestr s (𝟙 i) ⟨d, hd⟩) = ↑(id ⟨d, hd⟩) match d with X:TypeY:TypeP:SlicePFunctor X Ys:(arrowData P).Ai:Fin 2d:(arrowData P).B sval✝:Xhd:(arrowData P).DirectionOver s i (Sum.inl val✝)⊢ ↑((arrowData P).directionRestr s (𝟙 i) ⟨Sum.inl val✝, hd⟩) = ↑(id ⟨Sum.inl val✝, hd⟩) All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Ys:(arrowData P).Ai:Fin 2d:(arrowData P).B sval✝:fibDir P shd:(arrowData P).DirectionOver s i (Sum.inr val✝)⊢ ↑((arrowData P).directionRestr s (𝟙 i) ⟨Sum.inr val✝, hd⟩) = ↑(id ⟨Sum.inr val✝, hd⟩) X:TypeY:TypeP:SlicePFunctor X Ys:(arrowData P).Ai:Fin 2d:(arrowData P).B sval✝:fibDir P shd:1 = i⊢ ↑((arrowData P).directionRestr s (𝟙 i) ⟨Sum.inr val✝, hd⟩) = ↑(id ⟨Sum.inr val✝, hd⟩) X:TypeY:TypeP:SlicePFunctor X Ys:(arrowData P).Ad:(arrowData P).B sval✝:fibDir P s⊢ ↑((arrowData P).directionRestr s (𝟙 1) ⟨Sum.inr val✝, ⋯⟩) = ↑(id ⟨Sum.inr val✝, ⋯⟩) All goals completed! 🐙

Direction restriction reverses composition.

theorem directionRestr_comp (P : SlicePFunctor.{0, 0, 0, 0} X Y) : (arrowData P).DirectionRestrComp := X:TypeY:TypeP:SlicePFunctor X Y⊢ (arrowData P).DirectionRestrComp X:TypeY:TypeP:SlicePFunctor X Ys:(arrowData P).Ai:Fin 2i':Fin 2i'':Fin 2f:i' ⟶ ig:i'' ⟶ i'⊢ (arrowData P).directionRestr s (g ≫ f) = (arrowData P).directionRestr s g ∘ (arrowData P).directionRestr s f X:TypeY:TypeP:SlicePFunctor X Ys:(arrowData P).Ai:Fin 2i':Fin 2i'':Fin 2f:i' ⟶ ig:i'' ⟶ i'd:(arrowData P).Direction s i⊢ (arrowData P).directionRestr s (g ≫ f) d = ((arrowData P).directionRestr s g ∘ (arrowData P).directionRestr s f) d X:TypeY:TypeP:SlicePFunctor X Ys:(arrowData P).Ai:Fin 2i':Fin 2i'':Fin 2f:i' ⟶ ig:i'' ⟶ i'd:(arrowData P).B shd:(arrowData P).DirectionOver s i d⊢ (arrowData P).directionRestr s (g ≫ f) ⟨d, hd⟩ = ((arrowData P).directionRestr s g ∘ (arrowData P).directionRestr s f) ⟨d, hd⟩ X:TypeY:TypeP:SlicePFunctor X Ys:(arrowData P).Ai:Fin 2i':Fin 2i'':Fin 2f:i' ⟶ ig:i'' ⟶ i'd:(arrowData P).B shd:(arrowData P).DirectionOver s i d⊢ ↑((arrowData P).directionRestr s (g ≫ f) ⟨d, hd⟩) = ↑(((arrowData P).directionRestr s g ∘ (arrowData P).directionRestr s f) ⟨d, hd⟩) match d with X:TypeY:TypeP:SlicePFunctor X Ys:(arrowData P).Ai:Fin 2i':Fin 2i'':Fin 2f:i' ⟶ ig:i'' ⟶ i'd:(arrowData P).B sval✝:Xhd:(arrowData P).DirectionOver s i (Sum.inl val✝)⊢ ↑((arrowData P).directionRestr s (g ≫ f) ⟨Sum.inl val✝, hd⟩) = ↑(((arrowData P).directionRestr s g ∘ (arrowData P).directionRestr s f) ⟨Sum.inl val✝, hd⟩) All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Ys:(arrowData P).Ai:Fin 2i':Fin 2i'':Fin 2f:i' ⟶ ig:i'' ⟶ i'd:(arrowData P).B sval✝:fibDir P shd:(arrowData P).DirectionOver s i (Sum.inr val✝)⊢ ↑((arrowData P).directionRestr s (g ≫ f) ⟨Sum.inr val✝, hd⟩) = ↑(((arrowData P).directionRestr s g ∘ (arrowData P).directionRestr s f) ⟨Sum.inr val✝, hd⟩) X:TypeY:TypeP:SlicePFunctor X Ys:(arrowData P).Ai:Fin 2i':Fin 2i'':Fin 2f:i' ⟶ ig:i'' ⟶ i'd:(arrowData P).B sval✝:fibDir P shd:1 = i⊢ ↑((arrowData P).directionRestr s (g ≫ f) ⟨Sum.inr val✝, hd⟩) = ↑(((arrowData P).directionRestr s g ∘ (arrowData P).directionRestr s f) ⟨Sum.inr val✝, hd⟩) X:TypeY:TypeP:SlicePFunctor X Ys:(arrowData P).Ai':Fin 2i'':Fin 2g:i'' ⟶ i'd:(arrowData P).B sval✝:fibDir P sf:i' ⟶ 1⊢ ↑((arrowData P).directionRestr s (g ≫ f) ⟨Sum.inr val✝, ⋯⟩) = ↑(((arrowData P).directionRestr s g ∘ (arrowData P).directionRestr s f) ⟨Sum.inr val✝, ⋯⟩) match i', i'' with X:TypeY:TypeP:SlicePFunctor X Ys:(arrowData P).Ai':Fin 2i'':Fin 2d:(arrowData P).B sval✝:fibDir P sg:0 ⟶ 0f:0 ⟶ 1⊢ ↑((arrowData P).directionRestr s (g ≫ f) ⟨Sum.inr val✝, ⋯⟩) = ↑(((arrowData P).directionRestr s g ∘ (arrowData P).directionRestr s f) ⟨Sum.inr val✝, ⋯⟩) All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Ys:(arrowData P).Ai':Fin 2i'':Fin 2d:(arrowData P).B sval✝:fibDir P sg:0 ⟶ 1f:1 ⟶ 1⊢ ↑((arrowData P).directionRestr s (g ≫ f) ⟨Sum.inr val✝, ⋯⟩) = ↑(((arrowData P).directionRestr s g ∘ (arrowData P).directionRestr s f) ⟨Sum.inr val✝, ⋯⟩) All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Ys:(arrowData P).Ai':Fin 2i'':Fin 2d:(arrowData P).B sval✝:fibDir P sg:1 ⟶ 1f:1 ⟶ 1⊢ ↑((arrowData P).directionRestr s (g ≫ f) ⟨Sum.inr val✝, ⋯⟩) = ↑(((arrowData P).directionRestr s g ∘ (arrowData P).directionRestr s f) ⟨Sum.inr val✝, ⋯⟩) All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Ys:(arrowData P).Ai':Fin 2i'':Fin 2d:(arrowData P).B sval✝:fibDir P sg:1 ⟶ 0f:0 ⟶ 1⊢ ↑((arrowData P).directionRestr s (g ≫ f) ⟨Sum.inr val✝, ⋯⟩) = ↑(((arrowData P).directionRestr s g ∘ (arrowData P).directionRestr s f) ⟨Sum.inr val✝, ⋯⟩) exact absurd (leOfHom g) (X:TypeY:TypeP:SlicePFunctor X Ys:(arrowData P).Ai':Fin 2i'':Fin 2d:(arrowData P).B sval✝:fibDir P sg:1 ⟶ 0f:0 ⟶ 1⊢ ¬1 ≤ 0 All goals completed! 🐙)

Shape restriction along an identity is the identity.

theorem shapeRestr_id (P : SlicePFunctor.{0, 0, 0, 0} X Y) : (arrowData P).ShapeRestrId := X:TypeY:TypeP:SlicePFunctor X Y⊢ (arrowData P).ShapeRestrId X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2⊢ (arrowData P).shapeRestr (𝟙 j) = id X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2s:{ toSliceDomPFunctor := (arrowData P).toSliceDomPFunctor, q := (arrowData P).q }.Shape j⊢ (arrowData P).shapeRestr (𝟙 j) s = id s X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2s:{ toSliceDomPFunctor := (arrowData P).toSliceDomPFunctor, q := (arrowData P).q }.Ahs:{ toSliceDomPFunctor := (arrowData P).toSliceDomPFunctor, q := (arrowData P).q }.ShapeOver j s⊢ (arrowData P).shapeRestr (𝟙 j) ⟨s, hs⟩ = id ⟨s, hs⟩ X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2s:{ toSliceDomPFunctor := (arrowData P).toSliceDomPFunctor, q := (arrowData P).q }.Ahs:{ toSliceDomPFunctor := (arrowData P).toSliceDomPFunctor, q := (arrowData P).q }.ShapeOver j s⊢ ↑((arrowData P).shapeRestr (𝟙 j) ⟨s, hs⟩) = ↑(id ⟨s, hs⟩) match s with X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2s:{ toSliceDomPFunctor := (arrowData P).toSliceDomPFunctor, q := (arrowData P).q }.Aval✝:Yhs:{ toSliceDomPFunctor := (arrowData P).toSliceDomPFunctor, q := (arrowData P).q }.ShapeOver j (Sum.inl val✝)⊢ ↑((arrowData P).shapeRestr (𝟙 j) ⟨Sum.inl val✝, hs⟩) = ↑(id ⟨Sum.inl val✝, hs⟩) All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2s:{ toSliceDomPFunctor := (arrowData P).toSliceDomPFunctor, q := (arrowData P).q }.Aval✝:P.Ahs:{ toSliceDomPFunctor := (arrowData P).toSliceDomPFunctor, q := (arrowData P).q }.ShapeOver j (Sum.inr val✝)⊢ ↑((arrowData P).shapeRestr (𝟙 j) ⟨Sum.inr val✝, hs⟩) = ↑(id ⟨Sum.inr val✝, hs⟩) X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2s:{ toSliceDomPFunctor := (arrowData P).toSliceDomPFunctor, q := (arrowData P).q }.Aval✝:P.Ahs:1 = j⊢ ↑((arrowData P).shapeRestr (𝟙 j) ⟨Sum.inr val✝, hs⟩) = ↑(id ⟨Sum.inr val✝, hs⟩) X:TypeY:TypeP:SlicePFunctor X Ys:{ toSliceDomPFunctor := (arrowData P).toSliceDomPFunctor, q := (arrowData P).q }.Aval✝:P.A⊢ ↑((arrowData P).shapeRestr (𝟙 1) ⟨Sum.inr val✝, ⋯⟩) = ↑(id ⟨Sum.inr val✝, ⋯⟩) All goals completed! 🐙

Shape restriction reverses composition.

theorem shapeRestr_comp (P : SlicePFunctor.{0, 0, 0, 0} X Y) : (arrowData P).ShapeRestrComp := X:TypeY:TypeP:SlicePFunctor X Y⊢ (arrowData P).ShapeRestrComp X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2j':Fin 2j'':Fin 2g:j' ⟶ jh:j'' ⟶ j'⊢ (arrowData P).shapeRestr (h ≫ g) = (arrowData P).shapeRestr h ∘ (arrowData P).shapeRestr g X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2j':Fin 2j'':Fin 2g:j' ⟶ jh:j'' ⟶ j's:{ toSliceDomPFunctor := (arrowData P).toSliceDomPFunctor, q := (arrowData P).q }.Shape j⊢ (arrowData P).shapeRestr (h ≫ g) s = ((arrowData P).shapeRestr h ∘ (arrowData P).shapeRestr g) s X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2j':Fin 2j'':Fin 2g:j' ⟶ jh:j'' ⟶ j's:{ toSliceDomPFunctor := (arrowData P).toSliceDomPFunctor, q := (arrowData P).q }.Ahs:{ toSliceDomPFunctor := (arrowData P).toSliceDomPFunctor, q := (arrowData P).q }.ShapeOver j s⊢ (arrowData P).shapeRestr (h ≫ g) ⟨s, hs⟩ = ((arrowData P).shapeRestr h ∘ (arrowData P).shapeRestr g) ⟨s, hs⟩ X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2j':Fin 2j'':Fin 2g:j' ⟶ jh:j'' ⟶ j's:{ toSliceDomPFunctor := (arrowData P).toSliceDomPFunctor, q := (arrowData P).q }.Ahs:{ toSliceDomPFunctor := (arrowData P).toSliceDomPFunctor, q := (arrowData P).q }.ShapeOver j s⊢ ↑((arrowData P).shapeRestr (h ≫ g) ⟨s, hs⟩) = ↑(((arrowData P).shapeRestr h ∘ (arrowData P).shapeRestr g) ⟨s, hs⟩) match s with X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2j':Fin 2j'':Fin 2g:j' ⟶ jh:j'' ⟶ j's:{ toSliceDomPFunctor := (arrowData P).toSliceDomPFunctor, q := (arrowData P).q }.Aval✝:Yhs:{ toSliceDomPFunctor := (arrowData P).toSliceDomPFunctor, q := (arrowData P).q }.ShapeOver j (Sum.inl val✝)⊢ ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inl val✝, hs⟩) = ↑(((arrowData P).shapeRestr h ∘ (arrowData P).shapeRestr g) ⟨Sum.inl val✝, hs⟩) All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2j':Fin 2j'':Fin 2g:j' ⟶ jh:j'' ⟶ j's:{ toSliceDomPFunctor := (arrowData P).toSliceDomPFunctor, q := (arrowData P).q }.Aval✝:P.Ahs:{ toSliceDomPFunctor := (arrowData P).toSliceDomPFunctor, q := (arrowData P).q }.ShapeOver j (Sum.inr val✝)⊢ ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, hs⟩) = ↑(((arrowData P).shapeRestr h ∘ (arrowData P).shapeRestr g) ⟨Sum.inr val✝, hs⟩) X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2j':Fin 2j'':Fin 2g:j' ⟶ jh:j'' ⟶ j's:{ toSliceDomPFunctor := (arrowData P).toSliceDomPFunctor, q := (arrowData P).q }.Aval✝:P.Ahs:1 = j⊢ ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, hs⟩) = ↑(((arrowData P).shapeRestr h ∘ (arrowData P).shapeRestr g) ⟨Sum.inr val✝, hs⟩) X:TypeY:TypeP:SlicePFunctor X Yj':Fin 2j'':Fin 2h:j'' ⟶ j's:{ toSliceDomPFunctor := (arrowData P).toSliceDomPFunctor, q := (arrowData P).q }.Aval✝:P.Ag:j' ⟶ 1⊢ ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩) = ↑(((arrowData P).shapeRestr h ∘ (arrowData P).shapeRestr g) ⟨Sum.inr val✝, ⋯⟩) match j', j'' with X:TypeY:TypeP:SlicePFunctor X Yj':Fin 2j'':Fin 2s:{ toSliceDomPFunctor := (arrowData P).toSliceDomPFunctor, q := (arrowData P).q }.Aval✝:P.Ah:0 ⟶ 0g:0 ⟶ 1⊢ ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩) = ↑(((arrowData P).shapeRestr h ∘ (arrowData P).shapeRestr g) ⟨Sum.inr val✝, ⋯⟩) All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Yj':Fin 2j'':Fin 2s:{ toSliceDomPFunctor := (arrowData P).toSliceDomPFunctor, q := (arrowData P).q }.Aval✝:P.Ah:0 ⟶ 1g:1 ⟶ 1⊢ ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩) = ↑(((arrowData P).shapeRestr h ∘ (arrowData P).shapeRestr g) ⟨Sum.inr val✝, ⋯⟩) All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Yj':Fin 2j'':Fin 2s:{ toSliceDomPFunctor := (arrowData P).toSliceDomPFunctor, q := (arrowData P).q }.Aval✝:P.Ah:1 ⟶ 1g:1 ⟶ 1⊢ ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩) = ↑(((arrowData P).shapeRestr h ∘ (arrowData P).shapeRestr g) ⟨Sum.inr val✝, ⋯⟩) All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Yj':Fin 2j'':Fin 2s:{ toSliceDomPFunctor := (arrowData P).toSliceDomPFunctor, q := (arrowData P).q }.Aval✝:P.Ah:1 ⟶ 0g:0 ⟶ 1⊢ ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩) = ↑(((arrowData P).shapeRestr h ∘ (arrowData P).shapeRestr g) ⟨Sum.inr val✝, ⋯⟩) exact absurd (leOfHom h) (X:TypeY:TypeP:SlicePFunctor X Yj':Fin 2j'':Fin 2s:{ toSliceDomPFunctor := (arrowData P).toSliceDomPFunctor, q := (arrowData P).q }.Aval✝:P.Ah:1 ⟶ 0g:0 ⟶ 1⊢ ¬1 ≤ 0 All goals completed! 🐙)

Reindexing commutes with direction restriction.

theorem reindex_naturality (P : SlicePFunctor.{0, 0, 0, 0} X Y) : (arrowData P).ReindexNaturality := X:TypeY:TypeP:SlicePFunctor X Y⊢ (arrowData P).ReindexNaturality X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2j':Fin 2g:j' ⟶ js:(arrowData P).toSlicePFunctor.Shape ji:Fin 2i':Fin 2f:i' ⟶ i⊢ (arrowData P).directionRestr (↑s) f ∘ (arrowData P).reindex g s = (arrowData P).reindex g s ∘ (arrowData P).directionRestr (↑((arrowData P).shapeRestr g s)) f X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2j':Fin 2g:j' ⟶ js:(arrowData P).toSlicePFunctor.Shape ji:Fin 2i':Fin 2f:i' ⟶ id:(arrowData P).Direction (↑((arrowData P).shapeRestr g s)) i⊢ ((arrowData P).directionRestr (↑s) f ∘ (arrowData P).reindex g s) d = ((arrowData P).reindex g s ∘ (arrowData P).directionRestr (↑((arrowData P).shapeRestr g s)) f) d X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2j':Fin 2g:j' ⟶ js:(arrowData P).toSlicePFunctor.Shape ji:Fin 2i':Fin 2f:i' ⟶ id:(arrowData P).B ↑((arrowData P).shapeRestr g s)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr g s)) i d⊢ ((arrowData P).directionRestr (↑s) f ∘ (arrowData P).reindex g s) ⟨d, hd⟩ = ((arrowData P).reindex g s ∘ (arrowData P).directionRestr (↑((arrowData P).shapeRestr g s)) f) ⟨d, hd⟩ X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2j':Fin 2g:j' ⟶ js:(arrowData P).toSlicePFunctor.Shape ji:Fin 2i':Fin 2f:i' ⟶ id:(arrowData P).B ↑((arrowData P).shapeRestr g s)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr g s)) i d⊢ ↑(((arrowData P).directionRestr (↑s) f ∘ (arrowData P).reindex g s) ⟨d, hd⟩) = ↑(((arrowData P).reindex g s ∘ (arrowData P).directionRestr (↑((arrowData P).shapeRestr g s)) f) ⟨d, hd⟩) match d with X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2j':Fin 2g:j' ⟶ js:(arrowData P).toSlicePFunctor.Shape ji:Fin 2i':Fin 2f:i' ⟶ id:(arrowData P).B ↑((arrowData P).shapeRestr g s)val✝:Xhd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr g s)) i (Sum.inl val✝)⊢ ↑(((arrowData P).directionRestr (↑s) f ∘ (arrowData P).reindex g s) ⟨Sum.inl val✝, hd⟩) = ↑(((arrowData P).reindex g s ∘ (arrowData P).directionRestr (↑((arrowData P).shapeRestr g s)) f) ⟨Sum.inl val✝, hd⟩) All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2j':Fin 2g:j' ⟶ js:(arrowData P).toSlicePFunctor.Shape ji:Fin 2i':Fin 2f:i' ⟶ id:(arrowData P).B ↑((arrowData P).shapeRestr g s)b:fibDir P ↑((arrowData P).shapeRestr g s)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr g s)) i (Sum.inr b)⊢ ↑(((arrowData P).directionRestr (↑s) f ∘ (arrowData P).reindex g s) ⟨Sum.inr b, hd⟩) = ↑(((arrowData P).reindex g s ∘ (arrowData P).directionRestr (↑((arrowData P).shapeRestr g s)) f) ⟨Sum.inr b, hd⟩) X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2j':Fin 2g:j' ⟶ js:(arrowData P).toSlicePFunctor.Shape ji:Fin 2i':Fin 2f:i' ⟶ id:(arrowData P).B ↑((arrowData P).shapeRestr g s)b:fibDir P ↑((arrowData P).shapeRestr g s)hd:1 = i⊢ ↑(((arrowData P).directionRestr (↑s) f ∘ (arrowData P).reindex g s) ⟨Sum.inr b, hd⟩) = ↑(((arrowData P).reindex g s ∘ (arrowData P).directionRestr (↑((arrowData P).shapeRestr g s)) f) ⟨Sum.inr b, hd⟩) X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2j':Fin 2g:j' ⟶ js:(arrowData P).toSlicePFunctor.Shape ji':Fin 2d:(arrowData P).B ↑((arrowData P).shapeRestr g s)b:fibDir P ↑((arrowData P).shapeRestr g s)f:i' ⟶ 1⊢ ↑(((arrowData P).directionRestr (↑s) f ∘ (arrowData P).reindex g s) ⟨Sum.inr b, ⋯⟩) = ↑(((arrowData P).reindex g s ∘ (arrowData P).directionRestr (↑((arrowData P).shapeRestr g s)) f) ⟨Sum.inr b, ⋯⟩) match i' with X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2j':Fin 2g:j' ⟶ js:(arrowData P).toSlicePFunctor.Shape ji':Fin 2d:(arrowData P).B ↑((arrowData P).shapeRestr g s)b:fibDir P ↑((arrowData P).shapeRestr g s)f:1 ⟶ 1⊢ ↑(((arrowData P).directionRestr (↑s) f ∘ (arrowData P).reindex g s) ⟨Sum.inr b, ⋯⟩) = ↑(((arrowData P).reindex g s ∘ (arrowData P).directionRestr (↑((arrowData P).shapeRestr g s)) f) ⟨Sum.inr b, ⋯⟩) All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2j':Fin 2g:j' ⟶ js:(arrowData P).toSlicePFunctor.Shape ji':Fin 2d:(arrowData P).B ↑((arrowData P).shapeRestr g s)b:fibDir P ↑((arrowData P).shapeRestr g s)f:0 ⟶ 1⊢ ↑(((arrowData P).directionRestr (↑s) f ∘ (arrowData P).reindex g s) ⟨Sum.inr b, ⋯⟩) = ↑(((arrowData P).reindex g s ∘ (arrowData P).directionRestr (↑((arrowData P).shapeRestr g s)) f) ⟨Sum.inr b, ⋯⟩) All goals completed! 🐙

Reindexing along an identity is the identity.

theorem reindex_id (P : SlicePFunctor.{0, 0, 0, 0} X Y) : (arrowData P).ReindexId (shapeRestr_id P) := X:TypeY:TypeP:SlicePFunctor X Y⊢ (arrowData P).ReindexId ⋯ X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2s:(arrowData P).toSlicePFunctor.Shape ji:Fin 2d:(arrowData P).Direction (↑((arrowData P).shapeRestr (𝟙 j) s)) i⊢ (arrowData P).reindex (𝟙 j) s d = cast ⋯ d X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2i:Fin 2s:(arrowData P).toSlicePFunctor.Ahs:(arrowData P).toSlicePFunctor.ShapeOver j sd:(arrowData P).Direction (↑((arrowData P).shapeRestr (𝟙 j) ⟨s, hs⟩)) i⊢ (arrowData P).reindex (𝟙 j) ⟨s, hs⟩ d = cast ⋯ d X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2i:Fin 2s:(arrowData P).toSlicePFunctor.Ahs:(arrowData P).toSlicePFunctor.ShapeOver j sd:(arrowData P).B ↑((arrowData P).shapeRestr (𝟙 j) ⟨s, hs⟩)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (𝟙 j) ⟨s, hs⟩)) i d⊢ (arrowData P).reindex (𝟙 j) ⟨s, hs⟩ ⟨d, hd⟩ = cast ⋯ ⟨d, hd⟩ match s with X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2i:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝:Yhs:(arrowData P).toSlicePFunctor.ShapeOver j (Sum.inl val✝)d:(arrowData P).B ↑((arrowData P).shapeRestr (𝟙 j) ⟨Sum.inl val✝, hs⟩)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (𝟙 j) ⟨Sum.inl val✝, hs⟩)) i d⊢ (arrowData P).reindex (𝟙 j) ⟨Sum.inl val✝, hs⟩ ⟨d, hd⟩ = cast ⋯ ⟨d, hd⟩ X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2i:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝:Yhs:(arrowData P).toSlicePFunctor.ShapeOver j (Sum.inl val✝)d:(arrowData P).B ↑((arrowData P).shapeRestr (𝟙 j) ⟨Sum.inl val✝, hs⟩)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (𝟙 j) ⟨Sum.inl val✝, hs⟩)) i d⊢ ↑((arrowData P).reindex (𝟙 j) ⟨Sum.inl val✝, hs⟩ ⟨d, hd⟩) = ↑(cast ⋯ ⟨d, hd⟩) match d with X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2i:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝¹:Yhs:(arrowData P).toSlicePFunctor.ShapeOver j (Sum.inl val✝)d:(arrowData P).B ↑((arrowData P).shapeRestr (𝟙 j) ⟨Sum.inl val✝, hs⟩)val✝:Xhd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (𝟙 j) ⟨Sum.inl val✝¹, hs⟩)) i (Sum.inl val✝)⊢ ↑((arrowData P).reindex (𝟙 j) ⟨Sum.inl val✝¹, hs⟩ ⟨Sum.inl val✝, hd⟩) = ↑(cast ⋯ ⟨Sum.inl val✝, hd⟩) All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2i:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝:Yhs:(arrowData P).toSlicePFunctor.ShapeOver j (Sum.inl val✝)d:(arrowData P).B ↑((arrowData P).shapeRestr (𝟙 j) ⟨Sum.inl val✝, hs⟩)e:fibDir P ↑((arrowData P).shapeRestr (𝟙 j) ⟨Sum.inl val✝, hs⟩)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (𝟙 j) ⟨Sum.inl val✝, hs⟩)) i (Sum.inr e)⊢ ↑((arrowData P).reindex (𝟙 j) ⟨Sum.inl val✝, hs⟩ ⟨Sum.inr e, hd⟩) = ↑(cast ⋯ ⟨Sum.inr e, hd⟩) All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2i:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝:P.Ahs:(arrowData P).toSlicePFunctor.ShapeOver j (Sum.inr val✝)d:(arrowData P).B ↑((arrowData P).shapeRestr (𝟙 j) ⟨Sum.inr val✝, hs⟩)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (𝟙 j) ⟨Sum.inr val✝, hs⟩)) i d⊢ (arrowData P).reindex (𝟙 j) ⟨Sum.inr val✝, hs⟩ ⟨d, hd⟩ = cast ⋯ ⟨d, hd⟩ X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2i:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝:P.Ahs:1 = jd:(arrowData P).B ↑((arrowData P).shapeRestr (𝟙 j) ⟨Sum.inr val✝, hs⟩)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (𝟙 j) ⟨Sum.inr val✝, hs⟩)) i d⊢ (arrowData P).reindex (𝟙 j) ⟨Sum.inr val✝, hs⟩ ⟨d, hd⟩ = cast ⋯ ⟨d, hd⟩ X:TypeY:TypeP:SlicePFunctor X Yi:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝:P.Ad:(arrowData P).B ↑((arrowData P).shapeRestr (𝟙 1) ⟨Sum.inr val✝, ⋯⟩)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (𝟙 1) ⟨Sum.inr val✝, ⋯⟩)) i d⊢ (arrowData P).reindex (𝟙 1) ⟨Sum.inr val✝, ⋯⟩ ⟨d, hd⟩ = cast ⋯ ⟨d, hd⟩ X:TypeY:TypeP:SlicePFunctor X Yi:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝:P.Ad:(arrowData P).B ↑((arrowData P).shapeRestr (𝟙 1) ⟨Sum.inr val✝, ⋯⟩)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (𝟙 1) ⟨Sum.inr val✝, ⋯⟩)) i d⊢ ↑((arrowData P).reindex (𝟙 1) ⟨Sum.inr val✝, ⋯⟩ ⟨d, hd⟩) = ↑(cast ⋯ ⟨d, hd⟩) match d with X:TypeY:TypeP:SlicePFunctor X Yi:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝¹:P.Ad:(arrowData P).B ↑((arrowData P).shapeRestr (𝟙 1) ⟨Sum.inr val✝, ⋯⟩)val✝:Xhd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (𝟙 1) ⟨Sum.inr val✝¹, ⋯⟩)) i (Sum.inl val✝)⊢ ↑((arrowData P).reindex (𝟙 1) ⟨Sum.inr val✝¹, ⋯⟩ ⟨Sum.inl val✝, hd⟩) = ↑(cast ⋯ ⟨Sum.inl val✝, hd⟩) All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Yi:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝¹:P.Ad:(arrowData P).B ↑((arrowData P).shapeRestr (𝟙 1) ⟨Sum.inr val✝, ⋯⟩)val✝:fibDir P ↑((arrowData P).shapeRestr (𝟙 1) ⟨Sum.inr val✝¹, ⋯⟩)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (𝟙 1) ⟨Sum.inr val✝¹, ⋯⟩)) i (Sum.inr val✝)⊢ ↑((arrowData P).reindex (𝟙 1) ⟨Sum.inr val✝¹, ⋯⟩ ⟨Sum.inr val✝, hd⟩) = ↑(cast ⋯ ⟨Sum.inr val✝, hd⟩) All goals completed! 🐙

Reindexing along a composite is the composite of the reindexings.

theorem reindex_comp (P : SlicePFunctor.{0, 0, 0, 0} X Y) : (arrowData P).ReindexComp (shapeRestr_comp P) := X:TypeY:TypeP:SlicePFunctor X Y⊢ (arrowData P).ReindexComp ⋯ X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2j':Fin 2j'':Fin 2g:j' ⟶ jh:j'' ⟶ j's:(arrowData P).toSlicePFunctor.Shape ji:Fin 2d:(arrowData P).Direction (↑((arrowData P).shapeRestr (h ≫ g) s)) i⊢ (arrowData P).reindex (h ≫ g) s d = (arrowData P).reindex g s ((arrowData P).reindex h ((arrowData P).shapeRestr g s) (cast ⋯ d)) X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2j':Fin 2j'':Fin 2g:j' ⟶ jh:j'' ⟶ j'i:Fin 2s:(arrowData P).toSlicePFunctor.Ahs:(arrowData P).toSlicePFunctor.ShapeOver j sd:(arrowData P).Direction (↑((arrowData P).shapeRestr (h ≫ g) ⟨s, hs⟩)) i⊢ (arrowData P).reindex (h ≫ g) ⟨s, hs⟩ d = (arrowData P).reindex g ⟨s, hs⟩ ((arrowData P).reindex h ((arrowData P).shapeRestr g ⟨s, hs⟩) (cast ⋯ d)) X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2j':Fin 2j'':Fin 2g:j' ⟶ jh:j'' ⟶ j'i:Fin 2s:(arrowData P).toSlicePFunctor.Ahs:(arrowData P).toSlicePFunctor.ShapeOver j sd:(arrowData P).B ↑((arrowData P).shapeRestr (h ≫ g) ⟨s, hs⟩)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (h ≫ g) ⟨s, hs⟩)) i d⊢ (arrowData P).reindex (h ≫ g) ⟨s, hs⟩ ⟨d, hd⟩ = (arrowData P).reindex g ⟨s, hs⟩ ((arrowData P).reindex h ((arrowData P).shapeRestr g ⟨s, hs⟩) (cast ⋯ ⟨d, hd⟩)) match s with X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2j':Fin 2j'':Fin 2g:j' ⟶ jh:j'' ⟶ j'i:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝:Yhs:(arrowData P).toSlicePFunctor.ShapeOver j (Sum.inl val✝)d:(arrowData P).B ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inl val✝, hs⟩)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inl val✝, hs⟩)) i d⊢ (arrowData P).reindex (h ≫ g) ⟨Sum.inl val✝, hs⟩ ⟨d, hd⟩ = (arrowData P).reindex g ⟨Sum.inl val✝, hs⟩ ((arrowData P).reindex h ((arrowData P).shapeRestr g ⟨Sum.inl val✝, hs⟩) (cast ⋯ ⟨d, hd⟩)) X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2j':Fin 2j'':Fin 2g:j' ⟶ jh:j'' ⟶ j'i:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝:Yhs:(arrowData P).toSlicePFunctor.ShapeOver j (Sum.inl val✝)d:(arrowData P).B ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inl val✝, hs⟩)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inl val✝, hs⟩)) i d⊢ ↑((arrowData P).reindex (h ≫ g) ⟨Sum.inl val✝, hs⟩ ⟨d, hd⟩) = ↑((arrowData P).reindex g ⟨Sum.inl val✝, hs⟩ ((arrowData P).reindex h ((arrowData P).shapeRestr g ⟨Sum.inl val✝, hs⟩) (cast ⋯ ⟨d, hd⟩))) match d with X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2j':Fin 2j'':Fin 2g:j' ⟶ jh:j'' ⟶ j'i:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝¹:Yhs:(arrowData P).toSlicePFunctor.ShapeOver j (Sum.inl val✝)d:(arrowData P).B ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inl val✝, hs⟩)val✝:Xhd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inl val✝¹, hs⟩)) i (Sum.inl val✝)⊢ ↑((arrowData P).reindex (h ≫ g) ⟨Sum.inl val✝¹, hs⟩ ⟨Sum.inl val✝, hd⟩) = ↑((arrowData P).reindex g ⟨Sum.inl val✝¹, hs⟩ ((arrowData P).reindex h ((arrowData P).shapeRestr g ⟨Sum.inl val✝¹, hs⟩) (cast ⋯ ⟨Sum.inl val✝, hd⟩))) All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2j':Fin 2j'':Fin 2g:j' ⟶ jh:j'' ⟶ j'i:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝:Yhs:(arrowData P).toSlicePFunctor.ShapeOver j (Sum.inl val✝)d:(arrowData P).B ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inl val✝, hs⟩)e:fibDir P ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inl val✝, hs⟩)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inl val✝, hs⟩)) i (Sum.inr e)⊢ ↑((arrowData P).reindex (h ≫ g) ⟨Sum.inl val✝, hs⟩ ⟨Sum.inr e, hd⟩) = ↑((arrowData P).reindex g ⟨Sum.inl val✝, hs⟩ ((arrowData P).reindex h ((arrowData P).shapeRestr g ⟨Sum.inl val✝, hs⟩) (cast ⋯ ⟨Sum.inr e, hd⟩))) All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2j':Fin 2j'':Fin 2g:j' ⟶ jh:j'' ⟶ j'i:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝:P.Ahs:(arrowData P).toSlicePFunctor.ShapeOver j (Sum.inr val✝)d:(arrowData P).B ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, hs⟩)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, hs⟩)) i d⊢ (arrowData P).reindex (h ≫ g) ⟨Sum.inr val✝, hs⟩ ⟨d, hd⟩ = (arrowData P).reindex g ⟨Sum.inr val✝, hs⟩ ((arrowData P).reindex h ((arrowData P).shapeRestr g ⟨Sum.inr val✝, hs⟩) (cast ⋯ ⟨d, hd⟩)) X:TypeY:TypeP:SlicePFunctor X Yj:Fin 2j':Fin 2j'':Fin 2g:j' ⟶ jh:j'' ⟶ j'i:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝:P.Ahs:1 = jd:(arrowData P).B ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, hs⟩)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, hs⟩)) i d⊢ (arrowData P).reindex (h ≫ g) ⟨Sum.inr val✝, hs⟩ ⟨d, hd⟩ = (arrowData P).reindex g ⟨Sum.inr val✝, hs⟩ ((arrowData P).reindex h ((arrowData P).shapeRestr g ⟨Sum.inr val✝, hs⟩) (cast ⋯ ⟨d, hd⟩)) X:TypeY:TypeP:SlicePFunctor X Yj':Fin 2j'':Fin 2h:j'' ⟶ j'i:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝:P.Ag:j' ⟶ 1d:(arrowData P).B ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩)) i d⊢ (arrowData P).reindex (h ≫ g) ⟨Sum.inr val✝, ⋯⟩ ⟨d, hd⟩ = (arrowData P).reindex g ⟨Sum.inr val✝, ⋯⟩ ((arrowData P).reindex h ((arrowData P).shapeRestr g ⟨Sum.inr val✝, ⋯⟩) (cast ⋯ ⟨d, hd⟩)) X:TypeY:TypeP:SlicePFunctor X Yj':Fin 2j'':Fin 2h:j'' ⟶ j'i:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝:P.Ag:j' ⟶ 1d:(arrowData P).B ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩)) i d⊢ ↑((arrowData P).reindex (h ≫ g) ⟨Sum.inr val✝, ⋯⟩ ⟨d, hd⟩) = ↑((arrowData P).reindex g ⟨Sum.inr val✝, ⋯⟩ ((arrowData P).reindex h ((arrowData P).shapeRestr g ⟨Sum.inr val✝, ⋯⟩) (cast ⋯ ⟨d, hd⟩))) match j', j'' with X:TypeY:TypeP:SlicePFunctor X Yj':Fin 2j'':Fin 2i:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝:P.Ah:0 ⟶ 0g:0 ⟶ 1d:(arrowData P).B ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩)) i d⊢ ↑((arrowData P).reindex (h ≫ g) ⟨Sum.inr val✝, ⋯⟩ ⟨d, hd⟩) = ↑((arrowData P).reindex g ⟨Sum.inr val✝, ⋯⟩ ((arrowData P).reindex h ((arrowData P).shapeRestr g ⟨Sum.inr val✝, ⋯⟩) (cast ⋯ ⟨d, hd⟩))) match d with X:TypeY:TypeP:SlicePFunctor X Yj':Fin 2j'':Fin 2i:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝¹:P.Ah:0 ⟶ 0g:0 ⟶ 1d:(arrowData P).B ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩)val✝:Xhd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝¹, ⋯⟩)) i (Sum.inl val✝)⊢ ↑((arrowData P).reindex (h ≫ g) ⟨Sum.inr val✝¹, ⋯⟩ ⟨Sum.inl val✝, hd⟩) = ↑((arrowData P).reindex g ⟨Sum.inr val✝¹, ⋯⟩ ((arrowData P).reindex h ((arrowData P).shapeRestr g ⟨Sum.inr val✝¹, ⋯⟩) (cast ⋯ ⟨Sum.inl val✝, hd⟩))) All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Yj':Fin 2j'':Fin 2i:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝:P.Ah:0 ⟶ 0g:0 ⟶ 1d:(arrowData P).B ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩)e:fibDir P ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩)) i (Sum.inr e)⊢ ↑((arrowData P).reindex (h ≫ g) ⟨Sum.inr val✝, ⋯⟩ ⟨Sum.inr e, hd⟩) = ↑((arrowData P).reindex g ⟨Sum.inr val✝, ⋯⟩ ((arrowData P).reindex h ((arrowData P).shapeRestr g ⟨Sum.inr val✝, ⋯⟩) (cast ⋯ ⟨Sum.inr e, hd⟩))) All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Yj':Fin 2j'':Fin 2i:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝:P.Ah:0 ⟶ 1g:1 ⟶ 1d:(arrowData P).B ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩)) i d⊢ ↑((arrowData P).reindex (h ≫ g) ⟨Sum.inr val✝, ⋯⟩ ⟨d, hd⟩) = ↑((arrowData P).reindex g ⟨Sum.inr val✝, ⋯⟩ ((arrowData P).reindex h ((arrowData P).shapeRestr g ⟨Sum.inr val✝, ⋯⟩) (cast ⋯ ⟨d, hd⟩))) match d with X:TypeY:TypeP:SlicePFunctor X Yj':Fin 2j'':Fin 2i:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝¹:P.Ah:0 ⟶ 1g:1 ⟶ 1d:(arrowData P).B ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩)val✝:Xhd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝¹, ⋯⟩)) i (Sum.inl val✝)⊢ ↑((arrowData P).reindex (h ≫ g) ⟨Sum.inr val✝¹, ⋯⟩ ⟨Sum.inl val✝, hd⟩) = ↑((arrowData P).reindex g ⟨Sum.inr val✝¹, ⋯⟩ ((arrowData P).reindex h ((arrowData P).shapeRestr g ⟨Sum.inr val✝¹, ⋯⟩) (cast ⋯ ⟨Sum.inl val✝, hd⟩))) All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Yj':Fin 2j'':Fin 2i:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝:P.Ah:0 ⟶ 1g:1 ⟶ 1d:(arrowData P).B ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩)e:fibDir P ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩)) i (Sum.inr e)⊢ ↑((arrowData P).reindex (h ≫ g) ⟨Sum.inr val✝, ⋯⟩ ⟨Sum.inr e, hd⟩) = ↑((arrowData P).reindex g ⟨Sum.inr val✝, ⋯⟩ ((arrowData P).reindex h ((arrowData P).shapeRestr g ⟨Sum.inr val✝, ⋯⟩) (cast ⋯ ⟨Sum.inr e, hd⟩))) All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Yj':Fin 2j'':Fin 2i:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝:P.Ah:1 ⟶ 1g:1 ⟶ 1d:(arrowData P).B ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩)) i d⊢ ↑((arrowData P).reindex (h ≫ g) ⟨Sum.inr val✝, ⋯⟩ ⟨d, hd⟩) = ↑((arrowData P).reindex g ⟨Sum.inr val✝, ⋯⟩ ((arrowData P).reindex h ((arrowData P).shapeRestr g ⟨Sum.inr val✝, ⋯⟩) (cast ⋯ ⟨d, hd⟩))) match d with X:TypeY:TypeP:SlicePFunctor X Yj':Fin 2j'':Fin 2i:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝¹:P.Ah:1 ⟶ 1g:1 ⟶ 1d:(arrowData P).B ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩)val✝:Xhd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝¹, ⋯⟩)) i (Sum.inl val✝)⊢ ↑((arrowData P).reindex (h ≫ g) ⟨Sum.inr val✝¹, ⋯⟩ ⟨Sum.inl val✝, hd⟩) = ↑((arrowData P).reindex g ⟨Sum.inr val✝¹, ⋯⟩ ((arrowData P).reindex h ((arrowData P).shapeRestr g ⟨Sum.inr val✝¹, ⋯⟩) (cast ⋯ ⟨Sum.inl val✝, hd⟩))) All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Yj':Fin 2j'':Fin 2i:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝¹:P.Ah:1 ⟶ 1g:1 ⟶ 1d:(arrowData P).B ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩)val✝:fibDir P ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝¹, ⋯⟩)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝¹, ⋯⟩)) i (Sum.inr val✝)⊢ ↑((arrowData P).reindex (h ≫ g) ⟨Sum.inr val✝¹, ⋯⟩ ⟨Sum.inr val✝, hd⟩) = ↑((arrowData P).reindex g ⟨Sum.inr val✝¹, ⋯⟩ ((arrowData P).reindex h ((arrowData P).shapeRestr g ⟨Sum.inr val✝¹, ⋯⟩) (cast ⋯ ⟨Sum.inr val✝, hd⟩))) All goals completed! 🐙 X:TypeY:TypeP:SlicePFunctor X Yj':Fin 2j'':Fin 2i:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝:P.Ah:1 ⟶ 0g:0 ⟶ 1d:(arrowData P).B ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩)) i d⊢ ↑((arrowData P).reindex (h ≫ g) ⟨Sum.inr val✝, ⋯⟩ ⟨d, hd⟩) = ↑((arrowData P).reindex g ⟨Sum.inr val✝, ⋯⟩ ((arrowData P).reindex h ((arrowData P).shapeRestr g ⟨Sum.inr val✝, ⋯⟩) (cast ⋯ ⟨d, hd⟩))) exact absurd (leOfHom h) (X:TypeY:TypeP:SlicePFunctor X Yj':Fin 2j'':Fin 2i:Fin 2s:(arrowData P).toSlicePFunctor.Aval✝:P.Ah:1 ⟶ 0g:0 ⟶ 1d:(arrowData P).B ↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩)hd:(arrowData P).DirectionOver (↑((arrowData P).shapeRestr (h ≫ g) ⟨Sum.inr val✝, ⋯⟩)) i d⊢ ¬1 ≤ 0 All goals completed! 🐙)

The transcription's operations satisfy the functor laws.

theorem arrowData_isFunctorial (P : SlicePFunctor.{0, 0, 0, 0} X Y) : (arrowData P).IsFunctorial where directionRestr_id := directionRestr_id P directionRestr_comp := directionRestr_comp P shapeRestr_id := shapeRestr_id P shapeRestr_comp := shapeRestr_comp P reindex_naturality := reindex_naturality P reindex_id := reindex_id P reindex_comp := reindex_comp P

The presheaf polynomial endofunctor on the walking arrow transcribing a slice polynomial functor Type/X → Type/Y.

def arrowPsh (P : SlicePFunctor.{0, 0, 0, 0} X Y) : PresheafPFunctor.{0, 0, 0, 0, 0, 0} (Fin 2) (Fin 2) := { arrowData P with isFunctorial := arrowData_isFunctorial P }

The value

Over the walking arrow, a direction assignment is natural exactly when it satisfies the naturality equation along the one non-identity morphism PresheafIRUniv.­waHom, given that direction restriction along identities is the identity.

theorem isNatural_iff (F : PresheafDomPFunctorData.{0, 0, 0, 0} (Fin 2)) (hid : F.DirectionRestrId) (Z : (Fin 2)ᵒᵖ ⥤ Type) (x : F.toSliceDomPFunctor.Obj (PresheafDomPFunctorData.elemProj Z)) : F.IsNatural x ↔ ∀ d : F.Direction x.1.1 1, F.value x (F.directionRestr x.1.1 waHom d) = Z.map waHom.op (F.value x d) := F:PresheafDomPFunctorData (Fin 2)hid:F.DirectionRestrIdZ:(Fin 2)ᵒᵖ ⥤ Typex:F.Obj (PresheafDomPFunctorData.elemProj Z)⊢ F.IsNatural x ↔ ∀ (d : F.Direction (↑x).fst 1), F.value x (F.directionRestr (↑x).fst waHom d) = (ConcreteCategory.hom (Z.map waHom.op)) (F.value x d) F:PresheafDomPFunctorData (Fin 2)hid:F.DirectionRestrIdZ:(Fin 2)ᵒᵖ ⥤ Typex:F.Obj (PresheafDomPFunctorData.elemProj Z)h:∀ (d : F.Direction (↑x).fst 1), F.value x (F.directionRestr (↑x).fst waHom d) = (ConcreteCategory.hom (Z.map waHom.op)) (F.value x d)i:Fin 2i':Fin 2f:i' ⟶ id:F.Direction (↑x).fst i⊢ F.value x (F.directionRestr (↑x).fst f d) = (ConcreteCategory.hom (Z.map f.op)) (F.value x d) match i, i' with F:PresheafDomPFunctorData (Fin 2)hid:F.DirectionRestrIdZ:(Fin 2)ᵒᵖ ⥤ Typex:F.Obj (PresheafDomPFunctorData.elemProj Z)h:∀ (d : F.Direction (↑x).fst 1), F.value x (F.directionRestr (↑x).fst waHom d) = (ConcreteCategory.hom (Z.map waHom.op)) (F.value x d)i:Fin 2i':Fin 2f:0 ⟶ 0d:F.Direction (↑x).fst 0⊢ F.value x (F.directionRestr (↑x).fst f d) = (ConcreteCategory.hom (Z.map f.op)) (F.value x d) F:PresheafDomPFunctorData (Fin 2)hid:F.DirectionRestrIdZ:(Fin 2)ᵒᵖ ⥤ Typex:F.Obj (PresheafDomPFunctorData.elemProj Z)h:∀ (d : F.Direction (↑x).fst 1), F.value x (F.directionRestr (↑x).fst waHom d) = (ConcreteCategory.hom (Z.map waHom.op)) (F.value x d)i:Fin 2i':Fin 2f:0 ⟶ 0d:F.Direction (↑x).fst 0⊢ F.value x (id d) = (ConcreteCategory.hom (𝟙 (Z.obj (Opposite.op 0)))) (F.value x d) All goals completed! 🐙 F:PresheafDomPFunctorData (Fin 2)hid:F.DirectionRestrIdZ:(Fin 2)ᵒᵖ ⥤ Typex:F.Obj (PresheafDomPFunctorData.elemProj Z)h:∀ (d : F.Direction (↑x).fst 1), F.value x (F.directionRestr (↑x).fst waHom d) = (ConcreteCategory.hom (Z.map waHom.op)) (F.value x d)i:Fin 2i':Fin 2f:1 ⟶ 1d:F.Direction (↑x).fst 1⊢ F.value x (F.directionRestr (↑x).fst f d) = (ConcreteCategory.hom (Z.map f.op)) (F.value x d) F:PresheafDomPFunctorData (Fin 2)hid:F.DirectionRestrIdZ:(Fin 2)ᵒᵖ ⥤ Typex:F.Obj (PresheafDomPFunctorData.elemProj Z)h:∀ (d : F.Direction (↑x).fst 1), F.value x (F.directionRestr (↑x).fst waHom d) = (ConcreteCategory.hom (Z.map waHom.op)) (F.value x d)i:Fin 2i':Fin 2f:1 ⟶ 1d:F.Direction (↑x).fst 1⊢ F.value x (id d) = (ConcreteCategory.hom (𝟙 (Z.obj (Opposite.op 1)))) (F.value x d) All goals completed! 🐙 F:PresheafDomPFunctorData (Fin 2)hid:F.DirectionRestrIdZ:(Fin 2)ᵒᵖ ⥤ Typex:F.Obj (PresheafDomPFunctorData.elemProj Z)h:∀ (d : F.Direction (↑x).fst 1), F.value x (F.directionRestr (↑x).fst waHom d) = (ConcreteCategory.hom (Z.map waHom.op)) (F.value x d)i:Fin 2i':Fin 2f:0 ⟶ 1d:F.Direction (↑x).fst 1⊢ F.value x (F.directionRestr (↑x).fst f d) = (ConcreteCategory.hom (Z.map f.op)) (F.value x d) F:PresheafDomPFunctorData (Fin 2)hid:F.DirectionRestrIdZ:(Fin 2)ᵒᵖ ⥤ Typex:F.Obj (PresheafDomPFunctorData.elemProj Z)h:∀ (d : F.Direction (↑x).fst 1), F.value x (F.directionRestr (↑x).fst waHom d) = (ConcreteCategory.hom (Z.map waHom.op)) (F.value x d)i:Fin 2i':Fin 2f:0 ⟶ 1d:F.Direction (↑x).fst 1⊢ F.value x (F.directionRestr (↑x).fst waHom d) = (ConcreteCategory.hom (Z.map waHom.op)) (F.value x d) All goals completed! 🐙 F:PresheafDomPFunctorData (Fin 2)hid:F.DirectionRestrIdZ:(Fin 2)ᵒᵖ ⥤ Typex:F.Obj (PresheafDomPFunctorData.elemProj Z)h:∀ (d : F.Direction (↑x).fst 1), F.value x (F.directionRestr (↑x).fst waHom d) = (ConcreteCategory.hom (Z.map waHom.op)) (F.value x d)i:Fin 2i':Fin 2f:1 ⟶ 0d:F.Direction (↑x).fst 0⊢ F.value x (F.directionRestr (↑x).fst f d) = (ConcreteCategory.hom (Z.map f.op)) (F.value x d) exact absurd (leOfHom f) (F:PresheafDomPFunctorData (Fin 2)hid:F.DirectionRestrIdZ:(Fin 2)ᵒᵖ ⥤ Typex:F.Obj (PresheafDomPFunctorData.elemProj Z)h:∀ (d : F.Direction (↑x).fst 1), F.value x (F.directionRestr (↑x).fst waHom d) = (ConcreteCategory.hom (Z.map waHom.op)) (F.value x d)i:Fin 2i':Fin 2f:1 ⟶ 0d:F.Direction (↑x).fst 0⊢ ¬1 ≤ 0 All goals completed! 🐙)
variable (P : SlicePFunctor.{0, 0, 0, 0} X Y) (Z : (Fin 2)ᵒᵖ ⥤ Type)

The pullback of the family Z 1 → Z 0 along f₀ : X → Z 0: the pairs of an x and an element of Z 1 over f₀ x.

def pullbackAlong (f₀ : X → Z.obj ⟨0⟩) : Type := Σ x : X, { z : Z.obj ⟨1⟩ // Z.map waHom.op z = f₀ x }

The pullback as an object of Type/X.

def pullbackProj (f₀ : X → Z.obj ⟨0⟩) : pullbackAlong Z f₀ → X := Sigma.fst

The value of the transcription at Z, in dependent-type terms: level 0 is Y × (X → Z 0), and level 1 is the sum over f₀ : X → Z 0 of the slice functor's value at the pullback along f₀.

abbrev Levels : Type := (Y × (X → Z.obj ⟨0⟩)) ⊕ (Σ f₀ : X → Z.obj ⟨0⟩, P.toSliceDomPFunctor.Obj (pullbackProj Z f₀))

From the transcription's value to Levels: the level-0 directions of an element assign it a base map X → Z 0, and the level-1 directions of a level-1 element assign it elements of Z 1, which its naturality places over the base map.

def toLevels (x : (arrowPsh P).obj Z) : Levels P Z := match x with | ⟨⟨⟨.inl y, v⟩, hc⟩, _⟩ => .inl (y, fun x₀ ↦ (arrowPsh P).value ⟨⟨.inl y, v⟩, hc⟩ (i := 0) ⟨.inl x₀, rfl⟩) | ⟨⟨⟨.inr a, v⟩, hc⟩, hn⟩ => .inr ⟨fun x₀ ↦ (arrowPsh P).value ⟨⟨.inr a, v⟩, hc⟩ (i := 0) ⟨.inl x₀, rfl⟩, ⟨⟨a, fun b ↦ ⟨P.r ⟨a, b⟩, (arrowPsh P).value ⟨⟨.inr a, v⟩, hc⟩ (i := 1) ⟨.inr b, rfl⟩, (hn waHom ⟨.inr b, rfl⟩).symm⟩⟩, rfl⟩⟩

From Levels to the transcription's value: the inverse assignment, natural by the equation over the base map.

def ofLevels (o : Levels P Z) : (arrowPsh P).obj Z := match o with | .inl (y, f₀) => ⟨⟨⟨.inl y, fun d ↦ match d with | .inl x₀ => ⟨0, f₀ x₀⟩ | .inr e => PEmpty.elim e⟩, funext fun d ↦ match d with | .inl _ => rfl | .inr e => PEmpty.elim e⟩, (isNatural_iff _ (directionRestr_id P) Z _).mpr fun d ↦ match d with | ⟨.inl _, hd⟩ => absurd hd Fin.zero_ne_one | ⟨.inr e, _⟩ => PEmpty.elim e⟩ | .inr ⟨f₀, o⟩ => ⟨⟨⟨.inr o.1.1, fun d ↦ match d with | .inl x₀ => ⟨0, f₀ x₀⟩ | .inr b => ⟨1, (o.1.2 b).2.1⟩⟩, funext fun d ↦ match d with | .inl _ => rfl | .inr _ => rfl⟩, (isNatural_iff _ (directionRestr_id P) Z _).mpr fun d ↦ match d with | ⟨.inl _, hd⟩ => absurd hd Fin.zero_ne_one | ⟨.inr b, _⟩ => ((o.1.2 b).2.2.trans (congrArg f₀ (congrFun o.2 b))).symm⟩

A dependent pair reassembled from its components after a cast of the second along an equation of the first is the original pair.

private theorem sigma_mk_cast {j i : Fin 2} (z : Z.obj ⟨j⟩) (e : j = i) : (⟨i, cast (congrArg (fun k : Fin 2 ↦ Z.obj ⟨k⟩) e) z⟩ : Σ k : Fin 2, Z.obj ⟨k⟩) = ⟨j, z⟩ := Z:(Fin 2)ᵒᵖ ⥤ Typej:Fin 2i:Fin 2z:Z.obj (Opposite.op j)e:j = i⊢ ⟨i, cast ⋯ z⟩ = ⟨j, z⟩ Z:(Fin 2)ᵒᵖ ⥤ Typej:Fin 2z:Z.obj (Opposite.op j)⊢ ⟨j, cast ⋯ z⟩ = ⟨j, z⟩ All goals completed! 🐙

The Z-value an element assigns to a direction, paired with the direction's level, is the element's raw assignment.

theorem sigma_value (F : PresheafDomPFunctorData.{0, 0, 0, 0} (Fin 2)) (x : F.toSliceDomPFunctor.Obj (PresheafDomPFunctorData.elemProj Z)) ⦃i : Fin 2⦄ (b : F.Direction x.1.1 i) : (⟨i, F.value x b⟩ : Σ k : Fin 2, Z.obj ⟨k⟩) = x.1.2 b.1 := Z:(Fin 2)ᵒᵖ ⥤ TypeF:PresheafDomPFunctorData (Fin 2)x:F.Obj (PresheafDomPFunctorData.elemProj Z)i:Fin 2b:F.Direction (↑x).fst i⊢ ⟨i, F.value x b⟩ = (↑x).snd ↑b Z:(Fin 2)ᵒᵖ ⥤ TypeF:PresheafDomPFunctorData (Fin 2)i:Fin 2a:F.Av:F.B a → (i : Fin 2) × Z.obj (Opposite.op i)hc:F.Compatible (PresheafDomPFunctorData.elemProj Z) ⟨a, v⟩.fst ⟨a, v⟩.sndb:F.Direction (↑⟨⟨a, v⟩, hc⟩).fst i⊢ ⟨i, F.value ⟨⟨a, v⟩, hc⟩ b⟩ = (↑⟨⟨a, v⟩, hc⟩).snd ↑b Z:(Fin 2)ᵒᵖ ⥤ TypeF:PresheafDomPFunctorData (Fin 2)i:Fin 2a:F.Av:F.B a → (i : Fin 2) × Z.obj (Opposite.op i)hc:F.Compatible (PresheafDomPFunctorData.elemProj Z) ⟨a, v⟩.fst ⟨a, v⟩.sndb:F.B (↑⟨⟨a, v⟩, hc⟩).fsthb:F.DirectionOver (↑⟨⟨a, v⟩, hc⟩).fst i b⊢ ⟨i, F.value ⟨⟨a, v⟩, hc⟩ ⟨b, hb⟩⟩ = (↑⟨⟨a, v⟩, hc⟩).snd ↑⟨b, hb⟩ All goals completed! 🐙

An element of a pullback reassembled from its components along an equation of its base point is the original element.

theorem pullbackAlong_ext {f₀ : X → Z.obj ⟨0⟩} (q : pullbackAlong Z f₀) (x : X) (h : q.1 = x) : (⟨x, q.2.1, X:TypeY:TypeP:SlicePFunctor X YZ:(Fin 2)ᵒᵖ ⥤ Typef₀:X → Z.obj (Opposite.op 0)q:pullbackAlong Z f₀x:Xh:q.fst = x⊢ (ConcreteCategory.hom (Z.map waHom.op)) ↑q.snd = f₀ x X:TypeY:TypeP:SlicePFunctor X YZ:(Fin 2)ᵒᵖ ⥤ Typef₀:X → Z.obj (Opposite.op 0)q:pullbackAlong Z f₀x:Xh:q.fst = x⊢ (ConcreteCategory.hom (Z.map waHom.op)) ↑q.snd = f₀ q.fst; All goals completed! 🐙⟩ : pullbackAlong Z f₀) = q := X:TypeZ:(Fin 2)ᵒᵖ ⥤ Typef₀:X → Z.obj (Opposite.op 0)q:pullbackAlong Z f₀x:Xh:q.fst = x⊢ ⟨x, ⟨↑q.snd, ⋯⟩⟩ = q X:TypeZ:(Fin 2)ᵒᵖ ⥤ Typef₀:X → Z.obj (Opposite.op 0)x:Xfst✝:Xval✝:Z.obj (Opposite.op 1)property✝:(ConcreteCategory.hom (Z.map waHom.op)) val✝ = f₀ fst✝h:⟨fst✝, ⟨val✝, property✝⟩⟩.fst = x⊢ ⟨x, ⟨↑⟨fst✝, ⟨val✝, property✝⟩⟩.snd, ⋯⟩⟩ = ⟨fst✝, ⟨val✝, property✝⟩⟩ X:TypeZ:(Fin 2)ᵒᵖ ⥤ Typef₀:X → Z.obj (Opposite.op 0)fst✝:Xval✝:Z.obj (Opposite.op 1)property✝:(ConcreteCategory.hom (Z.map waHom.op)) val✝ = f₀ fst✝⊢ ⟨⟨fst✝, ⟨val✝, property✝⟩⟩.fst, ⟨↑⟨fst✝, ⟨val✝, property✝⟩⟩.snd, ⋯⟩⟩ = ⟨fst✝, ⟨val✝, property✝⟩⟩ All goals completed! 🐙

The transcription's value at Z is Levels P Z.

def objEquiv : (arrowPsh P).obj Z ≃ Levels P Z where toFun := toLevels P Z invFun := ofLevels P Z left_inv x := match x with | ⟨⟨⟨.inl _, _⟩, _⟩, _⟩ => Subtype.ext (Subtype.ext (Sigma.ext rfl (heq_of_eq (funext fun d ↦ match d with | .inl _ => sigma_value Z _ _ _ | .inr e => PEmpty.elim e)))) | ⟨⟨⟨.inr _, _⟩, _⟩, _⟩ => Subtype.ext (Subtype.ext (Sigma.ext rfl (heq_of_eq (funext fun d ↦ match d with | .inl _ => sigma_value Z _ _ _ | .inr _ => sigma_value Z _ _ _)))) right_inv o := match o with | .inl _ => rfl | .inr ⟨_, o⟩ => congrArg Sum.inr (Sigma.ext rfl (heq_of_eq (Subtype.ext (Sigma.ext rfl (heq_of_eq (funext fun b ↦ pullbackAlong_ext Z (o.1.2 b) _ (congrFun o.2 b)))))))

Restricting a level-1 element over (y, f₀) along 0 ⟶ 1 gives the level-0 element (y, f₀), where y is the slice functor's output index of the element.

theorem toLevels_objRestr (f₀ : X → Z.obj ⟨0⟩) (o : P.toSliceDomPFunctor.Obj (pullbackProj Z f₀)) : toLevels P Z ((arrowPsh P).objRestr waHom (ofLevels P Z (.inr ⟨f₀, o⟩)) rfl) = .inl (P.obj (pullbackProj Z f₀) o, f₀) := rfl

The fibre over X

The fibres of a walking-arrow presheaf built from an object of Type/X: X at level 0, the object at level 1.

def arrowObj (A B : Type) : Fin 2 → Type | 0 => A | 1 => B

The restriction maps of that presheaf: identities, and the structure map along 0 ⟶ 1.

def arrowMap {A B : Type} (p : B → A) : ∀ (i i' : Fin 2), (i' ⟶ i) → arrowObj A B i → arrowObj A B i' | 0, 0, _ => id | 1, 1, _ => id | 1, 0, _ => p | 0, 1, f => absurd (leOfHom f) (X:TypeY:TypeP:SlicePFunctor X YZ:(Fin 2)ᵒᵖ ⥤ TypeA:TypeB:Typep:B → Af:1 ⟶ 0⊢ ¬1 ≤ 0 All goals completed! 🐙)

An object p : E → X of Type/X as a walking-arrow presheaf: X at level 0, E at level 1, p the restriction along 0 ⟶ 1. This is the inclusion of the fibre Type/X into Fam(Type).

def ofSlice {E : Type} (p : E → X) : (Fin 2)ᵒᵖ ⥤ Type where obj o := arrowObj X E o.unop map f := ↾ arrowMap p _ _ f.unop map_id o := match o with | ⟨0⟩ => rfl | ⟨1⟩ => rfl map_comp {o o' o''} f g := match o, o', o'', f, g with | ⟨0⟩, ⟨0⟩, ⟨0⟩, _, _ => rfl | ⟨1⟩, ⟨1⟩, ⟨1⟩, _, _ => rfl | ⟨1⟩, ⟨0⟩, ⟨0⟩, _, _ => rfl | ⟨1⟩, ⟨1⟩, ⟨0⟩, _, _ => rfl | ⟨1⟩, ⟨0⟩, ⟨1⟩, _, g => absurd (leOfHom g.unop) (X:TypeY:TypeP:SlicePFunctor X YZ:(Fin 2)ᵒᵖ ⥤ TypeE:Typep:E → Xo:(Fin 2)ᵒᵖo':(Fin 2)ᵒᵖo'':(Fin 2)ᵒᵖf:o ⟶ o'g✝:o' ⟶ o''x✝:Opposite.op 1 ⟶ Opposite.op 0g:Opposite.op 0 ⟶ Opposite.op 1⊢ ¬Opposite.unop (Opposite.op 1) ≤ Opposite.unop (Opposite.op 0) All goals completed! 🐙) | ⟨0⟩, ⟨1⟩, _, f, _ => absurd (leOfHom f.unop) (X:TypeY:TypeP:SlicePFunctor X YZ:(Fin 2)ᵒᵖ ⥤ TypeE:Typep:E → Xo:(Fin 2)ᵒᵖo':(Fin 2)ᵒᵖo'':(Fin 2)ᵒᵖf✝:o ⟶ o'g:o' ⟶ o''x✝¹:(Fin 2)ᵒᵖf:Opposite.op 0 ⟶ Opposite.op 1x✝:Opposite.op 1 ⟶ x✝¹⊢ ¬Opposite.unop (Opposite.op 1) ≤ Opposite.unop (Opposite.op 0) All goals completed! 🐙) | ⟨0⟩, ⟨0⟩, ⟨1⟩, _, g => absurd (leOfHom g.unop) (X:TypeY:TypeP:SlicePFunctor X YZ:(Fin 2)ᵒᵖ ⥤ TypeE:Typep:E → Xo:(Fin 2)ᵒᵖo':(Fin 2)ᵒᵖo'':(Fin 2)ᵒᵖf:o ⟶ o'g✝:o' ⟶ o''x✝:Opposite.op 0 ⟶ Opposite.op 0g:Opposite.op 0 ⟶ Opposite.op 1⊢ ¬Opposite.unop (Opposite.op 1) ≤ Opposite.unop (Opposite.op 0) All goals completed! 🐙)

The components of a morphism over X as a natural transformation: the identity at level 0, the morphism at level 1.

def arrowHomApp {E E' : Type} (h : E → E') : ∀ i : Fin 2, arrowObj X E i → arrowObj X E' i | 0 => id | 1 => h

A morphism h over X, p' ∘ h = p, as a natural transformation ofSlice p ⟶ ofSlice p'.

def ofSliceHom {E E' : Type} {p : E → X} {p' : E' → X} (h : E → E') (hh : p' ∘ h = p) : NatTrans (ofSlice p) (ofSlice p') where app o := ↾ arrowHomApp h o.unop naturality {o o'} f := match o, o', f with | ⟨0⟩, ⟨0⟩, _ => rfl | ⟨1⟩, ⟨1⟩, _ => rfl | ⟨1⟩, ⟨0⟩, _ => congrArg TypeCat.ofHom hh.symm | ⟨0⟩, ⟨1⟩, f => absurd (leOfHom f.unop) (X:TypeY:TypeP:SlicePFunctor X YZ:(Fin 2)ᵒᵖ ⥤ TypeE:TypeE':Typep:E → Xp':E' → Xh:E → E'hh:p' ∘ h = po:(Fin 2)ᵒᵖo':(Fin 2)ᵒᵖf✝:o ⟶ o'f:Opposite.op 0 ⟶ Opposite.op 1⊢ ¬Opposite.unop (Opposite.op 1) ≤ Opposite.unop (Opposite.op 0) All goals completed! 🐙)

An element of E as an element of the pullback of ofSlice p along the identity, over its own image.

def toPullback {E : Type} (p : E → X) (e : E) : pullbackAlong (ofSlice p) id := ⟨p e, e, rfl⟩

The pullback of ofSlice p along the identity is p itself, at the level of the slice functor's values: the level-1 fibre of the transcription over (y, id) is the slice functor's value.

def pullbackIdEquiv {E : Type} (p : E → X) : P.toSliceDomPFunctor.Obj (pullbackProj (ofSlice p) id) ≃ P.toSliceDomPFunctor.Obj p where toFun := P.map (fun q ↦ q.2.1) (funext fun q ↦ q.2.2) invFun := P.map (toPullback p) rfl left_inv q := Subtype.ext (Sigma.ext rfl (heq_of_eq (funext fun b ↦ pullbackAlong_ext (ofSlice p) (q.1.2 b) _ (q.1.2 b).2.2.symm))) right_inv _ := Subtype.ext rfl

The comparison map from the slice functor's value at p to the transcription's value at ofSlice p: the level-1 element over the identity base map.

def cmp {E : Type} (p : E → X) (o : P.toSliceDomPFunctor.Obj p) : (arrowPsh P).obj (ofSlice p) := ofLevels P (ofSlice p) (.inr ⟨id, (pullbackIdEquiv P p).symm o⟩)

The comparison map's image, read in Levels: the identity base map with the slice functor's value transported along pullbackIdEquiv.

theorem objEquiv_cmp {E : Type} (p : E → X) (o : P.toSliceDomPFunctor.Obj p) : objEquiv P (ofSlice p) (cmp P p o) = .inr ⟨id, (pullbackIdEquiv P p).symm o⟩ := X:TypeY:TypeP:SlicePFunctor X YE:Typep:E → Xo:P.Obj p⊢ (objEquiv P (ofSlice p)) (cmp P p o) = Sum.inr ⟨id, (pullbackIdEquiv P p).symm o⟩ All goals completed! 🐙

The comparison map is natural in the object of Type/X.

theorem map_cmp {E E' : Type} {p : E → X} {p' : E' → X} (h : E → E') (hh : p' ∘ h = p) (o : P.toSliceDomPFunctor.Obj p) : (arrowPsh P).map (ofSliceHom h hh) (cmp P p o) = cmp P p' (P.map h hh o) := Subtype.ext (Subtype.ext (Sigma.ext rfl (heq_of_eq (funext fun d ↦ match d with | .inl _ => rfl | .inr _ => rfl))))

The comparison map's image restricts along 0 ⟶ 1 to the level-0 element (y, id), where y is the slice functor's output index.

theorem toLevels_objRestr_cmp {E : Type} (p : E → X) (o : P.toSliceDomPFunctor.Obj p) : toLevels P (ofSlice p) ((arrowPsh P).objRestr waHom (cmp P p o) rfl) = .inl (P.obj p o, id) := toLevels_objRestr P (ofSlice p) id _
end GebProto.LargeIR