DTT

Stream: general

[Sebastien Gouezel]

Trying my hands on multilinear forms with dependent types, as @Patrick Massot asked when reviewing #1814. Very quickly, I run into issues such as the following one.

import linear_algebra.basic
open function fin set
/-- Embedding a type `α` in a type `β`, covering all of `β` but one element `i` called the hole. -/
structure embed_but_one (α : Type u) (β : Type v) :=
(to_fun : α → β)
(inj_to_fun : injective to_fun)
(hole : β)
(range : range to_fun = univ - {hole})

def cons {α : Type u} {β : Type v} {γ : β → Type w} (e : embed_but_one α β)
  (f : Π(a : α), γ (e a)) (x : γ (e.hole)) : Π(b : β), γ b :=
λb, sorry

I have an injective map from α to β whose range is everything but a hole. I want to glue together a map on α and a value on the hole, to get a map on β. If my target is a single type, this is easy to do. But if it goes in a dependent type, then one needs to convince at every step Lean that one is in the right type, using casts all over the place. Is there a nice way to do this, or should I just drop dependent types because usually multilinear maps are defined on n copies of the same space?

[Kevin Buzzard]

I know less about dependent type theory than you do but can you define a map from beta to option alpha and a map from option alpha to the dependent type? Or does this not solve the problem?