test(tests/lean/hott): add test for no_confusion construction for HoTT

tests/lean/hott/sig_noc.hlean

@@ -0,0 +1,45 @@
+namespace sigma
+  open lift
+  open sigma.ops
+  variables {A : Type} {B : A → Type}
+
+  variables {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂}
+
+  definition dpair.inj (H : ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩) : Σ (e₁ : a₁ = a₂), eq.rec b₁ e₁ = b₂ :=
+  down (no_confusion H (λ e₁ e₂, ⟨e₁, e₂⟩))
+
+  definition dpair.inj₁ (H : ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩) : a₁ = a₂ :=
+  (dpair.inj H).1
+
+  definition dpair.inj₂ (H : ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩) : eq.rec b₁ (dpair.inj₁ H) = b₂ :=
+  (dpair.inj H).2
+
+end sigma
+
+structure foo :=
+mk :: (A : Type) (B : A → Type) (a : A) (b : B a)
+
+set_option pp.implicit true
+
+namespace foo
+  open lift sigma.ops
+  universe variables l₁ l₂
+  variables {A₁ : Type.{l₁}} {B₁ : A₁ → Type.{l₂}} {a₁ : A₁} {b₁ : B₁ a₁}
+  variables {A₂ : Type.{l₁}} {B₂ : A₂ → Type.{l₂}} {a₂ : A₂} {b₂ : B₂ a₂}
+
+  definition foo.inj (H : mk A₁ B₁ a₁ b₁ = mk A₂ B₂ a₂ b₂) :
+    Σ (e₁ : A₁ = A₂) (e₂ : eq.rec B₁ e₁ = B₂) (e₃ : eq.rec a₁ e₁ = a₂), eq.rec (eq.rec (eq.rec b₁ e₁) e₂) e₃ = b₂ :=
+  down (no_confusion H (λ e₁ e₂ e₃ e₄, ⟨e₁, e₂, e₃, e₄⟩))
+
+  definition foo.inj₁ (H : mk A₁ B₁ a₁ b₁ = mk A₂ B₂ a₂ b₂) : A₁ = A₂ :=
+  (foo.inj H).1
+
+  definition foo.inj₂ (H : mk A₁ B₁ a₁ b₁ = mk A₂ B₂ a₂ b₂) : eq.rec B₁ (foo.inj₁ H) = B₂ :=
+  (foo.inj H).2.1
+
+  definition foo.inj₃ (H : mk A₁ B₁ a₁ b₁ = mk A₂ B₂ a₂ b₂) : eq.rec a₁ (foo.inj₁ H) = a₂ :=
+  (foo.inj H).2.2.1
+
+  definition foo.inj₄ (H : mk A₁ B₁ a₁ b₁ = mk A₂ B₂ a₂ b₂) : eq.rec (eq.rec (eq.rec b₁ (foo.inj₁ H)) (foo.inj₂ H)) (foo.inj₃ H) = b₂ :=
+  (foo.inj H).2.2.2
+end foo