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.Mathlib.Data.PFunctor.Presheaf.W
public import Geb.Mathlib.Data.PFunctor.Slice.Decidable
public import Geb.Mathlib.Data.W.BasicDecidability of naturality and hereditary naturality
PresheafDomPFunctorData.IsNatural is a quantifier over the objects, the
hom-sets, and the directions of the index category, of an equality in a fiber
of the input presheaf. It is decidable when the functor is finitary, the index
category has finitely many objects and finite hom-sets, and the input
presheaf's values have decidable equality.
PresheafPFunctor.IsHereditarilyNatural extends the naturality condition to
every node of a slice W-tree. It is decided by a classless Bool-valued core
that carries every finiteness and decidability datum explicitly, enumerating
each node's raw directions with FinEnum.toList rather than synthesising a
Decidable instance through the PresheafPFunctor diamond.
Main definitions
PresheafDomPFunctorData.decidableIsNatural — decidability of IsNatural.
PresheafPFunctor.isHereditarilyNaturalBoolCore — the classless Bool-valued
hereditary-naturality checker.
PresheafPFunctor.decidableIsHereditarilyNatural — decidability of
IsHereditarilyNatural.
Main statements
PresheafPFunctor.isHereditarilyNaturalBoolCore_eq_true_iff — the core returns
true exactly on hereditarily natural slice W-trees.
Tags
polynomial functor, presheaf, naturality, decidability, FinEnum
public sectionopen CategoryTheoryuniverse uI uA uB vI uZnamespace PresheafDomPFunctorData
Naturality of a direction assignment is decidable when the functor is
finitary, the index category has finitely many objects and finite
hom-sets, and the input presheaf's values have decidable equality. Its
subject is a slice object over elemProj Z, not a PresheafDomPFunctorData.obj Z:
the latter is the IsNatural subtype itself, on which the predicate
holds by projection.
instance decidableIsNatural {I : Type uI} [Category.{vI} I]
(F : PresheafDomPFunctorData.{uI, uA, uB, vI} I) {Z : Iᵒᵖ ⥤ Type uZ}
[F.Finitary] [FinEnum I] [∀ i i' : I, FinEnum (i' ⟶ i)]
[∀ i : I, DecidableEq (Z.obj ⟨i⟩)]
(x : F.toSliceDomPFunctor.Obj (elemProj Z)) : Decidable (F.IsNatural x) :=
inferInstanceAs (Decidable (∀ ⦃i i' : I⦄ (f : i' ⟶ i)
(b : F.toSliceDomPFunctor.Direction x.1.1 i),
F.value x (F.directionRestr x.1.1 f b) = Z.map f.op (F.value x b)))end PresheafDomPFunctorDatanamespace PresheafPFunctor
The root-only restriction of a raw W-tree along a morphism: restrict
the root shape and reindex the direction assignment. The underlying-tree
form of wRestrTree, stated on the admissibility subtype; the head-index
witness hq is retained because objRestrElt consumes it.
@[expose] def wRestrTreeRaw {I : Type uI} [Category.{vI} I]
(F : PresheafPFunctor.{uI, uI, uA, uB, vI, vI} I I) ⦃j j' : I⦄ (g : j' ⟶ j)
(w : F.toPFunctor.W) (hq : F.q (PFunctor.W.head w) = j) : WType F.toPFunctor.B :=
match w, hq with
| WType.mk a f, hq =>
WType.mk (F.shapeRestr g ⟨a, hq⟩).1
fun b' ↦ f (F.reindex g ⟨a, hq⟩ (i := F.rCurried _ b') ⟨b', rfl⟩).1
The underlying tree of wRestrTree is wRestrTreeRaw.
theorem wRestrTree_val {I : Type uI} [Category.{vI} I]
(F : PresheafPFunctor.{uI, uI, uA, uB, vI, vI} I I) ⦃j j' : I⦄ (g : j' ⟶ j)
(z : F.toSlicePFunctor.W) (hq : F.q (PFunctor.W.head z.1) = j) :
(F.wRestrTree g z hq).1 = F.wRestrTreeRaw g z.1 hq := I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I Ij:Ij':Ig:j' ⟶ jz:F.toSlicePFunctor.Whq:F.q (↑z).head = j⊢ ↑(F.wRestrTree g z hq) = F.wRestrTreeRaw g (↑z) hq
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I Ij:Ij':Ig:j' ⟶ jw:F.toSlicePFunctor.Whw:F.toSlicePFunctor.WValid whq:F.q (↑⟨w, hw⟩).head = j⊢ ↑(F.wRestrTree g ⟨w, hw⟩ hq) = F.wRestrTreeRaw g (↑⟨w, hw⟩) hq
cases w with
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I Ij:Ij':Ig:j' ⟶ ja:F.toSlicePFunctor.Af:F.toSlicePFunctor.B a → WType F.toSlicePFunctor.Bhw:F.toSlicePFunctor.WValid (WType.mk a f)hq:F.q (↑⟨WType.mk a f, hw⟩).head = j⊢ ↑(F.wRestrTree g ⟨WType.mk a f, hw⟩ hq) = F.wRestrTreeRaw g (↑⟨WType.mk a f, hw⟩) hq All goals completed! 🐙
Hereditary naturality as a Bool, classless. All finiteness and
decidability supplied explicitly; the raw directions of each node are
enumerated and filtered by an explicit equality test, so no typeclass
inference traverses the PresheafPFunctor diamond.
@[expose] def isHereditarilyNaturalBoolCore {I : Type uI} [Category.{vI} I]
(F : PresheafPFunctor.{uI, uI, uA, uB, vI, vI} I I)
(decI : DecidableEq I) (feI : FinEnum I) (feHom : ∀ i i' : I, FinEnum (i' ⟶ i))
(feB : ∀ a, FinEnum (F.toPFunctor.B a)) (decEqW : DecidableEq (WType F.toPFunctor.B)) :
F.toPFunctor.W → Bool :=
WType.para Bool fun x ↦
((feI.toList).all fun i ↦ (feI.toList).all fun i' ↦
((feHom i i').toList).all fun g ↦
((feB x.1).toList).all fun b' ↦
match decI (F.rCurried x.1 b') i with
| isFalse _ => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.2 b').1)) i with
| isFalse _ => true
| isTrue hq =>
(decEqW (x.2 (F.directionRestr x.1 g ⟨b', hb⟩).1).1
(F.wRestrTreeRaw g (x.2 b').1 hq)).decide)
&& ((feB x.1).toList).all fun b' ↦ (x.2 b').2
isHereditarilyNaturalBoolCore decides hereditary naturality.
theorem isHereditarilyNaturalBoolCore_eq_true_iff {I : Type uI} [Category.{vI} I]
(F : PresheafPFunctor.{uI, uI, uA, uB, vI, vI} I I)
(decI : DecidableEq I) (feI : FinEnum I) (feHom : ∀ i i' : I, FinEnum (i' ⟶ i))
(feB : ∀ a, FinEnum (F.toPFunctor.B a)) (decEqW : DecidableEq (WType F.toPFunctor.B))
(z : F.toSlicePFunctor.W) :
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW z.1 = true ↔
F.IsHereditarilyNatural z := I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.W⊢ F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑z = true ↔ F.IsHereditarilyNatural z
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)⊢ F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑(SlicePFunctor.W.mk x) = true ↔
F.IsHereditarilyNatural (SlicePFunctor.W.mk x)
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)⊢ F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑(SlicePFunctor.W.mk x) = true ↔
(∀ ⦃i i' : I⦄ (g : i' ⟶ i) (b : F.Direction (↑x).fst i),
(↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯) ∧
∀ (b : F.B (↑x).fst), F.IsHereditarilyNatural ((↑x).snd b)
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)⊢ (((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B (↑x).fst)).all fun b' ↦
match decI (F.rCurried (↑x).fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) b'))) i with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst g ⟨b', hb⟩) =
F.wRestrTreeRaw g ((Subtype.val ∘ (↑x).snd) b') hq)) &&
(FinEnum.toList (F.B (↑x).fst)).all fun b' ↦
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b')) =
true ↔
(∀ ⦃i i' : I⦄ (g : i' ⟶ i) (b : F.Direction (↑x).fst i),
(↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯) ∧
∀ (b : F.B (↑x).fst), F.IsHereditarilyNatural ((↑x).snd b)
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)⊢ ((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B (↑x).fst)).all fun b' ↦
match decI (F.rCurried (↑x).fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) b'))) i with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst g ⟨b', hb⟩) =
F.wRestrTreeRaw g ((Subtype.val ∘ (↑x).snd) b') hq)) =
true ∧
((FinEnum.toList (F.B (↑x).fst)).all fun b' ↦
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b')) =
true ↔
(∀ ⦃i i' : I⦄ (g : i' ⟶ i) (b : F.Direction (↑x).fst i),
(↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯) ∧
∀ (b : F.B (↑x).fst), F.IsHereditarilyNatural ((↑x).snd b)
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)⊢ ((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B (↑x).fst)).all fun b' ↦
match decI (F.rCurried (↑x).fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) b'))) i with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst g ⟨b', hb⟩) =
F.wRestrTreeRaw g ((Subtype.val ∘ (↑x).snd) b') hq)) =
true ↔
∀ ⦃i i' : I⦄ (g : i' ⟶ i) (b : F.Direction (↑x).fst i),
(↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)⊢ ((FinEnum.toList (F.B (↑x).fst)).all fun b' ↦
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide ((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b')) =
true ↔
∀ (b : F.B (↑x).fst), F.IsHereditarilyNatural ((↑x).snd b)
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)⊢ ((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B (↑x).fst)).all fun b' ↦
match decI (F.rCurried (↑x).fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) b'))) i with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst g ⟨b', hb⟩) =
F.wRestrTreeRaw g ((Subtype.val ∘ (↑x).snd) b') hq)) =
true ↔
∀ ⦃i i' : I⦄ (g : i' ⟶ i) (b : F.Direction (↑x).fst i),
(↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯ I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)⊢ (∀ (x_1 x_2 : I) (x_3 : x_2 ⟶ x_1) (x_4 : F.B (↑x).fst),
(match decI (F.rCurried (↑x).fst x_4) x_1 with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) x_4))) x_1 with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst x_3 ⟨x_4, hb⟩) =
F.wRestrTreeRaw x_3 ((Subtype.val ∘ (↑x).snd) x_4) hq)) =
true) ↔
∀ ⦃i i' : I⦄ (g : i' ⟶ i) (b : F.Direction (↑x).fst i),
(↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)⊢ (∀ (x_1 x_2 : I) (x_3 : x_2 ⟶ x_1) (x_4 : F.B (↑x).fst),
(match decI (F.rCurried (↑x).fst x_4) x_1 with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) x_4))) x_1 with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst x_3 ⟨x_4, hb⟩) =
F.wRestrTreeRaw x_3 ((Subtype.val ∘ (↑x).snd) x_4) hq)) =
true) →
∀ ⦃i i' : I⦄ (g : i' ⟶ i) (b : F.Direction (↑x).fst i),
(↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)⊢ (∀ ⦃i i' : I⦄ (g : i' ⟶ i) (b : F.Direction (↑x).fst i),
(↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯) →
∀ (x_1 x_2 : I) (x_3 : x_2 ⟶ x_1) (x_4 : F.B (↑x).fst),
(match decI (F.rCurried (↑x).fst x_4) x_1 with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) x_4))) x_1 with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst x_3 ⟨x_4, hb⟩) =
F.wRestrTreeRaw x_3 ((Subtype.val ∘ (↑x).snd) x_4) hq)) =
true
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)⊢ (∀ (x_1 x_2 : I) (x_3 : x_2 ⟶ x_1) (x_4 : F.B (↑x).fst),
(match decI (F.rCurried (↑x).fst x_4) x_1 with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) x_4))) x_1 with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst x_3 ⟨x_4, hb⟩) =
F.wRestrTreeRaw x_3 ((Subtype.val ∘ (↑x).snd) x_4) hq)) =
true) →
∀ ⦃i i' : I⦄ (g : i' ⟶ i) (b : F.Direction (↑x).fst i),
(↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯ I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ (x_1 x_2 : I) (x_3 : x_2 ⟶ x_1) (x_4 : F.B (↑x).fst),
(match decI (F.rCurried (↑x).fst x_4) x_1 with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) x_4))) x_1 with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst x_3 ⟨x_4, hb⟩) =
F.wRestrTreeRaw x_3 ((Subtype.val ∘ (↑x).snd) x_4) hq)) =
truei:Ii':Ig:i' ⟶ ib:F.Direction (↑x).fst i⊢ (↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ (x_1 x_2 : I) (x_3 : x_2 ⟶ x_1) (x_4 : F.B (↑x).fst),
(match decI (F.rCurried (↑x).fst x_4) x_1 with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) x_4))) x_1 with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst x_3 ⟨x_4, hb⟩) =
F.wRestrTreeRaw x_3 ((Subtype.val ∘ (↑x).snd) x_4) hq)) =
truei:Ii':Ig:i' ⟶ ib:F.Direction (↑x).fst ihb:F.rCurried (↑x).fst ↑b = i⊢ (↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ (x_1 x_2 : I) (x_3 : x_2 ⟶ x_1) (x_4 : F.B (↑x).fst),
(match decI (F.rCurried (↑x).fst x_4) x_1 with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) x_4))) x_1 with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst x_3 ⟨x_4, hb⟩) =
F.wRestrTreeRaw x_3 ((Subtype.val ∘ (↑x).snd) x_4) hq)) =
truei:Ii':Ig:i' ⟶ ib:F.Direction (↑x).fst ihb:F.rCurried (↑x).fst ↑b = ihqval:F.q (↑((↑x).snd ↑b)).head = i⊢ (↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ (x_1 x_2 : I) (x_3 : x_2 ⟶ x_1) (x_4 : F.B (↑x).fst),
(match decI (F.rCurried (↑x).fst x_4) x_1 with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) x_4))) x_1 with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst x_3 ⟨x_4, hb⟩) =
F.wRestrTreeRaw x_3 ((Subtype.val ∘ (↑x).snd) x_4) hq)) =
truei:Ii':Ig:i' ⟶ ib:F.Direction (↑x).fst ihb:F.rCurried (↑x).fst ↑b = ihqval:F.q (↑((↑x).snd ↑b)).head = ihthis:(match decI (F.rCurried (↑x).fst ↑b) i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) ↑b))) i with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst g ⟨↑b, hb⟩) =
F.wRestrTreeRaw g ((Subtype.val ∘ (↑x).snd) ↑b) hq)) =
true⊢ (↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ (x_1 x_2 : I) (x_3 : x_2 ⟶ x_1) (x_4 : F.B (↑x).fst),
(match decI (F.rCurried (↑x).fst x_4) x_1 with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) x_4))) x_1 with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst x_3 ⟨x_4, hb⟩) =
F.wRestrTreeRaw x_3 ((Subtype.val ∘ (↑x).snd) x_4) hq)) =
truei:Ii':Ig:i' ⟶ ib:F.Direction (↑x).fst ihb:F.rCurried (↑x).fst ↑b = ihqval:F.q (↑((↑x).snd ↑b)).head = ix✝:Decidable
(F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
↑b =
i)h✝:¬F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
↑b =
iheq✝:decI (F.rCurried (↑x).fst ↑b) i = isFalse h✝hthis:true = true⊢ (↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ (x_1 x_2 : I) (x_3 : x_2 ⟶ x_1) (x_4 : F.B (↑x).fst),
(match decI (F.rCurried (↑x).fst x_4) x_1 with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) x_4))) x_1 with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst x_3 ⟨x_4, hb⟩) =
F.wRestrTreeRaw x_3 ((Subtype.val ∘ (↑x).snd) x_4) hq)) =
truei:Ii':Ig:i' ⟶ ib:F.Direction (↑x).fst ihb:F.rCurried (↑x).fst ↑b = ihqval:F.q (↑((↑x).snd ↑b)).head = ix✝:Decidable
(F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
↑b =
i)hb✝:F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
↑b =
iheq✝:decI (F.rCurried (↑x).fst ↑b) i = isTrue hb✝hthis:(match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) ↑b))) i with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst g ⟨↑b, hb✝⟩) =
F.wRestrTreeRaw g ((Subtype.val ∘ (↑x).snd) ↑b) hq)) =
true⊢ (↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ (x_1 x_2 : I) (x_3 : x_2 ⟶ x_1) (x_4 : F.B (↑x).fst),
(match decI (F.rCurried (↑x).fst x_4) x_1 with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) x_4))) x_1 with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst x_3 ⟨x_4, hb⟩) =
F.wRestrTreeRaw x_3 ((Subtype.val ∘ (↑x).snd) x_4) hq)) =
truei:Ii':Ig:i' ⟶ ib:F.Direction (↑x).fst ihb:F.rCurried (↑x).fst ↑b = ihqval:F.q (↑((↑x).snd ↑b)).head = ix✝:Decidable
(F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
↑b =
i)h✝:¬F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
↑b =
iheq✝:decI (F.rCurried (↑x).fst ↑b) i = isFalse h✝hthis:true = true⊢ (↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯ exact absurd hb (I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ (x_1 x_2 : I) (x_3 : x_2 ⟶ x_1) (x_4 : F.B (↑x).fst),
(match decI (F.rCurried (↑x).fst x_4) x_1 with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) x_4))) x_1 with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst x_3 ⟨x_4, hb⟩) =
F.wRestrTreeRaw x_3 ((Subtype.val ∘ (↑x).snd) x_4) hq)) =
truei:Ii':Ig:i' ⟶ ib:F.Direction (↑x).fst ihb:F.rCurried (↑x).fst ↑b = ihqval:F.q (↑((↑x).snd ↑b)).head = ix✝:Decidable
(F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
↑b =
i)h✝:¬F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
↑b =
iheq✝:decI (F.rCurried (↑x).fst ↑b) i = isFalse h✝hthis:true = true⊢ ¬F.rCurried (↑x).fst ↑b = i All goals completed! 🐙)
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ (x_1 x_2 : I) (x_3 : x_2 ⟶ x_1) (x_4 : F.B (↑x).fst),
(match decI (F.rCurried (↑x).fst x_4) x_1 with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) x_4))) x_1 with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst x_3 ⟨x_4, hb⟩) =
F.wRestrTreeRaw x_3 ((Subtype.val ∘ (↑x).snd) x_4) hq)) =
truei:Ii':Ig:i' ⟶ ib:F.Direction (↑x).fst ihb:F.rCurried (↑x).fst ↑b = ihqval:F.q (↑((↑x).snd ↑b)).head = ix✝:Decidable
(F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
↑b =
i)hb✝:F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
↑b =
iheq✝:decI (F.rCurried (↑x).fst ↑b) i = isTrue hb✝hthis:(match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) ↑b))) i with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst g ⟨↑b, hb✝⟩) =
F.wRestrTreeRaw g ((Subtype.val ∘ (↑x).snd) ↑b) hq)) =
true⊢ (↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯ I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ (x_1 x_2 : I) (x_3 : x_2 ⟶ x_1) (x_4 : F.B (↑x).fst),
(match decI (F.rCurried (↑x).fst x_4) x_1 with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) x_4))) x_1 with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst x_3 ⟨x_4, hb⟩) =
F.wRestrTreeRaw x_3 ((Subtype.val ∘ (↑x).snd) x_4) hq)) =
truei:Ii':Ig:i' ⟶ ib:F.Direction (↑x).fst ihb:F.rCurried (↑x).fst ↑b = ihqval:F.q (↑((↑x).snd ↑b)).head = ix✝¹:Decidable
(F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
↑b =
i)hb✝:F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
↑b =
iheq✝¹:decI (F.rCurried (↑x).fst ↑b) i = isTrue hb✝x✝:Decidable
(F.q
(PFunctor.W.head
(⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 =
F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.snd
↑b).1) =
i)h✝:¬F.q
(PFunctor.W.head
(⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 =
F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.snd
↑b).1) =
iheq✝:decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) ↑b))) i = isFalse h✝hthis:true = true⊢ (↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ (x_1 x_2 : I) (x_3 : x_2 ⟶ x_1) (x_4 : F.B (↑x).fst),
(match decI (F.rCurried (↑x).fst x_4) x_1 with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) x_4))) x_1 with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst x_3 ⟨x_4, hb⟩) =
F.wRestrTreeRaw x_3 ((Subtype.val ∘ (↑x).snd) x_4) hq)) =
truei:Ii':Ig:i' ⟶ ib:F.Direction (↑x).fst ihb:F.rCurried (↑x).fst ↑b = ihqval:F.q (↑((↑x).snd ↑b)).head = ix✝¹:Decidable
(F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
↑b =
i)hb✝:F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
↑b =
iheq✝¹:decI (F.rCurried (↑x).fst ↑b) i = isTrue hb✝x✝:Decidable
(F.q
(PFunctor.W.head
(⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 =
F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.snd
↑b).1) =
i)hq✝:F.q
(PFunctor.W.head
(⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 =
F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.snd
↑b).1) =
iheq✝:decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) ↑b))) i = isTrue hq✝hthis:decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst g ⟨↑b, hb✝⟩) =
F.wRestrTreeRaw g ((Subtype.val ∘ (↑x).snd) ↑b) hq✝) =
true⊢ (↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ (x_1 x_2 : I) (x_3 : x_2 ⟶ x_1) (x_4 : F.B (↑x).fst),
(match decI (F.rCurried (↑x).fst x_4) x_1 with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) x_4))) x_1 with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst x_3 ⟨x_4, hb⟩) =
F.wRestrTreeRaw x_3 ((Subtype.val ∘ (↑x).snd) x_4) hq)) =
truei:Ii':Ig:i' ⟶ ib:F.Direction (↑x).fst ihb:F.rCurried (↑x).fst ↑b = ihqval:F.q (↑((↑x).snd ↑b)).head = ix✝¹:Decidable
(F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
↑b =
i)hb✝:F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
↑b =
iheq✝¹:decI (F.rCurried (↑x).fst ↑b) i = isTrue hb✝x✝:Decidable
(F.q
(PFunctor.W.head
(⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 =
F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.snd
↑b).1) =
i)h✝:¬F.q
(PFunctor.W.head
(⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 =
F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.snd
↑b).1) =
iheq✝:decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) ↑b))) i = isFalse h✝hthis:true = true⊢ (↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯ exact absurd hqval (I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ (x_1 x_2 : I) (x_3 : x_2 ⟶ x_1) (x_4 : F.B (↑x).fst),
(match decI (F.rCurried (↑x).fst x_4) x_1 with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) x_4))) x_1 with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst x_3 ⟨x_4, hb⟩) =
F.wRestrTreeRaw x_3 ((Subtype.val ∘ (↑x).snd) x_4) hq)) =
truei:Ii':Ig:i' ⟶ ib:F.Direction (↑x).fst ihb:F.rCurried (↑x).fst ↑b = ihqval:F.q (↑((↑x).snd ↑b)).head = ix✝¹:Decidable
(F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
↑b =
i)hb✝:F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
↑b =
iheq✝¹:decI (F.rCurried (↑x).fst ↑b) i = isTrue hb✝x✝:Decidable
(F.q
(PFunctor.W.head
(⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 =
F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.snd
↑b).1) =
i)h✝:¬F.q
(PFunctor.W.head
(⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 =
F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.snd
↑b).1) =
iheq✝:decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) ↑b))) i = isFalse h✝hthis:true = true⊢ ¬F.q (↑((↑x).snd ↑b)).head = i All goals completed! 🐙)
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ (x_1 x_2 : I) (x_3 : x_2 ⟶ x_1) (x_4 : F.B (↑x).fst),
(match decI (F.rCurried (↑x).fst x_4) x_1 with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) x_4))) x_1 with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst x_3 ⟨x_4, hb⟩) =
F.wRestrTreeRaw x_3 ((Subtype.val ∘ (↑x).snd) x_4) hq)) =
truei:Ii':Ig:i' ⟶ ib:F.Direction (↑x).fst ihb:F.rCurried (↑x).fst ↑b = ihqval:F.q (↑((↑x).snd ↑b)).head = ix✝¹:Decidable
(F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
↑b =
i)hb✝:F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
↑b =
iheq✝¹:decI (F.rCurried (↑x).fst ↑b) i = isTrue hb✝x✝:Decidable
(F.q
(PFunctor.W.head
(⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 =
F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.snd
↑b).1) =
i)hq✝:F.q
(PFunctor.W.head
(⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 =
F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.snd
↑b).1) =
iheq✝:decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) ↑b))) i = isTrue hq✝hthis:decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst g ⟨↑b, hb✝⟩) =
F.wRestrTreeRaw g ((Subtype.val ∘ (↑x).snd) ↑b) hq✝) =
true⊢ (↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯ I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ (x_1 x_2 : I) (x_3 : x_2 ⟶ x_1) (x_4 : F.B (↑x).fst),
(match decI (F.rCurried (↑x).fst x_4) x_1 with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) x_4))) x_1 with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst x_3 ⟨x_4, hb⟩) =
F.wRestrTreeRaw x_3 ((Subtype.val ∘ (↑x).snd) x_4) hq)) =
truei:Ii':Ig:i' ⟶ ib:F.Direction (↑x).fst ihb:F.rCurried (↑x).fst ↑b = ihqval:F.q (↑((↑x).snd ↑b)).head = ix✝¹:Decidable
(F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
↑b =
i)hb✝:F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
↑b =
iheq✝¹:decI (F.rCurried (↑x).fst ↑b) i = isTrue hb✝x✝:Decidable
(F.q
(PFunctor.W.head
(⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 =
F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.snd
↑b).1) =
i)hq✝:F.q
(PFunctor.W.head
(⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 =
F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.snd
↑b).1) =
iheq✝:decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) ↑b))) i = isTrue hq✝hthis:(Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst g ⟨↑b, hb✝⟩) = F.wRestrTreeRaw g ((Subtype.val ∘ (↑x).snd) ↑b) hq✝⊢ (↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯
All goals completed! 🐙
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)⊢ (∀ ⦃i i' : I⦄ (g : i' ⟶ i) (b : F.Direction (↑x).fst i),
(↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯) →
∀ (x_1 x_2 : I) (x_3 : x_2 ⟶ x_1) (x_4 : F.B (↑x).fst),
(match decI (F.rCurried (↑x).fst x_4) x_1 with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) x_4))) x_1 with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst x_3 ⟨x_4, hb⟩) =
F.wRestrTreeRaw x_3 ((Subtype.val ∘ (↑x).snd) x_4) hq)) =
true I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ ⦃i i' : I⦄ (g : i' ⟶ i) (b : F.Direction (↑x).fst i),
(↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯i:Ii':Ig:i' ⟶ ib':F.B (↑x).fst⊢ (match decI (F.rCurried (↑x).fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) b'))) i with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst g ⟨b', hb⟩) =
F.wRestrTreeRaw g ((Subtype.val ∘ (↑x).snd) b') hq)) =
true
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ ⦃i i' : I⦄ (g : i' ⟶ i) (b : F.Direction (↑x).fst i),
(↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯i:Ii':Ig:i' ⟶ ib':F.B (↑x).fstx✝:Decidable
(F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
b' =
i)h✝:¬F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
b' =
iheq✝:decI (F.rCurried (↑x).fst b') i = isFalse h✝⊢ true = trueI:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ ⦃i i' : I⦄ (g : i' ⟶ i) (b : F.Direction (↑x).fst i),
(↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯i:Ii':Ig:i' ⟶ ib':F.B (↑x).fstx✝:Decidable
(F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
b' =
i)hb✝:F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
b' =
iheq✝:decI (F.rCurried (↑x).fst b') i = isTrue hb✝⊢ (match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) b'))) i with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst g ⟨b', hb✝⟩) =
F.wRestrTreeRaw g ((Subtype.val ∘ (↑x).snd) b') hq)) =
true
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ ⦃i i' : I⦄ (g : i' ⟶ i) (b : F.Direction (↑x).fst i),
(↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯i:Ii':Ig:i' ⟶ ib':F.B (↑x).fstx✝:Decidable
(F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
b' =
i)h✝:¬F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
b' =
iheq✝:decI (F.rCurried (↑x).fst b') i = isFalse h✝⊢ true = true All goals completed! 🐙
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ ⦃i i' : I⦄ (g : i' ⟶ i) (b : F.Direction (↑x).fst i),
(↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯i:Ii':Ig:i' ⟶ ib':F.B (↑x).fstx✝:Decidable
(F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
b' =
i)hb✝:F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
b' =
iheq✝:decI (F.rCurried (↑x).fst b') i = isTrue hb✝⊢ (match decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) b'))) i with
| isFalse h => true
| isTrue hq =>
decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst g ⟨b', hb✝⟩) =
F.wRestrTreeRaw g ((Subtype.val ∘ (↑x).snd) b') hq)) =
true I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ ⦃i i' : I⦄ (g : i' ⟶ i) (b : F.Direction (↑x).fst i),
(↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯i:Ii':Ig:i' ⟶ ib':F.B (↑x).fstx✝¹:Decidable
(F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
b' =
i)hb✝:F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
b' =
iheq✝¹:decI (F.rCurried (↑x).fst b') i = isTrue hb✝x✝:Decidable
(F.q
(PFunctor.W.head
(⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 =
F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.snd
b').1) =
i)h✝:¬F.q
(PFunctor.W.head
(⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 =
F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.snd
b').1) =
iheq✝:decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) b'))) i = isFalse h✝⊢ true = trueI:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ ⦃i i' : I⦄ (g : i' ⟶ i) (b : F.Direction (↑x).fst i),
(↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯i:Ii':Ig:i' ⟶ ib':F.B (↑x).fstx✝¹:Decidable
(F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
b' =
i)hb✝:F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
b' =
iheq✝¹:decI (F.rCurried (↑x).fst b') i = isTrue hb✝x✝:Decidable
(F.q
(PFunctor.W.head
(⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 =
F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.snd
b').1) =
i)hq✝:F.q
(PFunctor.W.head
(⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 =
F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.snd
b').1) =
iheq✝:decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) b'))) i = isTrue hq✝⊢ decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst g ⟨b', hb✝⟩) =
F.wRestrTreeRaw g ((Subtype.val ∘ (↑x).snd) b') hq✝) =
true
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ ⦃i i' : I⦄ (g : i' ⟶ i) (b : F.Direction (↑x).fst i),
(↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯i:Ii':Ig:i' ⟶ ib':F.B (↑x).fstx✝¹:Decidable
(F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
b' =
i)hb✝:F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
b' =
iheq✝¹:decI (F.rCurried (↑x).fst b') i = isTrue hb✝x✝:Decidable
(F.q
(PFunctor.W.head
(⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 =
F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.snd
b').1) =
i)h✝:¬F.q
(PFunctor.W.head
(⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 =
F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.snd
b').1) =
iheq✝:decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) b'))) i = isFalse h✝⊢ true = true All goals completed! 🐙
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ ⦃i i' : I⦄ (g : i' ⟶ i) (b : F.Direction (↑x).fst i),
(↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯i:Ii':Ig:i' ⟶ ib':F.B (↑x).fstx✝¹:Decidable
(F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
b' =
i)hb✝:F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
b' =
iheq✝¹:decI (F.rCurried (↑x).fst b') i = isTrue hb✝x✝:Decidable
(F.q
(PFunctor.W.head
(⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 =
F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.snd
b').1) =
i)hq✝:F.q
(PFunctor.W.head
(⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 =
F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.snd
b').1) =
iheq✝:decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) b'))) i = isTrue hq✝⊢ decide
((Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst g ⟨b', hb✝⟩) =
F.wRestrTreeRaw g ((Subtype.val ∘ (↑x).snd) b') hq✝) =
true I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ ⦃i i' : I⦄ (g : i' ⟶ i) (b : F.Direction (↑x).fst i),
(↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯i:Ii':Ig:i' ⟶ ib':F.B (↑x).fstx✝¹:Decidable
(F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
b' =
i)hb✝:F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
b' =
iheq✝¹:decI (F.rCurried (↑x).fst b') i = isTrue hb✝x✝:Decidable
(F.q
(PFunctor.W.head
(⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 =
F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.snd
b').1) =
i)hq✝:F.q
(PFunctor.W.head
(⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 =
F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.snd
b').1) =
iheq✝:decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) b'))) i = isTrue hq✝⊢ (Subtype.val ∘ (↑x).snd) ↑(F.directionRestr (↑x).fst g ⟨b', hb✝⟩) = F.wRestrTreeRaw g ((Subtype.val ∘ (↑x).snd) b') hq✝
exact (congrArg Subtype.val (H g ⟨b', I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ ⦃i i' : I⦄ (g : i' ⟶ i) (b : F.Direction (↑x).fst i),
(↑x).snd ↑(F.directionRestr (↑x).fst g b) = F.wRestrTree g ((↑x).snd ↑b) ⋯i:Ii':Ig:i' ⟶ ib':F.B (↑x).fstx✝¹:Decidable
(F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
b' =
i)hb✝:F.rCurried
⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.fst
b' =
iheq✝¹:decI (F.rCurried (↑x).fst b') i = isTrue hb✝x✝:Decidable
(F.q
(PFunctor.W.head
(⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 =
F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.snd
b').1) =
i)hq✝:F.q
(PFunctor.W.head
(⟨(↑x).fst, fun b ↦
((Subtype.val ∘ (↑x).snd) b,
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide
((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 =
F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b))⟩.snd
b').1) =
iheq✝:decI (F.q (PFunctor.W.head ((Subtype.val ∘ (↑x).snd) b'))) i = isTrue hq✝⊢ F.DirectionOver (↑x).fst i b' All goals completed! 🐙⟩)).trans
(F.wRestrTree_val g (x.1.2 b') _)
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)⊢ ((FinEnum.toList (F.B (↑x).fst)).all fun b' ↦
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide ((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b')) =
true ↔
∀ (b : F.B (↑x).fst), F.IsHereditarilyNatural ((↑x).snd b) I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)⊢ (∀ x_1 ∈ FinEnum.toList (F.B (↑x).fst),
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide ((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) x_1) =
true) ↔
∀ (b : F.B (↑x).fst), F.IsHereditarilyNatural ((↑x).snd b)
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)⊢ (∀ x_1 ∈ FinEnum.toList (F.B (↑x).fst),
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide ((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) x_1) =
true) →
∀ (b : F.B (↑x).fst), F.IsHereditarilyNatural ((↑x).snd b)I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)⊢ (∀ (b : F.B (↑x).fst), F.IsHereditarilyNatural ((↑x).snd b)) →
∀ x_1 ∈ FinEnum.toList (F.B (↑x).fst),
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide ((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) x_1) =
true
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)⊢ (∀ x_1 ∈ FinEnum.toList (F.B (↑x).fst),
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide ((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) x_1) =
true) →
∀ (b : F.B (↑x).fst), F.IsHereditarilyNatural ((↑x).snd b) I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ x_1 ∈ FinEnum.toList (F.B (↑x).fst),
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide ((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) x_1) =
trueb:F.B (↑x).fst⊢ F.IsHereditarilyNatural ((↑x).snd b)
All goals completed! 🐙
I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)⊢ (∀ (b : F.B (↑x).fst), F.IsHereditarilyNatural ((↑x).snd b)) →
∀ x_1 ∈ FinEnum.toList (F.B (↑x).fst),
WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide ((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) x_1) =
true I:Type uIinst✝:Category.{vI, uI} IF:PresheafPFunctor I IdecI:DecidableEq IfeI:FinEnum IfeHom:(i i' : I) → FinEnum (i' ⟶ i)feB:(a : F.A) → FinEnum (F.B a)decEqW:DecidableEq (WType F.B)z:F.toSlicePFunctor.Wx:F.toSlicePFunctor.Obj F.toSlicePFunctor.wIndexih:∀ (b : F.toSlicePFunctor.B (↑x).fst),
F.isHereditarilyNaturalBoolCore decI feI feHom feB decEqW ↑((↑x).snd b) = true ↔ F.IsHereditarilyNatural ((↑x).snd b)H:∀ (b : F.B (↑x).fst), F.IsHereditarilyNatural ((↑x).snd b)b':F.B (↑x).fsta✝:b' ∈ FinEnum.toList (F.B (↑x).fst)⊢ WType.para Bool
(fun x ↦
((FinEnum.toList I).all fun i ↦
(FinEnum.toList I).all fun i' ↦
(FinEnum.toList (i' ⟶ i)).all fun g ↦
(FinEnum.toList (F.B x.fst)).all fun b' ↦
match decI (F.rCurried x.fst b') i with
| isFalse h => true
| isTrue hb =>
match decI (F.q (PFunctor.W.head (x.snd b').1)) i with
| isFalse h => true
| isTrue hq =>
decide ((x.snd ↑(F.directionRestr x.fst g ⟨b', hb⟩)).1 = F.wRestrTreeRaw g (x.snd b').1 hq)) &&
(FinEnum.toList (F.B x.fst)).all fun b' ↦ (x.snd b').2)
((Subtype.val ∘ (↑x).snd) b') =
true
All goals completed! 🐙Hereditary naturality of a slice W-tree is decidable.
instance decidableIsHereditarilyNatural {I : Type uI} [Category.{vI} I]
(F : PresheafPFunctor.{uI, uI, uA, uB, vI, vI} I I)
[F.Finitary] [FinEnum I] [∀ i i' : I, FinEnum (i' ⟶ i)]
[DecidableEq F.A] (z : F.toSlicePFunctor.W) :
Decidable (F.IsHereditarilyNatural z) :=
decidable_of_iff _ (F.isHereditarilyNaturalBoolCore_eq_true_iff inferInstance inferInstance
inferInstance inferInstance inferInstance z)end PresheafPFunctor