annotate a proof
annotate a proof
reorganize a proof
Merge branch 'master' of github.com:UniMath/UniMath
correct a misspelling
proved ZZBiRecursionEquiv, with computation rule

Definition ZZBiRecursionEquiv (P:ZZ->Type) (IH :forall i, weq (P i) (P(1+i))) :
  weq (total2 (ZZBiRecursionData P IH)) (P 0).
ZZTorsorRecursionEquiv with computation rule

Definition ZZTorsorRecursionEquiv {T:Torsor ZZ} (P:T->Type)
      (IH:forall t, weq (P t) (P (one + t))) :
  forall t0,
  weq (total2 (fun
          f:forall t, P t =>
            forall t, f (one + t) == IH t (f t)))
      (P t0).
the affine line is done

(no more "admits")
clean up
clean up

1. Fix some confusion about "pr1" versus "pr1weq".

2. Make isweqtoforallpaths opaque with "Qed", fixing a problem
   in toforallpaths_funextsec.

3. Change the definition of total2 to a "primitive" record, to
   prepare for forthcoming "primitive" projections.
circle ...
circle ...
circle ...
circle ...
circle ...
circle ...
circle ...
circle_map_check_paths now follows from a lemma

and it takes 6.6 seconds to check that (!).
The lemma includes an "admit", to work on next.
circle ...
iscontrGuidedHomotopy_comp_2 proved

... after a great deal of struggle.

Advice: for any proof with types more complicated than nat==nat,
avoid "change" and "rewrite".