I am trying to build an inductive type for cobordism using Coq in such way that some properties of cobordism (1-groupoid and 2-groupoid) can be proved. I am using the following Coq code:
Unset Automatic Introduction.
Inductive Topo : Set := t | nt.
Definition F (i j : Topo) :=
match i, j with
| t, t => t
| t, nt => nt
| nt, t => nt
| nt, nt => nt
end.
I am considering two kinds of topologies for the cobordisms : trivial (t) and nontrivial (nt). The trivial cobordisms is the cylinder considered like the unit in the 1-groupoid. The function F gives the composition of topologies.
The inductive type of cobordism is assumed as:
Inductive cobordisms {A} : A -> A -> Topo -> Type := idcobordism : forall
x : A, cobordisms x x t.
with the tactics:
Hint Resolve @idcobordism.
Ltac cobordism_induction :=
intros; repeat progress (
match goal with
| [ p : cobordisms _ _ _ |- _ ] => induction p
| _ => idtac
end
); auto.
The composition of cobordisms is introduced according with:
Definition concat {A} {x y z : A} {i j : Topo} : cobordisms x y i -> cobordisms y z j
-> cobordisms x z (F i j) .
Proof.
cobordism_induction.
Defined.
Notation "p @ q" := (concat p q) (at level 60).
The inverse of a given cobordism is defined by:
Definition opposite {A} {x y : A} {i : Topo} : cobordisms x y i -> cobordisms y x i .
Proof.
cobordism_induction.
Defined.
Notation "! p" := (opposite p) (at level 50).
Until now all is okay. But when I am trying to prove the firs property of the 1-groupid, namely, left unity:
Lemma idcobordism_left_unit A (x y : A) (i : Topo) (p : cobordisms x y i) :
(idcobordism x) @ p = p.
I am obtaining the following error message:
Error: In environment
A : Type
x : A
y : A
i : Topo
p : cobordisms x y i
The term "p" has type "cobordisms x y i" while it is expected to have type
"cobordisms x y (F t i)".
Then my question is, how to make that Coq consider that (F t i) is equivalent to i for all i according with the previous definition of F?
The problem is that your definition of F always makes a match on its second argument, even when it's not required. Because of this, F t i and i will not be definitionally equal when i is not a constructor. The solution is to change the definition of F so that the equality you want becomes manifest:
Definition F (i j : Topo) :=
match i with
| t => j
| nt => nt
end.
Unfortunately, you won't be able to perform the same trick when showing the right identity, since then you would have the converse problem. In that case, the solution would be to use an explicit cast to relate both paths:
Definition cast_cb {A} {x y : A} i : cobordisms x y (F i t) -> cobordisms x y i :=
match i with t => fun x => x | nt => fun x => x end.
Lemma right_id A (x y : A) i (p : cobordisms x y i) :
cast_cb i (p @ (idcobordism y)) = p.