(***** we define H^1 in an intuitionistic type-theory setting;
we show the first stage of the long exact sequence, saying that
H^1 being trivial gives surjectivity of a map on a space of sections ***)

(**** Carlos Simpson CNRS, Universit\'e de Nice-Sophia Antipolis
   carlos@math.unice.fr *******************************************)


Set Implicit Arguments.
Unset Strict Implicit.




Implicit Arguments ex [A].

Definition mark (X : Type) (x : X) := x.




Theorem plug : forall (a b : Type) (h : a -> b) (u v : a), u = v -> h u = h v.
Proof. 
intros. rewrite H. trivial.
Qed.

Inductive JMeqT (A : Type) (a : A) : forall (B : Type) (b : B), Prop :=
    JMeqT_refl : JMeqT a a.

Infix "-=-" := JMeqT (left associativity, at level 96).

Axiom JMeqT_eqT : forall (A : Type) (a b : A), (a -=- b) -> a = b.

Theorem eqT_JMeqT : forall (A : Type) (a b : A), a = b -> (a -=- b).
Proof. 
intros. rewrite H. eapply JMeqT_refl. 
Qed.


Parameter eqT_rect : forall A B : Type, A = B -> A -> B.
Axiom
  eqT_rect_JMeqT :
    forall (A B : Type) (hyp : A = B) (a : A), eqT_rect hyp a -=- a.


Axiom proof_irrelevance : forall (P : Prop) (p q : P), p = q.

Axiom
  extensionality :
    forall (x : Type) (f : x -> Type) (u v : forall y : x, f y),
    (forall y : x, u y = v y) -> u = v.

Definition type_of (T : Type) (t : T) := T.


Theorem eqT_utility :
 forall (X : Type) (P : forall (a b : X) (hyp : a = b), Prop) 
   (a b : X) (hyp : a = b), P a a (refl_equal a) -> P a b hyp.
Proof. 
intros.
generalize hyp.
induction hyp.
intros.
assert (refl_equal a = hyp).
eapply proof_irrelevance.

rewrite <- H0.
assumption.
Qed.




Inductive nonempty (T : Type) : Prop :=
    nonempty_intro : T -> nonempty T.

Record has_one_element (T : Type) : Prop := 
  {one_nonempty : nonempty T; one_unique : forall a b : T, a = b}.

Inductive ONE : Type :=
    pt : ONE.

Theorem ONE_has_one_element : has_one_element ONE.
Proof. 
eapply Build_has_one_element.
eapply nonempty_intro.
exact pt.

intros.
induction a; induction b.
trivial.
Qed.


Record virtual (X : Type) : Type := 
  {carrier : Type;
   virt_touch :> carrier -> X;
   virt_nonempty : nonempty carrier;
   virt_equal : forall v w : carrier, virt_touch v = virt_touch w}.

Definition virtualize : forall X : Type, X -> virtual X.
intros.
eapply (Build_virtual (X:=X) (carrier:=ONE) (virt_touch:=fun u : ONE => X0)).
eapply (nonempty_intro pt).

intros.
trivial.
Defined.


Record description (X : Type) : Type := 
  {the_description :> virtual X -> X;
   description_eq :
    forall (v : virtual X) (x : carrier v), the_description v = v x}.

Definition use_description :
  forall (X : Type) (de : description X) (Y : Type) 
    (t : Y -> X) (ne : nonempty Y) (e : forall y z : Y, t y = t z), X.
intros.
set (V := Build_virtual (X:=X) (carrier:=Y) (virt_touch:=t) ne e) in *.
exact (de V).
Defined.

Theorem use_description_eq :
 forall (X : Type) (de : description X) (Y : Type) 
   (t : Y -> X) (ne : nonempty Y) (e : forall y z : Y, t y = t z) 
   (y : Y), use_description de ne e = t y.
Proof. 
intros.
unfold use_description in |- *.
set (V := Build_virtual ne e) in *.
set (K := description_eq (X:=X) de (v:=V) y) in *.
rewrite K.
trivial.
Qed.

(********** quotients ***********)


Definition TypeQ := Type.

Parameter quotient : forall (r x : Type) (p1 p2 : r -> x), Type.

Definition quotient_fix_universe :
  forall (r x : TypeQ) (p1 p2 : r -> x), TypeQ := quotient.
(*Implicits quotient [1 2].*)

Parameter
  quotient_map : forall (r x : Type) (p1 p2 : r -> x), x -> quotient p1 p2.
(*Implicits quotient_map [1 2].*)

Axiom
  quotient_eq :
    forall (r x : Type) (p1 p2 : r -> x) (w : r),
    quotient_map p1 p2 (p1 w) = quotient_map p1 p2 (p2 w).

Parameter
  quotient_fact :
    forall (r x : Type) (p1 p2 : r -> x) (y : Type) 
      (g : x -> y) (hyp : forall w : r, g (p1 w) = g (p2 w)),
    quotient p1 p2 -> y.
(*Implicits quotient_fact [1 2].*)

Parameter
  quotient_recT :
    forall (r x : Type) (p1 p2 : r -> x) (g : x -> Type)
      (hyp : forall w : r, g (p1 w) = g (p2 w)), quotient p1 p2 -> Type.

Parameter
  quotient_rect :
    forall (r x : Type) (p1 p2 : r -> x) (g : x -> Type)
      (hyp : forall w : r, g (p1 w) = g (p2 w)) (s : forall a : x, g a)
      (hyp1 : forall w : r, s (p1 w) -=- s (p2 w)) 
      (q : quotient p1 p2), quotient_recT hyp q.


Axiom
  quotient_fact_comp :
    forall (r x : Type) (p1 p2 : r -> x) (y : Type) 
      (g : x -> y) (hyp : forall w : r, g (p1 w) = g (p2 w)) 
      (a : x), quotient_fact hyp (quotient_map p1 p2 a) = g a.



Axiom
  quotient_surj :
    forall (r x : Type) (p1 p2 : r -> x) (b : quotient p1 p2),
    exists a : x, quotient_map p1 p2 a = b.

(**** we might have to repeat the above for other universe levels *****)

Inductive R_gen_by (r x : Type) (p1 p2 : r -> x) : x -> x -> Prop :=
  | R_gen_by_i1 : forall w : r, R_gen_by p1 p2 (p1 w) (p2 w)
  | R_gen_by_i2 : forall w : r, R_gen_by p1 p2 (p2 w) (p1 w)
  | R_gen_by_refl : forall a : x, R_gen_by p1 p2 a a
  | R_gen_by_trans :
      forall a b c : x,
      R_gen_by p1 p2 a b -> R_gen_by p1 p2 b c -> R_gen_by p1 p2 a c.

Record is_equivalence_relation (x : Type) (R : x -> x -> Prop) : Prop := 
  {reln_refl : forall a : x, R a a;
   reln_symm : forall a b : x, R a b -> R b a;
   reln_trans : forall a b c : x, R a b -> R b c -> R a c}.

Theorem R_gen_by_er :
 forall (r x : Type) (p1 p2 : r -> x),
 is_equivalence_relation (R_gen_by p1 p2).
Proof. 
intros.
eapply (Build_is_equivalence_relation (x:=x) (R:=R_gen_by p1 p2)).
intros.
eapply R_gen_by_refl.

intros.
induction H as [w| w| a| a b c H IHR_gen_by1 H1 IHR_gen_by2].
eapply R_gen_by_i2.

eapply R_gen_by_i1.

eapply R_gen_by_refl.

eapply R_gen_by_trans with b.
assumption.

assumption.

intros.
eapply R_gen_by_trans with b.
assumption.

assumption.
Defined.

Theorem R_gen_by_minimal :
 forall (r x : Type) (p1 p2 : r -> x) (R : x -> x -> Prop)
   (eR : is_equivalence_relation R) (hyp : forall w : r, R (p1 w) (p2 w))
   (a b : x), R_gen_by p1 p2 a b -> R a b.
Proof. 
intros.
induction H as [w| w| a| a b c H IHR_gen_by1 H1 IHR_gen_by2].
eapply hyp.

eapply reln_symm.
exact eR.

eapply hyp.

eapply reln_refl.
eapply eR.

eapply reln_trans with x b.
assumption.

assumption.

assumption.
Qed.


Axiom
  quotient_inj :
    forall (r x : Type) (p1 p2 : r -> x) (a b : x),
    quotient_map p1 p2 a = quotient_map p1 p2 b -> R_gen_by p1 p2 a b.

Theorem quotient_R_eq :
 forall (r x : Type) (p1 p2 : r -> x) (a b : x),
 R_gen_by p1 p2 a b -> quotient_map p1 p2 a = quotient_map p1 p2 b.
Proof. 
intros.
induction H as [w| w| a| a b c H IHR_gen_by1 H1 IHR_gen_by2].
eapply quotient_eq.

symmetry  in |- *.
eapply quotient_eq.

trivial.

transitivity (quotient_map p1 p2 b).
assumption.

assumption.
Qed.

(******* groups *************)

Record group : Type := 
  {the_group :> Type;
   op : the_group -> the_group -> the_group;
   id : the_group;
   inv : the_group -> the_group;
   left_id : forall x : the_group, op id x = x;
   right_id : forall x : the_group, op x id = x;
   assoc : forall x y z : the_group, op (op x y) z = op x (op y z);
   left_inv : forall x : the_group, op (inv x) x = id;
   right_inv : forall x : the_group, op x (inv x) = id}.

Theorem id_left_char : forall (G : group) (x y : G), op x y = y -> x = id G.
Proof. 
intros.
set (h := inv y) in *.
assert (op y h = id G).
unfold h in |- *.
eapply right_inv.

rewrite <- H0.
rewrite <- H.
transitivity (op x (op y h)).
rewrite H0.
symmetry  in |- *.
eapply right_id.

symmetry  in |- *.
eapply assoc.
Qed.

Theorem id_right_char : forall (G : group) (x y : G), op x y = x -> y = id G.
Proof. 
intros.
set (z := inv x) in *.
assert (id G = op z x).
unfold z in |- *.
symmetry  in |- *.
eapply left_inv.

rewrite H0.
rewrite <- H.
transitivity (op (op z x) y).
rewrite <- H0.
symmetry  in |- *.
eapply left_id.

eapply assoc.
Qed.

Theorem inv_left_char :
 forall (G : group) (x y : G), op x y = id G -> x = inv y.
Proof. 
intros.
assert (op (id G) (inv y) = inv y).
eapply left_id.

rewrite <- H0.
rewrite <- H.
transitivity (op x (op y (inv y))).
assert (op y (inv y) = id G).
eapply right_inv.

rewrite H1.
symmetry  in |- *.
eapply right_id.

symmetry  in |- *.
eapply assoc.
Qed.

Theorem inv_right_char :
 forall (G : group) (x y : G), op x y = id G -> y = inv x.
Proof. 
intros.
transitivity (inv (inv y)).
eapply inv_left_char.
eapply right_inv.

assert (inv y = x).
symmetry  in |- *.
eapply inv_left_char.
assumption.

rewrite H0.
trivial.
Qed.

Hint Rewrite [ assoc ] in assoc_right.

Hint Rewrite <- [ assoc ] in assoc_left.

Theorem unop_left : forall (G : group) (x y z : G), y = z -> op x y = op x z.
Proof. 
intros.
rewrite H.
trivial.
Qed.

Theorem unop_right : forall (G : group) (x y z : G), y = z -> op y x = op z x.
Proof. 
intros.
rewrite H.
trivial.
Qed.

Theorem multiply_left :
 forall (G : group) (x y z : G), op x y = op x z -> y = z.
Proof. 
intros.
assert (op (inv x) x = id G).
eapply left_inv.

assert (y = op (inv x) (op x y)).
autorewrite [ assoc_left ].
rewrite H0.
symmetry  in |- *.
eapply left_id.

assert (z = op (inv x) (op x z)).
autorewrite [ assoc_left ].
rewrite H0.
symmetry  in |- *.
eapply left_id.

rewrite H1.
rewrite H2.
eapply unop_left.
assumption.
Qed.

Theorem multiply_right :
 forall (G : group) (x y z : G), op y x = op z x -> y = z.
Proof. 
intros.
assert (op x (inv x) = id G).
eapply right_inv.

assert (y = op (op y x) (inv x)).
autorewrite [ assoc_right ].
rewrite H0.
symmetry  in |- *.
eapply right_id.

assert (z = op (op z x) (inv x)).
autorewrite [ assoc_right ].
rewrite H0.
symmetry  in |- *.
eapply right_id.

rewrite H1.
rewrite H2.
eapply unop_right.
assumption.
Qed.


Theorem switch : forall (G : group) (x y : G), op x y = id G -> op y x = id G.
Proof. 
intros.
eapply multiply_right with (inv x).
rewrite left_id.
autorewrite [ assoc_right ].
rewrite right_inv.
rewrite right_id.
eapply multiply_left with x.
rewrite right_inv.
assumption.
Qed.

Theorem inv_op :
 forall (G : group) (x y : G), inv (op x y) = op (inv y) (inv x).
Proof. 
intros.
symmetry  in |- *.
eapply inv_left_char.
autorewrite [ assoc_left ].
eapply switch.
autorewrite [ assoc_right ].
rewrite left_inv.
rewrite right_id.
apply right_inv.
Qed.

Hint Rewrite [ inv_op ] in inv_in.

Theorem inv_inv : forall (G : group) (x : G), inv (inv x) = x.
Proof. 
intros.
symmetry  in |- *.
eapply inv_left_char.
eapply right_inv.
Qed.


Record gmap (A B : group) : Type := 
  {the_gmap :> A -> B;
   gmap_op : forall x y : A, op (the_gmap x) (the_gmap y) = the_gmap (op x y)}.

Hint Rewrite <- [ gmap_op ] in gmap_in.

Theorem gmap_extens :
 forall (A B : group) (f g : gmap A B), (forall x : A, f x = g x) -> f = g.
Proof. 
intros.
assert (the_gmap f = the_gmap g).
eapply (extensionality (x:=A) (f:=fun x : A => B)).
assumption.

induction f.
induction g.
assert (the_gmap0 = the_gmap1).
assumption.

induction H1.
assert (gmap_op0 = gmap_op1).
eapply proof_irrelevance.

rewrite H1.
trivial.
Qed.

Theorem gmap_id : forall (A B : group) (f : gmap A B), f (id A) = id B.
intros.
eapply id_left_char with (f (id A)).
transitivity (f (op (id A) (id A))).
eapply gmap_op.

set (x := op (id A) (id A)) in *.
assert (x = id A).
unfold x in |- *.
eapply left_id.

rewrite H.
trivial.
Qed.

Theorem gmap_inv :
 forall (A B : group) (f : gmap A B) (x : A), f (inv x) = inv (f x).
Proof. 
intros.
eapply inv_left_char.
transitivity (f (op (inv x) x)).
eapply gmap_op.

assert (op (inv x) x = id A).
eapply left_inv.

rewrite H.
eapply gmap_id.
Qed.

Definition gmap_comp : forall A B C : group, gmap B C -> gmap A B -> gmap A C.
intros A B C f g.
eapply (Build_gmap (A:=A) (B:=C) (the_gmap:=fun x : A => f (g x))).
intros.
transitivity (f (op (g x) (g y))).
eapply gmap_op.

assert (op (g x) (g y) = g (op x y)).
eapply gmap_op.

rewrite H.
trivial.
Defined.

Theorem gmap_comp_eq :
 forall (A B C : group) (f : gmap B C) (g : gmap A B) (x : A),
 gmap_comp f g x = f (g x).
Proof. 
intros.
trivial.
Qed.



Section onecohomology_def.
Variable G : group.

Record onecocycle : Type := 
  {substrate : Type;
   cdiff :> substrate -> substrate -> G;
   substrate_nonempty : nonempty substrate;
   cocycle_rule :
    forall x y z : substrate, op (cdiff y z) (cdiff x y) = cdiff x z}.

Record onecoboundary (alpha beta : onecocycle) : Type := 
  {bdiff :> substrate alpha -> substrate beta -> G;
   cobound_left :
    forall (x y : substrate alpha) (z : substrate beta),
    op (bdiff y z) (alpha x y) = bdiff x z;
   cobound_right :
    forall (x : substrate alpha) (y z : substrate beta),
    op (beta y z) (bdiff x y) = bdiff x z}.

Lemma onecocycle_extens :
 forall alpha beta : onecocycle,
 substrate alpha = substrate beta ->
 (forall (x y : substrate alpha) (x' y' : substrate beta),
  (x -=- x') -> (y -=- y') -> alpha x y = beta x' y') -> 
 alpha = beta.
Proof. 
intros.
induction alpha.
induction beta.
assert (substrate0 = substrate1).
exact H.

induction H1.
set (alpha := Build_onecocycle substrate_nonempty0 cocycle_rule0) in *.
set (beta := Build_onecocycle substrate_nonempty1 cocycle_rule1) in *.
assert (cdiff0 = cdiff1).
eapply
 (extensionality (x:=substrate0)
    (f:=fun x : substrate0 => type_of (cdiff0 x))).
intros.
eapply
 (extensionality (x:=substrate0)
    (f:=fun z : substrate0 => type_of (cdiff0 y z)))
 .
intros.
change (alpha y y0 = beta y y0) in |- *.
eapply H0.
eapply JMeqT_refl.

eapply JMeqT_refl.

induction H1.
assert (cocycle_rule0 = cocycle_rule1).
eapply proof_irrelevance.

assert (substrate_nonempty0 = substrate_nonempty1).
eapply proof_irrelevance.

induction H1.
induction H2.
trivial.
Qed.

Lemma onecoboundary_extens :
 forall (alpha beta : onecocycle) (f g : onecoboundary alpha beta),
 (forall (x : substrate alpha) (y : substrate beta), f x y = g x y) -> f = g.
Proof. 
intros.
induction f.
induction g.
assert (bdiff0 = bdiff1).
eapply
 (extensionality (x:=substrate alpha)
    (f:=fun y : substrate alpha => type_of (bdiff0 y)))
 .
intros.
eapply
 (extensionality (x:=substrate beta)
    (f:=fun z : substrate beta => type_of (bdiff0 y z)))
 .
intros.
eapply H.

induction H0.
assert (cobound_left0 = cobound_left1).
eapply proof_irrelevance.

assert (cobound_right0 = cobound_right1).
eapply proof_irrelevance.

rewrite H0.
rewrite H1.
trivial.
Qed.


Section onecob_descrip.
Variables alpha beta : onecocycle.
Variable de : description G.
Variable v : virtual (onecoboundary alpha beta).


Section onecob_descripA.
Variable x : substrate alpha.
Variable y : substrate beta.

Definition virt_bdiff : virtual G.
apply
 (Build_virtual (X:=G) (carrier:=carrier v)
    (virt_touch:=fun c : carrier v => v c x y)).
apply virt_nonempty.
intros.
assert (v v0 = v w).
apply virt_equal.
rewrite H.
trivial.
Defined.

Lemma onecob_descripA_rmk1 :
 forall (c : carrier v) (d : carrier virt_bdiff), virt_bdiff d = v c x y.
Proof. 
change (forall c d : carrier v, virt_bdiff d = v c x y) in |- *.
intros.
assert (virt_bdiff d = virt_bdiff c).
eapply virt_equal.
rewrite H.
trivial.
Qed.

Definition real_bdiff : G.
exact (de virt_bdiff).
Defined.

Lemma onecob_descripA_rmk2 : forall c : carrier v, real_bdiff = v c x y.
Proof. 
intros.
transitivity (virt_bdiff c).
unfold real_bdiff in |- *.
eapply description_eq.
eapply onecob_descripA_rmk1.
Qed.

End onecob_descripA.

Definition onecob_the_descrip : onecoboundary alpha beta.
Proof. 
eapply (Build_onecoboundary (alpha:=alpha) (beta:=beta) (bdiff:=real_bdiff)).
intros.
assert (nonempty (carrier v)).
eapply virt_nonempty.
induction H.
assert (real_bdiff y z = v X y z).
eapply onecob_descripA_rmk2.
assert (real_bdiff x z = v X x z).
eapply onecob_descripA_rmk2.
rewrite H.
rewrite H0.
eapply cobound_left.
intros.
assert (nonempty (carrier v)).
eapply virt_nonempty.
induction H.
assert (real_bdiff x z = v X x z).
eapply onecob_descripA_rmk2.
assert (real_bdiff x y = v X x y).
eapply onecob_descripA_rmk2.
rewrite H.
rewrite H0.
eapply cobound_right.
Defined.

Lemma onecob_descrip_rmk3 : forall c : carrier v, onecob_the_descrip = v c.
Proof. 
intros.
eapply onecoboundary_extens.
intros.
change (real_bdiff x y = v c x y) in |- *.
eapply onecob_descripA_rmk2.
Qed.
End onecob_descrip.

Definition onecoboundary_description :
  forall alpha beta : onecocycle,
  description G -> description (onecoboundary alpha beta).
intros.
eapply
 (Build_description (X:=onecoboundary alpha beta)
    (the_description:=onecob_the_descrip (alpha:=alpha) (beta:=beta) X))
 .
intros.
eapply onecob_descrip_rmk3.
Defined.







Definition onecoboundary_cocycle :
  forall alpha beta gamma : onecocycle,
  onecoboundary beta gamma ->
  onecoboundary alpha beta -> onecoboundary alpha gamma -> Prop.
intros alpha beta gamma f g h.
exact
 (forall (x : substrate alpha) (y : substrate beta) (z : substrate gamma),
  op (f y z) (g x y) = h x z).
Defined.

Record onecoboundary_trans (alpha beta gamma : onecocycle)
  (f : onecoboundary beta gamma) (g : onecoboundary alpha beta) : Type := 
  {onecob_trans : onecoboundary alpha gamma;
   onecob_trans_cocycle : onecoboundary_cocycle f g onecob_trans}.



Theorem onecoboundary_trans_exists :
 forall (alpha beta gamma : onecocycle) (f : onecoboundary beta gamma)
   (g : onecoboundary alpha beta),
 exists h : onecoboundary alpha gamma, onecoboundary_cocycle f g h.
Proof. 
intros.
assert (nonempty (substrate beta)).
eapply substrate_nonempty.

induction H.
set
 (B := fun (x : substrate alpha) (z : substrate gamma) => op (f X z) (g x X))
 in *.
assert
 (B_left :
  forall (u v : substrate alpha) (w : substrate gamma),
  op (B v w) (alpha u v) = B u w).
intros.
unfold B in |- *.
transitivity (op (f X w) (op (g v X) (alpha u v))).
eapply assoc.

assert (op (g v X) (alpha u v) = g u X).
eapply cobound_left.

rewrite H.
trivial.

assert
 (B_right :
  forall (u : substrate alpha) (v w : substrate gamma),
  op (gamma v w) (B u v) = B u w).
intros.
unfold B in |- *.
transitivity (op (op (gamma v w) (f X v)) (g u X)).
symmetry  in |- *.
eapply assoc.

assert (op (gamma v w) (f X v) = f X w).
eapply cobound_right.

rewrite H.
trivial.

set
 (Bb :=
  Build_onecoboundary (alpha:=alpha) (beta:=gamma) (bdiff:=B) B_left B_right)
 in *.
eapply ex_intro with Bb.
unfold onecoboundary_cocycle in |- *.
intros.
unfold Bb in |- *.
transitivity (op (f X z) (g x X)).
assert (f y z = op (f X z) (beta y X)).
symmetry  in |- *.
eapply cobound_left.

rewrite H.
assert (g x y = op (beta X y) (g x X)).
symmetry  in |- *.
eapply cobound_right.

rewrite H0.
transitivity (op (f X z) (op (beta y X) (op (beta X y) (g x X)))).
eapply assoc.

assert (op (beta y X) (op (beta X y) (g x X)) = g x X).
transitivity (op (op (beta y X) (beta X y)) (g x X)).
symmetry  in |- *.
eapply assoc.

assert (op (beta y X) (beta X y) = beta X X).
eapply cocycle_rule.

rewrite H1.
eapply cobound_right.

rewrite H1.
trivial.

trivial.
Qed.

Theorem onecoboundary_trans_unique :
 forall (alpha beta gamma : onecocycle) (f : onecoboundary beta gamma)
   (g : onecoboundary alpha beta) (h h' : onecoboundary alpha gamma),
 onecoboundary_cocycle f g h -> onecoboundary_cocycle f g h' -> h = h'.
Proof. 
intros.
eapply onecoboundary_extens.
intros.
assert (nonempty (substrate beta)).
eapply substrate_nonempty.

induction H1.
transitivity (op (f X y) (g x X)).
symmetry  in |- *.
eapply H.

eapply H0.
Qed.

Definition onecoboundary_symm :
  forall (alpha beta : onecocycle) (f : onecoboundary alpha beta),
  onecoboundary beta alpha.

intros.
eapply
 (Build_onecoboundary (alpha:=beta) (beta:=alpha)
    (bdiff:=fun (x : substrate beta) (y : substrate alpha) => inv (f y x)))
 .
intros.
eapply inv_right_char.
transitivity (op (op (f z x) (inv (f z y))) (beta x y)).
symmetry  in |- *.
eapply assoc.

assert (op (f z x) (inv (f z y)) = beta y x).
transitivity (op (beta y x) (op (f z y) (inv (f z y)))).
assert (op (f z y) (inv (f z y)) = id _).
eapply right_inv.

transitivity (op (op (beta y x) (f z y)) (inv (f z y))).
assert (f z x = op (beta y x) (f z y)).
symmetry  in |- *.
eapply cobound_right.

rewrite H0.
trivial.

eapply assoc.

assert (op (f z y) (inv (f z y)) = id G).
eapply right_inv.

rewrite H.
eapply right_id.

rewrite H.
transitivity (beta x x).
eapply cocycle_rule.

eapply id_left_char with (beta x x).
eapply cocycle_rule.

intros.
eapply inv_left_char.
transitivity (op (alpha y z) (op (inv (f y x)) (f z x))).
eapply assoc.

assert (op (inv (f y x)) (f z x) = alpha z y).
transitivity (op (inv (f y x)) (op (f y x) (alpha z y))).
assert (f z x = op (f y x) (alpha z y)).
symmetry  in |- *.
eapply cobound_left.

rewrite H.
trivial.

transitivity (op (op (inv (f y x)) (f y x)) (alpha z y)).
symmetry  in |- *.
eapply assoc.

assert (op (inv (f y x)) (f y x) = id G).
eapply left_inv.

rewrite H.
eapply left_id.

rewrite H.
transitivity (alpha z z).
eapply cocycle_rule.

eapply id_left_char with (alpha z z).
eapply cocycle_rule.
Defined.

Theorem onecoboundary_trans_one_elt :
 forall (alpha beta gamma : onecocycle) (f : onecoboundary beta gamma)
   (g : onecoboundary alpha beta), has_one_element (onecoboundary_trans f g).
Proof. 
intros.
eapply Build_has_one_element.
set (K := onecoboundary_trans_exists f g) in *.
induction K.
eapply nonempty_intro.
eapply (Build_onecoboundary_trans (f:=f) (g:=g) (onecob_trans:=x)).
assumption.

intros.
induction a.
induction b.
assert (onecob_trans0 = onecob_trans1).
eapply onecoboundary_trans_unique with beta f g.
assumption.

assumption.

induction H.
assert (onecob_trans_cocycle0 = onecob_trans_cocycle1).
eapply proof_irrelevance.

rewrite H.
trivial.
Qed.

Section onecoboundary_trans_touch_def.
Variables alpha beta gamma : onecocycle.
Variable f : onecoboundary beta gamma.
Variable g : onecoboundary alpha beta.
Variable de : description G.

Let V : virtual (onecoboundary alpha gamma).
eapply
 (Build_virtual (X:=onecoboundary alpha gamma)
    (carrier:=onecoboundary_trans f g)
    (virt_touch:=fun u : onecoboundary_trans f g => onecob_trans u))
 .
eapply one_nonempty.
eapply onecoboundary_trans_one_elt.

intros.
assert (v = w).
eapply one_unique.
eapply onecoboundary_trans_one_elt.

rewrite H.
trivial.
Defined.

Remark ott_rmk1 :
 forall (c : carrier V) (h : onecoboundary_trans f g), V c = onecob_trans h.
Proof. 
intros.
change (onecob_trans c = onecob_trans h) in |- *.
assert (h = c).
eapply one_unique.
eapply onecoboundary_trans_one_elt.

rewrite H.
trivial.
Qed.

Let h : onecoboundary alpha gamma.
assert (description (onecoboundary alpha gamma)).
eapply onecoboundary_description.
assumption.

exact (X V).
Defined.

Definition onecoboundary_trans_touch : onecoboundary_trans f g.
eapply
 (Build_onecoboundary_trans (alpha:=alpha) (beta:=beta) (gamma:=gamma) (f:=f)
    (g:=g) (onecob_trans:=h)).
assert (nonempty (onecoboundary_trans f g)).
eapply one_nonempty.
eapply onecoboundary_trans_one_elt.

induction H.
assert (forall c : carrier V, V c = h).
unfold h in |- *.
intros.
symmetry  in |- *.
eapply description_eq.

assert (V X = h).
eapply H.

assert (V X = onecob_trans X).
eapply ott_rmk1.

rewrite <- H0.
rewrite H1.
eapply onecob_trans_cocycle.
Defined.



End onecoboundary_trans_touch_def.




Definition onecoboundary_refl :
  forall alpha : onecocycle, onecoboundary alpha alpha.
intros.
eapply
 (Build_onecoboundary (alpha:=alpha) (beta:=alpha)
    (bdiff:=fun x y : substrate alpha => alpha x y))
 .
intros.
eapply cocycle_rule.

intros.
eapply cocycle_rule.
Defined.

End onecohomology_def.

Section onecohomology_functoriality.
Variables F G : group.
Variable f : gmap F G.

Definition onecocycle_funct : onecocycle F -> onecocycle G.
intro a.
induction a.
eapply
 (Build_onecocycle (G:=G) (substrate:=substrate0)
    (cdiff:=fun x y : substrate0 => f (cdiff0 x y)))
 .
assumption.

intros.
transitivity (f (op (cdiff0 y z) (cdiff0 x y))).
eapply gmap_op.

rewrite cocycle_rule0.
trivial.
Defined.


Definition onecoboundary_funct :
  forall alpha beta : onecocycle F,
  onecoboundary alpha beta ->
  onecoboundary (onecocycle_funct alpha) (onecocycle_funct beta).
intros.
set (a := alpha) in *.
set (b := beta) in *.
set (A := onecocycle_funct a) in *.
set (B := onecocycle_funct b) in *.
induction alpha.
induction beta.
induction X.
eapply
 (Build_onecoboundary (G:=G) (alpha:=A) (beta:=B)
    (bdiff:=fun (x : substrate A) (y : substrate B) => f (bdiff0 x y)))
 .
intros.
assert (A x y = f (a x y)).
trivial.

rewrite H.
transitivity (f (op (bdiff0 y z) (a x y))).
eapply gmap_op.

assert (op (bdiff0 y z) (a x y) = bdiff0 x z).
eapply cobound_left0.

rewrite H0.
trivial.

intros.
assert (B y z = f (b y z)).
trivial.

rewrite H.
transitivity (f (op (b y z) (bdiff0 x y))).
eapply gmap_op.

rewrite cobound_right0.
trivial.
Defined.


End onecohomology_functoriality.

Section change_substrate_def.
Variable G : group.
Variable alpha : onecocycle G.
Variable U : Type.
Variable s : U -> substrate alpha.
Hypothesis ne : nonempty U.

Definition change_substrate : onecocycle G.
eapply
 (Build_onecocycle (G:=G) (substrate:=U)
    (cdiff:=fun x y : U => alpha (s x) (s y))).
assumption.

intros.
eapply cocycle_rule.
Defined.

Theorem change_substrate_eq :
 forall x y : U, change_substrate x y = alpha (s x) (s y).
Proof. 
intros.
trivial.
Qed.

Definition change_substrate_cob : onecoboundary alpha change_substrate.
eapply
 (Build_onecoboundary (G:=G) (alpha:=alpha) (beta:=change_substrate)
    (bdiff:=fun (x : substrate alpha) (y : U) => alpha x (s y)))
 .
intros.
eapply cocycle_rule.

intros.
rewrite change_substrate_eq.
eapply cocycle_rule.
Defined.



End change_substrate_def.



Section onecohomology_X_def.
Variable X : Type.

Section h1_X_G.
Variable G : X -> group.


Definition c1 := forall x : X, onecocycle (G x).

Record b1 : Type := 
  {b1_a : c1;
   b1_b : c1;
   b1_bound : forall x : X, onecoboundary (b1_a x) (b1_b x)}.

Definition h1 := quotient b1_a b1_b.

Definition h1_fix_universe := Build_group (the_group:=h1).

Definition h1_class : c1 -> h1.
intros.
unfold h1 in |- *.
eapply quotient_map.
assumption.
Defined.

Theorem h1_class_surj : forall u : h1, exists a : c1, h1_class a = u.
Proof. 
unfold h1 in |- *.
unfold h1_class in |- *.
intro.
eapply quotient_surj.
Qed.

Theorem h1_class_inj1 :
 forall a b : c1, h1_class a = h1_class b -> R_gen_by b1_a b1_b a b.
Proof. 
unfold h1 in |- *.
unfold h1_class in |- *.
intros.
eapply quotient_inj.
assumption.
Qed.

(*** now we refine the statement of h1_class_inj using the hypothesis de *****)

Variable de : forall x : X, description (G x).

Definition b1R (a b : c1) :=
  nonempty (forall x : X, onecoboundary (a x) (b x)).

Theorem b1R_er : is_equivalence_relation b1R.
Proof. 
eapply Build_is_equivalence_relation.
intros.
unfold b1R in |- *.
eapply nonempty_intro.
intros.
eapply onecoboundary_refl.

intros a b.
unfold b1R in |- *.
intro.
induction H.
eapply nonempty_intro.
intros.
eapply onecoboundary_symm.
exact (X0 x).

intros.
unfold b1R in |- *.
unfold b1R in H.
unfold b1R in H0.
induction H.
induction H0.
set (U := fun x : X => onecoboundary_trans (X1 x) (X0 x)) in *.
assert (nonempty (forall x : X, U x)).
eapply nonempty_intro.
intro.
unfold U in |- *.
eapply onecoboundary_trans_touch.
eapply de.


induction H.
eapply nonempty_intro.
intros.
set (T := X2 x) in *.
exact (onecob_trans T).
Qed.


Theorem b1_b1R : forall a b : c1, R_gen_by b1_a b1_b a b -> b1R a b.
Proof. 
intros.
eapply R_gen_by_minimal with b1 c1 b1_a b1_b.
eapply b1R_er.

intros.
induction w.
change (b1R b1_a0 b1_b0) in |- *.
unfold b1R in |- *.
eapply nonempty_intro.
assumption.

assumption.
Qed.

Theorem b1R_b1 : forall a b : c1, b1R a b -> R_gen_by b1_a b1_b a b.
Proof. 
intros.
unfold b1R in H.
induction H.
set (U := Build_b1 X0) in *.
exact (R_gen_by_i1 b1_a b1_b U).
Qed.

Theorem h1_class_inj2 : forall a b : c1, h1_class a = h1_class b -> b1R a b.
Proof. 
intros.
eapply b1_b1R.
eapply h1_class_inj1.
assumption.
Qed.

Theorem h1_class_inj :
 forall a b : c1,
 h1_class a = h1_class b ->
 nonempty (forall x : X, onecoboundary (a x) (b x)).
Proof. 
exact h1_class_inj2.
Qed.

Theorem h1_class_eq :
 forall a b : c1,
 nonempty (forall x : X, onecoboundary (a x) (b x)) ->
 h1_class a = h1_class b.
Proof. 
unfold h1 in |- *.
unfold h1_class in |- *.
intros.
eapply quotient_R_eq.
eapply b1R_b1.
exact H.
Qed.

Definition h1_fact :
  forall (Y : Type) (f : c1 -> Y),
  (forall (a b : c1) (u : forall x : X, onecoboundary (a x) (b x)), f a = f b) ->
  h1 -> Y.
intros.
eapply quotient_fact with b1 c1 b1_a b1_b f.
intros.
induction w.
change (f b1_a0 = f b1_b0) in |- *.
eapply H.
assumption.

exact X0.
Defined.

Theorem h1_fact_eq :
 forall (Y : Type) (f : c1 -> Y)
   (hyp : forall (a b : c1) (u : forall x : X, onecoboundary (a x) (b x)),
          f a = f b) (u : c1), h1_fact hyp (h1_class u) = f u.
Proof. 
intros.
unfold h1 in |- *.
unfold h1_fact in |- *.
unfold h1_class in |- *.
eapply quotient_fact_comp.
Qed. 


End h1_X_G.

Section h1_funct_def.
Variables F G : X -> group.
Variable f : forall x : X, gmap (F x) (G x).

Definition c1_funct : c1 F -> c1 G.
intros.
unfold c1 in |- *.
intros.
eapply onecocycle_funct with (F x).
eapply f.

eapply X0.
Defined.

Definition h1_funct : h1 F -> h1 G.
intro u.
eapply h1_fact with F (fun a : c1 F => h1_class (c1_funct a)).
intros.
eapply h1_class_eq.
eapply nonempty_intro.
intros.
unfold c1_funct in |- *.
eapply onecoboundary_funct.
eapply u0.

assumption.
Defined.

End h1_funct_def.

End onecohomology_X_def.

Definition TypeL := Type.

Definition typeL_type_of_substrates (G : group) (U : TypeL) :=
  Build_onecocycle (G:=G) (substrate:=U).


Section exact_sequence_properties.
Variables A B C : group.
Variable f : gmap A B.
Variable g : gmap B C.

Hypothesis surj : forall c : C, exists b : B, g b = c.
Hypothesis inj : forall a1 a2 : A, f a1 = f a2 -> a1 = a2.
Hypothesis comp : forall a : A, g (f a) = id C.


Variable exact : forall (b : B) (hyp : g b = id C), A.
Hypothesis exact_eq : forall (b : B) (hyp : g b = id C), f (exact hyp) = b.

Definition exact_diff :
  forall (c : C) (b b' : B) (hyp : g b = c) (hyp' : g b' = c), A.
intros.
eapply exact with (op b' (inv b)).
transitivity (op (g b') (g (inv b))).
symmetry  in |- *.
eapply gmap_op.

rewrite hyp'.
assert (g (inv b) = inv (g b)).
eapply inv_left_char.
transitivity (g (op (inv b) b)).
eapply gmap_op.

assert (op (inv b) b = id B).
eapply left_inv.

rewrite H.
eapply gmap_id.

rewrite H.
rewrite hyp.
eapply right_inv.
Defined.

Theorem exact_diff_eq :
 forall (c : C) (b b' : B) (hyp : g b = c) (hyp' : g b' = c),
 f (exact_diff hyp hyp') = op b' (inv b).
Proof. 
intros.
unfold exact_diff in |- *.
eapply exact_eq.
Qed.

(*** by the way we show that with (description A) we can get exact ****)
Section exact_from_description_def.
Variable de : description A.

Hypothesis exact_ext : forall b : B, g b = id C -> exists a : A, f a = b.

Variable b : B.
Hypothesis hyp : g b = id C.

Lemma efd_rmk1 : exists a : A, f a = b.
exact (exact_ext hyp).
Qed.

Record efd_carrier : Type :=  {the_efd :> A; efd_eq : f the_efd = b}.

Lemma efd_rmk2 : has_one_element efd_carrier.
Proof. 
eapply Build_has_one_element.
set (K := efd_rmk1) in *.
induction K.
eapply nonempty_intro.
exact (Build_efd_carrier H).

intros.
induction a.
induction b0.
assert (the_efd0 = the_efd1).
eapply inj.
rewrite efd_eq0.
symmetry  in |- *.
assumption.

induction H.
assert (efd_eq0 = efd_eq1).
eapply proof_irrelevance.

rewrite H.
trivial.
Qed.

Let V : virtual A.
eapply (Build_virtual (X:=A) (carrier:=efd_carrier) (virt_touch:=the_efd)).
eapply one_nonempty.
eapply efd_rmk2.

intros.
assert (v = w).
eapply one_unique.
eapply efd_rmk2.

rewrite H.
trivial.
Defined.

Definition exact_from_description : A.
exact (de V).
Defined.

Theorem exact_from_description_eq : f exact_from_description = b.
Proof. 
assert (nonempty (carrier V)).
eapply one_nonempty.
exact efd_rmk2.

induction H.
assert (exact_from_description = V X).
unfold exact_from_description in |- *.
eapply description_eq.

rewrite H.
change (f X = b) in |- *.
eapply efd_eq.
Qed.


End exact_from_description_def.




Record connecter (c : C) (alpha : onecocycle A) : Type := 
  {connecter_diff :> forall (b : B) (hyp : g b = c) (x : substrate alpha), A;
   connecter_left :
    forall (b b' : B) (hyp : g b = c) (hyp' : g b' = c) (x : substrate alpha),
    op (connecter_diff b' hyp' x) (exact_diff hyp hyp') =
    connecter_diff b hyp x;
   connecter_right :
    forall (b : B) (hyp : g b = c) (x y : substrate alpha),
    op (alpha x y) (connecter_diff b hyp x) = connecter_diff b hyp y}.

Theorem connecter_both :
 forall (c : C) (alpha : onecocycle A) (d : connecter c alpha) 
   (b b' : B) (hyp : g b = c) (hyp' : g b' = c) (x x' : substrate alpha),
 op (op (alpha x x') (d b hyp x)) (exact_diff hyp' hyp) = d b' hyp' x'.
Proof. 
intros.
transitivity (op (alpha x x') (d b' hyp' x)).
autorewrite [ assoc_right ].
eapply unop_left.
eapply connecter_left.

eapply connecter_right.
Qed. 

Theorem connecter_extens :
 forall (c : C) (alpha : onecocycle A) (e e' : connecter c alpha),
 (forall (b : B) (hyp : g b = c) (x : substrate alpha),
  e b hyp x = e' b hyp x) -> e = e'.
Proof. 
intros.
induction e.
induction e'.
assert
 (forall (b : B) (hyp : g b = c) (x : substrate alpha),
  connecter_diff0 b hyp x = connecter_diff1 b hyp x).
exact H.

assert (connecter_diff0 = connecter_diff1).
eapply (extensionality (x:=B) (f:=fun b : B => type_of (connecter_diff0 b))).
intros.
eapply
 (extensionality (x:=g y = c)
    (f:=fun u : g y = c => type_of (connecter_diff0 y u)))
 .
intros.
eapply
 (extensionality (x:=substrate alpha)
    (f:=fun x : substrate alpha => type_of (connecter_diff0 y y0 x)))
 .
intros.
eapply H0.

induction H1.
assert (connecter_left0 = connecter_left1).
eapply proof_irrelevance.

assert (connecter_right0 = connecter_right1).
eapply proof_irrelevance.

rewrite H1.
rewrite H2.
trivial.
Qed.

Section connecter_description_def.
Variable c : C.
Variable alpha : onecocycle A.
Variable de : description A.
Variable V : virtual (connecter c alpha).

Let Z := carrier V.

Section cdescripA.
Variable b : B.
Hypothesis hyp : g b = c.
Variable x : substrate alpha.

Let virt_cdiff : virtual A.
eapply
 (Build_virtual (X:=A) (carrier:=Z) (virt_touch:=fun z : Z => V z b hyp x))
 .
unfold Z in |- *.
eapply virt_nonempty.

intros.
assert (V v = V w).
apply virt_equal.

rewrite H.
trivial.
Defined.

Remark crd_rmk1 : forall z : Z, virt_cdiff z = V z b hyp x.
Proof. 
intros.
trivial.
Qed.

Definition real_cdiff : A.
exact (de virt_cdiff).
Defined.

Remark crd_rmk2 : forall z : Z, real_cdiff = V z b hyp x.
Proof. 
intros.
rewrite <- crd_rmk1.
unfold real_cdiff in |- *.
eapply description_eq.
Qed.

End cdescripA.

Definition connecter_the_descrip : connecter c alpha.
eapply (Build_connecter (c:=c) (alpha:=alpha) (connecter_diff:=real_cdiff)).
intros.
assert (nonempty Z).
unfold Z in |- *.
eapply virt_nonempty.

induction H.
assert (real_cdiff hyp' x = V X b' hyp' x).
eapply crd_rmk2.

assert (real_cdiff hyp x = V X b hyp x).
eapply crd_rmk2.

rewrite H.
rewrite H0.
eapply connecter_left.

intros.
assert (nonempty Z).
unfold Z in |- *.
eapply virt_nonempty.

induction H.
assert (real_cdiff hyp x = V X b hyp x).
eapply crd_rmk2.

assert (real_cdiff hyp y = V X b hyp y).
eapply crd_rmk2.

rewrite H.
rewrite H0.
eapply connecter_right.
Defined.


Lemma crd_rmk3 : forall z : Z, connecter_the_descrip = V z.
Proof. 
intros.
eapply connecter_extens.
intros.
change (real_cdiff hyp x = V z b hyp x) in |- *.
eapply crd_rmk2.
Qed.


End connecter_description_def.

Definition connecter_description :
  forall (c : C) (alpha : onecocycle A) (de : description A),
  description (connecter c alpha).
intros.
eapply
 (Build_description (X:=connecter c alpha)
    (the_description:=connecter_the_descrip (c:=c) (alpha:=alpha) de))
 .
intros.
eapply crd_rmk3.
Defined.



Definition connecter_cocycle (c : C) (alpha beta : onecocycle A)
  (d : connecter c alpha) (e : connecter c beta)
  (m : onecoboundary alpha beta) :=
  forall (b : B) (hyp : g b = c) (x : substrate alpha) (y : substrate beta),
  op (m x y) (d b hyp x) = e b hyp y.

Section connecter_coboundary_def.
Variable c : C.
Variables alpha beta : onecocycle A.
Variable d : connecter c alpha.
Variable e : connecter c beta.

Theorem connecter_coboundary_exists :
 exists m : onecoboundary alpha beta, connecter_cocycle d e m.
Proof. 
induction (surj c).
set
 (U :=
  fun (y : substrate alpha) (z : substrate beta) =>
  op (e x H z) (inv (d x H y))) in *.
assert
 (U_left :
  forall (u v : substrate alpha) (w : substrate beta),
  op (U v w) (alpha u v) = U u w).
intros.
unfold U in |- *.
transitivity (op (e x H w) (op (inv (d x H v)) (alpha u v))).
eapply assoc.

assert (op (inv (d x H v)) (alpha u v) = inv (d x H u)).
eapply inv_left_char.
transitivity (op (inv (d x H v)) (op (alpha u v) (d x H u))).
eapply assoc.

assert (op (alpha u v) (d x H u) = d x H v).
eapply connecter_right.

rewrite H0.
eapply left_inv.

rewrite H0.
trivial.


assert
 (U_right :
  forall (u : substrate alpha) (v w : substrate beta),
  op (beta v w) (U u v) = U u w).
intros.
unfold U in |- *.
transitivity (op (op (beta v w) (e x H v)) (inv (d x H u))).
symmetry  in |- *.
eapply assoc.

assert (op (beta v w) (e x H v) = e x H w).
eapply connecter_right.

rewrite H0.
trivial.

set
 (M :=
  Build_onecoboundary (G:=A) (alpha:=alpha) (beta:=beta) (bdiff:=U) U_left
    U_right) in *.
eapply ex_intro with M.
unfold connecter_cocycle in |- *.
intros.
change (op (U x0 y) (d b hyp x0) = e b hyp y) in |- *.
unfold U in |- *.
assert (e x H y = op (e b hyp y) (exact_diff H hyp)).
symmetry  in |- *.
eapply connecter_left.

assert (d b hyp x0 = op (d x H x0) (exact_diff hyp H)).
symmetry  in |- *.
eapply connecter_left.

rewrite H0.

transitivity
 (op (e b hyp y) (op (op (exact_diff H hyp) (inv (d x H x0))) (d b hyp x0))).
autorewrite [ assoc_left ].
trivial.

transitivity (op (e b hyp y) (id _)).
eapply unop_left.
eapply switch.
eapply multiply_right with (d x H x0).
rewrite left_id.
autorewrite [ assoc_right ].
rewrite left_inv.
autorewrite [ assoc_left ].
rewrite right_id.
eapply connecter_left.

eapply right_id.
Qed.

Theorem connecter_coboundary_unique :
 forall m m' : onecoboundary alpha beta,
 connecter_cocycle d e m -> connecter_cocycle d e m' -> m = m'.
Proof. 
intros.
eapply onecoboundary_extens.
intros.
unfold connecter_cocycle in H.
unfold connecter_cocycle in H0.
induction (surj c).
set (K := H x0 H1 x y) in *.
set (K0 := H0 x0 H1 x y) in *.
eapply multiply_right with (d x0 H1 x).
rewrite K.
rewrite K0.
trivial.
Qed.

Record ccob_carrier : Type := 
  {the_ccob :> onecoboundary alpha beta;
   ccob_cocycle : connecter_cocycle d e the_ccob}.

Theorem ccob_one_elt : has_one_element ccob_carrier.
Proof. 
eapply Build_has_one_element.
set (E := connecter_coboundary_exists) in *.
induction E.
eapply nonempty_intro.
eapply (Build_ccob_carrier (the_ccob:=x) H).

intros.
induction a.
induction b.
assert (the_ccob0 = the_ccob1).
eapply connecter_coboundary_unique.
assumption.

assumption.

induction H.
assert (ccob_cocycle0 = ccob_cocycle1).
eapply proof_irrelevance.

rewrite H.
trivial.
Qed.

Let V : virtual (onecoboundary alpha beta).
eapply
 (Build_virtual (X:=onecoboundary alpha beta) (carrier:=ccob_carrier)
    (virt_touch:=the_ccob)).
eapply one_nonempty.
eapply ccob_one_elt.

intros.
induction v.
induction w.
assert (the_ccob0 = the_ccob1).
eapply connecter_coboundary_unique.
assumption.

assumption.

induction H.
assert (ccob_cocycle0 = ccob_cocycle1).
eapply proof_irrelevance.

rewrite H.
trivial.
Defined.

Lemma ccob_rmk1 : forall c : carrier V, connecter_cocycle d e (V c).
Proof. 
intros.
assert (V c0 = the_ccob c0).
trivial.

rewrite H.
eapply ccob_cocycle.
Qed.

Definition ccob_touch : description A -> onecoboundary alpha beta.
intro de.
assert (description (onecoboundary alpha beta)).
eapply onecoboundary_description.
assumption.

eapply (the_description X).
exact V.
Defined.

Lemma ccob_rmk2 :
 forall (c : carrier V) (de : description A), ccob_touch de = V c.
Proof. 
intros.
unfold ccob_touch in |- *.
eapply description_eq.
Qed.

Theorem ccob_touch_cocycle :
 forall de : description A, connecter_cocycle d e (ccob_touch de).
Proof. 
intros.
assert (nonempty (carrier V)).
eapply virt_nonempty.

induction H.
assert (ccob_touch de = V X).
eapply ccob_rmk2.

rewrite H.
eapply ccob_rmk1.
Qed.


End connecter_coboundary_def.

Section connecter_connecter_def.
Variable c : C.
Variables alpha beta : onecocycle A.
Variable d : connecter c alpha.
Variable m : onecoboundary alpha beta.

Theorem connecter_connecter_exists :
 exists e : connecter c beta, connecter_cocycle d e m.
Proof. 
induction (surj c).
assert (nonempty (substrate alpha)).
eapply substrate_nonempty.

induction H0.
set
 (U :=
  fun (b : B) (hyp : g b = c) (u : substrate beta) => op (m X u) (d b hyp X))
 in *.

assert
 (U_left :
  forall (b1 b2 : B) (hyp1 : g b1 = c) (hyp2 : g b2 = c) (u : substrate beta),
  op (U b2 hyp2 u) (exact_diff hyp1 hyp2) = U b1 hyp1 u).
intros.
unfold U in |- *.
transitivity (op (m X u) (op (d b0 hyp2 X) (exact_diff hyp1 hyp2))).
eapply assoc.

eapply unop_left.
eapply connecter_left.

assert
 (U_right :
  forall (b : B) (hyp : g b = c) (u v : substrate beta),
  op (beta u v) (U b hyp u) = U b hyp v).
intros.
unfold U in |- *.
transitivity (op (op (beta u v) (m X u)) (d b hyp X)).
symmetry  in |- *.
eapply assoc.

eapply unop_right.
eapply cobound_right.

set
 (W :=
  Build_connecter (c:=c) (alpha:=beta) (connecter_diff:=U) U_left U_right)
 in *.
eapply ex_intro with W.
unfold connecter_cocycle in |- *.
intros.
unfold W in |- *.
symmetry  in |- *.
transitivity (U b hyp y).
trivial.

unfold U in |- *.
assert (m x0 y = op (m X y) (alpha x0 X)).
symmetry  in |- *.
eapply cobound_left.

rewrite H0.
symmetry  in |- *.
transitivity (op (m X y) (op (alpha x0 X) (d b hyp x0))).
eapply assoc.

eapply unop_left.
eapply connecter_right.
Qed.

Theorem connecter_connecter_unique :
 forall e e' : connecter c beta,
 connecter_cocycle d e m -> connecter_cocycle d e' m -> e = e'.
Proof. 
intros.
eapply connecter_extens.
intros.
assert (nonempty (substrate alpha)).
eapply substrate_nonempty.

induction H1.
transitivity (op (m X x) (d b hyp X)).
symmetry  in |- *.
eapply H.

eapply H0.
Qed.

Record ccon_carrier : Type := 
  {the_ccon :> connecter c beta;
   ccon_cocycle : connecter_cocycle d the_ccon m}.

Theorem ccon_one_elt : has_one_element ccon_carrier.
Proof. 
eapply Build_has_one_element.
set (K := connecter_connecter_exists) in *.
induction K.
eapply nonempty_intro.
eapply (Build_ccon_carrier (the_ccon:=x)).
assumption.

intros.
induction a.
induction b.
assert (the_ccon0 = the_ccon1).
eapply connecter_connecter_unique.
assumption.

assumption.

induction H.
assert (ccon_cocycle0 = ccon_cocycle1).
eapply proof_irrelevance.

rewrite H.
trivial.
Qed.

Let V : virtual (connecter c beta).
eapply
 (Build_virtual (X:=connecter c beta) (carrier:=ccon_carrier)
    (virt_touch:=the_ccon)).
eapply one_nonempty.
eapply ccon_one_elt.

intros.
assert (v = w).
eapply one_unique.
eapply ccon_one_elt.

rewrite H.
trivial.
Defined.

Variable de : description A.

Definition ccon_touch : connecter c beta.
assert (description (connecter c beta)).
eapply connecter_description.
assumption.

eapply (the_description X).
exact V.
Defined.

Remark ccon_rmk1 : forall z : carrier V, ccon_touch = V z.
Proof. 
intros.
unfold ccon_touch in |- *.
eapply description_eq.
Qed.

Theorem ccon_touch_cocycle : connecter_cocycle d ccon_touch m.
Proof. 
assert (nonempty (carrier V)).
eapply virt_nonempty.

induction H.
assert (ccon_touch = V X).
eapply ccon_rmk1.

rewrite H.
assert (V X = the_ccon X).
trivial.

rewrite H0.
eapply ccon_cocycle.
Qed.

End connecter_connecter_def.


Section connectee_def.
Variable c : C.
Variable U : TypeL.
Hypothesis ne : nonempty U.
Variable s : U -> B.
Variable hyp : forall u : U, g (s u) = c.

Definition connectee_diff : U -> U -> A.
intros x y.
assert (g (s x) = c).
apply hyp.

assert (g (s y) = c).
apply hyp.

exact (exact_diff H H0).
Defined.

Remark cee_rmk1 :
 forall x y : U, f (connectee_diff x y) = op (s y) (inv (s x)).
Proof. 
intros.
unfold connectee_diff in |- *.
eapply exact_diff_eq.
Qed.

Definition connectee : onecocycle A.
eapply (Build_onecocycle (G:=A) (substrate:=U) (cdiff:=connectee_diff)).
assumption.

intros.
eapply inj.
transitivity (op (f (connectee_diff y z)) (f (connectee_diff x y))).
symmetry  in |- *.
eapply gmap_op.

rewrite cee_rmk1.
rewrite cee_rmk1.
rewrite cee_rmk1.
autorewrite [ assoc_right ].
eapply unop_left.
autorewrite [ assoc_left ].
rewrite left_inv.
eapply left_id.
Defined.


Definition connectee_connecter_diff :
  forall (b : B) (hyp : g b = c) (x : U), A.
intros.
assert (g (s x) = c).
apply hyp.

exact (exact_diff hyp0 H).
Defined.

Lemma cee_rmk2 :
 forall (b : B) (hyp : g b = c) (x : U),
 f (connectee_connecter_diff hyp x) = op (s x) (inv b).
Proof. 
intros.
unfold connectee_connecter_diff in |- *.
eapply exact_diff_eq.
Qed.


Definition connectee_connecter : connecter c connectee.
eapply
 (Build_connecter (c:=c) (alpha:=connectee)
    (connecter_diff:=connectee_connecter_diff)).
intros.
eapply inj.
rewrite <- gmap_op.
rewrite cee_rmk2.
rewrite cee_rmk2.
rewrite exact_diff_eq.
autorewrite [ assoc_left ].
eapply unop_right.
autorewrite [ assoc_right ].
rewrite left_inv.
eapply right_id.

intros.
eapply inj.
rewrite <- gmap_op.
rewrite cee_rmk2.
rewrite cee_rmk2.
rewrite cee_rmk1.
autorewrite [ assoc_left ].
eapply unop_right.
autorewrite [ assoc_right ].
rewrite left_inv.
eapply right_id.
Defined.


End connectee_def.

Section connecter_two_section.
Variables c1 c2 : C.
Variable alpha : onecocycle A.
Variable d1 : connecter c1 alpha.
Variable d2 : connecter c2 alpha.

Variable deb : description B.

(*** try to get back an element b : B with (op b c1) == c2 ***)

Record connecter_two_carrier : Type := 
  {ctc_b1 : B;
   ctc_b2 : B;
   ctc_sub : substrate alpha;
   ctc_hyp1 : g ctc_b1 = c1;
   ctc_hyp2 : g ctc_b2 = c2}.

Let ctc_b1_corr (w : connecter_two_carrier) :=
  op (f (d1 (ctc_b1 w) (ctc_hyp1 w) (ctc_sub w))) (ctc_b1 w).

Let ctc_b2_corr (w : connecter_two_carrier) :=
  op (f (d2 (ctc_b2 w) (ctc_hyp2 w) (ctc_sub w))) (ctc_b2 w).

Lemma two_rmk1 : forall w : connecter_two_carrier, g (ctc_b1_corr w) = c1.
Proof. 
intros.
unfold ctc_b1_corr in |- *.
rewrite <- gmap_op.
rewrite comp.
rewrite left_id.
eapply ctc_hyp1.
Qed.

Lemma two_rmk2 : forall w : connecter_two_carrier, g (ctc_b2_corr w) = c2.
Proof. 
intros.
unfold ctc_b2_corr in |- *.
rewrite <- gmap_op.
rewrite comp.
rewrite left_id.
eapply ctc_hyp2.
Qed.

Definition ctc_virt_touch (w : connecter_two_carrier) : B :=
  op (inv (ctc_b1_corr w)) (ctc_b2_corr w).

Lemma two_rmk3 :
 forall w : connecter_two_carrier, op c1 (g (ctc_virt_touch w)) = c2.
Proof. 
intros.
unfold ctc_virt_touch in |- *.
rewrite <- gmap_op.
rewrite gmap_inv.
rewrite two_rmk1.
rewrite two_rmk2.
autorewrite [ assoc_left ].
rewrite right_inv.
apply left_id.
Qed.

Lemma two_rmk4 :
 forall w w' : connecter_two_carrier,
 op (f (exact_diff (ctc_hyp2 w') (ctc_hyp2 w))) (ctc_b2 w') = ctc_b2 w.
Proof. 
intros.
rewrite exact_diff_eq.
autorewrite [ assoc_right ].
rewrite left_inv.
eapply right_id.
Qed.

Lemma two_rmk5 :
 forall w w' : connecter_two_carrier,
 op (inv (ctc_b1 w')) (inv (f (exact_diff (ctc_hyp1 w') (ctc_hyp1 w)))) =
 inv (ctc_b1 w).
Proof. 
intros.
rewrite exact_diff_eq.
rewrite inv_op.
rewrite inv_inv.
autorewrite [ assoc_left ].
rewrite left_inv.
apply left_id.
Qed.


Theorem ctc_virt_unique :
 forall w w' : connecter_two_carrier, ctc_virt_touch w = ctc_virt_touch w'.
Proof. 
intros.
unfold ctc_virt_touch in |- *.
unfold ctc_b1_corr in |- *.
unfold ctc_b2_corr in |- *.
set
 (K1 :=
  connecter_both d1 (ctc_hyp1 w) (ctc_hyp1 w') (ctc_sub w) (ctc_sub w')) 
 in *.
set
 (K2 :=
  connecter_both d2 (ctc_hyp2 w) (ctc_hyp2 w') (ctc_sub w) (ctc_sub w')) 
 in *.
rewrite <- K1.
rewrite <- K2.
autorewrite [ gmap_in ].
autorewrite [ inv_in ].
autorewrite [ assoc_left ].
rewrite two_rmk5.
autorewrite [ assoc_right ].
eapply unop_left.
eapply unop_left.
rewrite two_rmk4.
autorewrite [ assoc_left ].
eapply unop_right.
rewrite left_inv.
rewrite left_id.
trivial.
Qed.


Lemma two_rmk6 : nonempty connecter_two_carrier.
Proof. 
assert (nonempty (substrate alpha)). 
eapply substrate_nonempty.

assert (exists u1 : B, g u1 = c1).
eapply surj.

assert (exists u2 : B, g u2 = c2).
eapply surj.

induction H.
induction H0.
induction H1.
eapply nonempty_intro.
eapply Build_connecter_two_carrier with x x0.
assumption.

assumption.

assumption.
Qed.


Definition connecter_two_virtual : virtual B.
eapply
 (Build_virtual (X:=B) (carrier:=connecter_two_carrier)
    (virt_touch:=ctc_virt_touch)).
eapply two_rmk6.

intros.
eapply ctc_virt_unique.
Defined.

Lemma two_rmk7 :
 forall u : carrier connecter_two_virtual,
 op c1 (g (connecter_two_virtual u)) = c2.
Proof. 
intros.
eapply two_rmk3.
Qed.

Definition connecter_two : B.
exact (deb connecter_two_virtual).
Defined.

Theorem connecter_two_property : op c1 (g connecter_two) = c2.
Proof. 
assert (nonempty (carrier connecter_two_virtual)).
eapply virt_nonempty.

induction H.
assert (connecter_two = connecter_two_virtual X).
unfold connecter_two in |- *.
eapply description_eq.

rewrite H.
eapply two_rmk7.
Qed.


End connecter_two_section.

Section connecter_three_section.
Variables c1 c2 : C.
Variables alpha beta : onecocycle A.
Variable d1 : connecter c1 alpha.
Variable d2 : connecter c2 beta.
Variable m : onecoboundary alpha beta.

Variable dea : description A.
Variable deb : description B.

Definition c3_new_d1 : connecter c1 beta.
eapply ccon_touch with alpha.
assumption.

assumption.

assumption.
Defined.

Definition connecter_three : B.
eapply connecter_two with c1 c2 beta.
eapply c3_new_d1.

assumption.

assumption.
Defined.

Theorem connecter_three_property : op c1 (g connecter_three) = c2.
Proof. 
unfold connecter_three in |- *.
eapply connecter_two_property.
Qed.

End connecter_three_section.


End exact_sequence_properties.


Record small_cover_replacement (X : Type) (Y : X -> Type) : Type := 
  {scr_upsilon : X -> TypeL;
   scr_phi : forall x : X, scr_upsilon x -> Y x;
   scr_nonempty : forall x : X, nonempty (scr_upsilon x)}.





Section long_exact_sequence_section.
Variable X : Type.
Variable
  scr :
    forall (Y : X -> Type) (hyp : forall x : X, nonempty (Y x)),
    small_cover_replacement Y.
Variables A B C : X -> group.
Variable f : forall x : X, gmap (A x) (B x).
Variable g : forall x : X, gmap (B x) (C x).
Variable de : forall x : X, description (A x).
Variable deb : forall x : X, description (B x).

Hypothesis inj : forall (x : X) (a1 a2 : A x), f x a1 = f x a2 -> a1 = a2.
Hypothesis surj : forall (x : X) (c : C x), exists b : B x, g x b = c.
Hypothesis comp : forall (x : X) (a : A x), g x (f x a) = id (C x).


Hypothesis
  exact :
    forall (x : X) (b : B x), g x b = id (C x) -> exists a : A x, f x a = b.

Record les_f_inv_im (x : X) (b : B x) : Type := 
  {lfii : A x; lfii_eq : f x lfii = b}.

Record les_g_inv_im (x : X) (c : C x) : Type := 
  {lgii : B x; lgii_eq : g x lgii = c}.

Definition exact_virtual_section :
  forall (x : X) (b : B x) (hyp : g x b = id (C x)), virtual (A x).
intros.
eapply
 (Build_virtual (X:=A x) (carrier:=les_f_inv_im b)
    (virt_touch:=lfii (x:=x) (b:=b))).
set (K := exact hyp) in *.
induction K.
eapply nonempty_intro.
exact (Build_les_f_inv_im H).

intros.
eapply inj.
rewrite lfii_eq.
rewrite lfii_eq.
trivial.
Defined.



Definition exact_section :
  forall (x : X) (b : B x) (hyp : g x b = id (C x)), A x.
Proof. 
intros.
exact (de x (exact_virtual_section hyp)).
Defined.

Theorem exact_section_eq :
 forall (x : X) (b : B x) (hyp : g x b = id (C x)),
 f x (exact_section hyp) = b.
Proof. 
intros.
set (V := exact_virtual_section hyp) in *.
assert (nonempty (carrier V)).
eapply virt_nonempty.

induction H.
assert (exact_section hyp = V X0).
unfold exact_section in |- *.
eapply description_eq.

rewrite H.
assert (V X0 = lfii (x:=x) (b:=b) X0).
trivial.

rewrite H0.
eapply lfii_eq.
Qed.

Section connecting_map_def.
Variable c : forall x : X, C x.

Let connecting_scr :
  small_cover_replacement (fun x : X => les_g_inv_im (c x)).
eapply scr.
intros.
set (K := surj (c x)) in *.
induction K.
eapply nonempty_intro.
exact (Build_les_g_inv_im H).
Defined.

Definition connecting_substrate : X -> TypeL.
exact (scr_upsilon connecting_scr).
Defined.

Definition connecting_substrate_map :
  forall x : X, connecting_substrate x -> B x.
intros.
eapply lgii with (c x).
eapply
 (scr_phi (X:=X) (Y:=fun x : X => les_g_inv_im (c x)) (s:=connecting_scr))
 .
exact X0.
Defined.

Theorem connecting_substrate_eq :
 forall (x : X) (u : connecting_substrate x),
 g x (connecting_substrate_map u) = c x.
Proof. 
intros.
unfold connecting_substrate_map in |- *.
eapply lgii_eq.
Qed.

Theorem connecting_substrate_ne :
 forall x : X, nonempty (connecting_substrate x).
Proof. 
intros.
unfold connecting_substrate in |- *.
eapply scr_nonempty.
Qed.


Definition les_connectee : forall x : X, onecocycle (A x).
intro x.
exact
 (connectee (A:=A x) (B:=B x) (C:=C x) (f:=f x) (g:=
    g x) (inj (x:=x)) (exact:=exact_section (x:=x)) (
    exact_section_eq (x:=x)) (c:=c x) (U:=connecting_substrate x)
    (connecting_substrate_ne x) (s:=connecting_substrate_map (x:=x))
    (connecting_substrate_eq (x:=x))).
Defined.

Definition les_connecter :
  forall x : X, connecter (exact_section (x:=x)) (c x) (les_connectee x).
intro x.
unfold les_connectee in |- *.
eapply connectee_connecter.
Defined.

Definition les_delta : h1 A.
exact (h1_class les_connectee).
Defined.


End connecting_map_def.

Section if_delta_same.
Variables c1 c2 : forall x : X, C x.

Hypothesis hyp : les_delta c1 = les_delta c2.

Theorem delta_same_onecoboundary_nonempty :
 nonempty
   (forall x : X, onecoboundary (les_connectee c1 x) (les_connectee c2 x)).
Proof. 
eapply h1_class_inj.
exact de.

exact hyp.
Qed.

Section delta_sameA.
Variable
  u : forall x : X, onecoboundary (les_connectee c1 x) (les_connectee c2 x).

Definition les_lift : forall x : X, B x.
intro x.
apply
 connecter_three
  with
    (A := A x)
    (B := B x)
    (C := C x)
    (f := f x)
    (g := g x)
    (exact := exact_section (x:=x))
    (c1 := c1 x)
    (c2 := c2 x)
    (alpha := les_connectee c1 x)
    (beta := les_connectee c2 x).
intros.
eapply surj.

intros.
eapply exact_section_eq.

eapply les_connecter.

eapply les_connecter.

eapply u.

eapply de.

eapply deb.
Defined.

Theorem les_lift_property : forall x : X, op (c1 x) (g x (les_lift x)) = c2 x.
Proof. 
intros.
unfold les_lift in |- *.
eapply connecter_three_property.
intros.
eapply comp.
Qed. 


End delta_sameA.

Theorem les_first_exact :
 exists b : forall x : X, B x, (forall x : X, op (c1 x) (g x (b x)) = c2 x).
Proof. 
set (K := delta_same_onecoboundary_nonempty) in *.
induction K.
eapply ex_intro with (les_lift X0).
intros.
eapply les_lift_property.
Qed.


End if_delta_same.

Section if_h1_trivial.
Variable c : forall x : X, C x.
Hypothesis h1_trivial : forall u v : h1 A, u = v.

Definition identity_section (x : X) : C x := id (C x).

Remark h1t_rmk1 : les_delta identity_section = les_delta c.
Proof. 
eapply h1_trivial.
Qed.

Remark h1t_rmk2 :
 exists b : forall x : X, B x,
   (forall x : X, op (identity_section x) (g x (b x)) = c x).
Proof. 
eapply les_first_exact.
exact h1t_rmk1.
Qed.

Theorem lift_when_h1_trivial :
 exists b : forall x : X, B x, (forall x : X, g x (b x) = c x).
Proof. 
set (K := h1t_rmk2) in *.
induction K.
eapply ex_intro with x.
intros.
rewrite <- H.
assert (identity_section x0 = id (C x0)).
trivial.

rewrite H0.
symmetry  in |- *.
eapply left_id.
Qed.

End if_h1_trivial.

(***** ideally we should still define the trivial element of h1 
and show that if c is something
whose les_delta is the trivial element then it comes from B, 
the point being to show that
the les_delta of the identity section is equivalent to the 
trivial element ******)


End long_exact_sequence_section.


Theorem lift_when_h1_trivial_rewrite :
 forall X : Type,
 (forall Y : X -> Type,
  (forall x : X, nonempty (Y x)) -> small_cover_replacement Y) ->
 forall (A B C : X -> group) (f : forall x : X, gmap (A x) (B x))
   (g : forall x : X, gmap (B x) (C x)),
 (forall x : X, description (A x)) ->
 (forall x : X, description (B x)) ->
 (forall (x : X) (a1 a2 : A x), f x a1 = f x a2 -> a1 = a2) ->
 (forall (x : X) (c : C x), exists b : B x, g x b = c) ->
 (forall (x : X) (a : A x), g x (f x a) = id (C x)) ->
 (forall (x : X) (b : B x), g x b = id (C x) -> exists a : A x, f x a = b) ->
 forall c : forall x : X, C x,
 (forall u v : h1 A, u = v) ->
 exists b : forall x : X, B x, (forall x : X, g x (b x) = c x).
Proof lift_when_h1_trivial.