> Thorsten Altenkirch wrote:
>
> Conor McBride wrote:
>
> > Sebastian Hanowski wrote:
> >
> > > ( f : Fin (suc m) -> Fin (suc n) !
> > > let !-----------------------------------!
> > > ! restrict _m _n f : Fin m -> Fin n )
> > >
> >
> > Should you be able to write a function with this type? I can
> > certainly write a function from Fin 2 to Fin 1, but I shouldn't be
> > able to extract a function from Fin 1 to Fin 0.
That's why i need this awkward call.
> Just for the record: I suggested to show:
>
> f : Fin (suc m) -> Fin (suc n); Injective f
> ------------------------------------------------------------
> restrict f : (f' : Fin m -> Fin n; Injective f')
>
> in freely invented syntax.
>
> T.
Which is easy to show, if you have the 'unrestricted' restrict:
------------------------------------------------------------------------
( p : !
! Sigma (Fin (suc m) -> Fin (suc n)) !
! % (lam f => all i, j => (f i = f j) -> i = j) !
let !----------------------------------------------------!
! lemma _m _n p : !
! Sigma (Fin m -> Fin n) !
! % (lam f' => all i, j => (f' i = f' j) -> i = j) )
lemma _ m _ n p <= case p
{ lemma _ m _ n (pair a b)
=> pair (restrict a) (lam i, j => b (fs i) (fs j))
}
------------------------------------------------------------------------
> > I fear max-or-weak may not be terribly helpful here: my suspicion
> > (not having prepared a solution) is that viewing things as i or
> > (thin i j) might help.
max-or-weak is just used for the cast of a (f i):Fin (suc n) to a
j:Fin n. Since you only have to peel off a constructor from (fMax_n),
max-or-weak comes in handy.
On the other hand, it should be possible to eschew Maybe, since
(fWeak i) is just (thin (fMax_m) i). It would require (maps2Max f) to
return (fMax_m) in case of nothing get's mapped to (fMax_n). We could
then have:
f' i = downcast (f (thin (maps2Max f) i))
Best Regards,
Sebastian
