Quantification on subshapes forgets the super-shape

[kyoDralliam]

The following quantification on the 3-2-horn

#def hom-Λ³₂
  (A : U)
  (w x y z : A)
  (f : hom A w x)
  (g : hom A x y)
  (h : hom A y z)
  (k : hom A w y)
  (l : hom A x z)
  (m : hom A w z)
  (α : hom2 A w x y f g k)
  (β : hom2 A x y z g h l)
  (δ : hom2 A w y z k h m)
  : U
  :=
    (((t1,t2),t3) : Λ³₂) → A[
      t3 ≡ 0₂ ↦ α (t1, t2),
      t1 ≡ 1₂ ↦ β (t2, t3),
      t1 ≡ t2 ↦ δ (t1, t3)
    ]

fails with the following error:

local context is not included in (does not entail) the tope
  Δ² (π₁ (π₁ x₁), π₂ (π₁ x₁))
in local context (normalised)
  π₂ x₁ ≡ 0₂ : TOPE
  π₂ x₁ ≡ 0₂ ∨ π₁ (π₁ x₁) ≡ π₂ (π₁ x₁) ∨ π₁ (π₁ x₁) ≡ 1₂ : TOPE
  ⊤ : TOPE



  Error occurred when checking
    #define hom-Λ³₂

Local tope context:
    π₂ x₁ ≡ 0₂
    Λ³₂ x₁

when checking if local context
  π₂ x₁ ≡ 0₂
  Λ³₂ x₁
  ⊤
is included in (entails) the tope
  Δ² (π₁ (π₁ x₁), π₂ (π₁ x₁))

when inferring type for term
  α (π₁ (π₁ x₁), π₂ (π₁ x₁))

when typechecking
  α (π₁ (π₁ x₁), π₂ (π₁ x₁))
against type
  A
[...]
  f : hom A w x
  g : hom A x y
  h : hom A y z
  k : hom A w y
  l : hom A x z
  m : hom A w z
  α : hom2 A w x y f g k
  β : hom2 A x y z g h l
  δ : hom2 A w y z k h m
  x₁ : 2 × 2 × 2

while its expanded version typechecks correctly

#def hom-Λ³₂
  (A : U)
  (w x y z : A)
  (f : hom A w x)
  (g : hom A x y)
  (h : hom A y z)
  (k : hom A w y)
  (l : hom A x z)
  (m : hom A w z)
  (α : hom2 A w x y f g k)
  (β : hom2 A x y z g h l)
  (δ : hom2 A w y z k h m)
  : U
  :=
  (((t1,t2),t3) : 2 × 2 × 2 | Λ³₂ ((t1,t2), t3)) → A[
      t3 ≡ 0₂ ↦ α (t1, t2),
      t1 ≡ 1₂ ↦ β (t2, t3),
      t1 ≡ t2 ↦ δ (t1, t3)
    ]

where the 3-2-horn is defined as

#def Λ³₂ : Δ³ → TOPE
  := \ ((t1, t2), t3) → t3 ≡ 0₂ ∨ t1 ≡ t2 ∨ t1 ≡ 1₂

It looks like the fact that Λ³₂ is a subshape of Δ³ has been forgotten in the abrreviated version

[fizruk]

Thanks for reporting! This is connected to #110 and #111, and I believe has the same underlying cause. I am hoping to get this sorted out in the next release.