I have a definition of a path in a quiver. Here `A`

and `B`

are supposed to be thought of as the type of nodes and edges respectively

```
Inductive tlist (A : Type) ( B : A -> A -> Type) (k : A) : A -> Type :=
| tnil : tlist k
| tcons i j : tlist j -> B i j -> tlist i.
```

i am trying to prove a goal of the form

```
i : A
f : tlist i i
H : match f with tnil => True | tcons _ _ => False end
----------
tnil i = f
```

and I am stuck. I cannot destruct f because it complains about it being ill-typed as it tries to abstract the annotation in `tlist`

, so then `f`

becomes of type `tlist i j`

for some new variable `j`

and `tnil i`

is of type `tlist i i`

so the equation is not well typed. I have been trying to use 'remember' and similar tactics to decouple `i`

and `j`

with the idea that i could transport across the equality but this has not been helpful, the dilemma seems to be that at some point I have to destruct the equality too. If I destruct f first then I am left with a branch of the form `tnil = transport p tnil`

where `p : i = i`

, and I cannot destruct p without the equality being ill-typed. I guess this is where assuming UIP as an axiom comes in handy, but I am looking for a way to do it without this

Inversion is not helpful as in the nil case it just returns the equality `i = i`

I guess it boils down to

```
Context (A : Type).
Context (pt : A).
Inductive P : A -> Type :=
| c : P pt.
Goal forall (H : P pt), H = c.
```
```

```
Inductive tlist (A : Type) ( B : A -> A -> Type) (k : A) : A -> Type :=
| tnil : tlist k
| tcons i j : tlist j -> B i j -> tlist i.
```

says `The term "k" has type "A" while it is expected to have type "Type".`

Gaëtan Gilbert said:

`Inductive tlist (A : Type) ( B : A -> A -> Type) (k : A) : A -> Type := | tnil : tlist k | tcons i j : tlist j -> B i j -> tlist i.`

says

`The term "k" has type "A" while it is expected to have type "Type".`

Ok, sorry, I must have screwed up copying it. I will edit the message

I am left with a branch of the form tnil = transport p tnil where p : i = i, and I cannot destruct p without the equality being ill-typed. I guess this is where assuming UIP as an axiom comes in handy

note that in this case p is an equality between nats, and uip for nat it true (Eqdep_dec.UIP_refl_nat)

```
Context (A : Type) (B : A -> A -> Type).
Inductive tlist' (k : A) : A -> Type :=
| tnil : tlist' k
| tcons : ∀ i j : A, B i j -> tlist' j -> tlist' i.
Definition tlist_is_nil (i : A) (f : tlist' i i) :=
match f return Type with tnil _ => True | tcons _ _ _ _ _ => False end.
Proposition tlist_quiver_nilcase (i : A) (f : tlist' i i) (H : tlist_is_nil i f) : tnil i = f.
```

I think this is a self contained version of what I am trying to prove

Gaëtan Gilbert said:

I am left with a branch of the form tnil = transport p tnil where p : i = i, and I cannot destruct p without the equality being ill-typed. I guess this is where assuming UIP as an axiom comes in handy

note that in this case p is an equality between nats, and uip for nat it true (Eqdep_dec.UIP_refl_nat)

I see, ok. Are you suggest I convert the lists to their lengths or something? I don't understand what you mean by nats

I guess it boils down to

that is one way to state UIP

```
Section S.
Context (A : Type).
Context (pt : A).
Inductive P : A -> Type :=
| c : P pt.
Axiom thing : forall (H : P pt), H = c.
Definition to_eq {y} (e:P y) : pt = y := match e with c => eq_refl end.
Definition from_eq {y} (e:pt = y) : P y := match e with eq_refl => c end.
Lemma to_from_eq {y} e : to_eq (@from_eq y e) = e.
Proof.
destruct e;reflexivity.
Qed.
Theorem uip (e:pt=pt) : e = eq_refl.
Proof.
rewrite <-(to_from_eq e).
change eq_refl with (to_eq c).
f_equal.
apply thing.
Qed.
End S.
```

Patrick Nicodemus said:

Gaëtan Gilbert said:

I am left with a branch of the form tnil = transport p tnil where p : i = i, and I cannot destruct p without the equality being ill-typed. I guess this is where assuming UIP as an axiom comes in handy

note that in this case p is an equality between nats, and uip for nat it true (Eqdep_dec.UIP_refl_nat)

I see, ok. Are you suggest I convert the lists to their lengths or something? I don't understand what you mean by nats

sorry, I misread and thought i:nat

I see, that's really interesting. I will have to remember that equivalence.

P is exactly the same as `@eq A pt`

just with a different name

Yeah I just realized that. It took me a minute.

I guess the way I have defined my inductive type of paths in the graph, an empty list of edges starting at node `i`

is essentially equivalent to a proof of `i = i`

and so I won't be able to prove that there's a unique empty list `tnil`

without assuming `A`

satisfies axiom `K`

you can turn your inductive into an equivalent one (up to isomorphism) by turning indices into (non uniform) parameters and adding equalities:

```
Inductive tlist' (k : A) (k' : A) : Type :=
| tnil : k = k' -> tlist' k k'
| tcons : ∀ i j : A, B i j -> tlist' k j -> i = k' -> tlist' k k '.
```

optionally you can then simplify if you have the pattern `forall i, ... -> i = k' -> ...`

to remove i and just use k' in that constructor (because `{i & i = k'}`

is contractible) getting

```
Inductive tlist' (k : A) (k' : A) : Type :=
| tnil : k = k' -> tlist' k k'
| tcons : ∀ j : A, B i j -> tlist' k j -> tlist' k k '.
```

I see what you're saying.

Patrick Nicodemus has marked this topic as resolved.

Last updated: Jun 25 2024 at 15:02 UTC