Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

(** A nice method for proving characterizations of path-types of nested sigma-types, due to Rijke. *)

(** To show that the based path-type of [A] is equivalent to some specified family [P], it suffices to show that [P] is reflexive and its total space is contractible. This is part of Theorem 5.8.2, namely (iv) implies (iii). *)
Definition equiv_path_from_contr {A : Type} (a : A) (P : A -> Type)
           (Prefl : P a)
           (cp : Contr {y:A & P y} )
           (b : A)
  : P b <~> a = b.
A: Type
a: A
P: A -> Type
Prefl: P a
cp: Contr {y : A & P y}
b: A
P b <~> a = b
Proof.
A: Type
a: A
P: A -> Type
Prefl: P a
cp: Contr {y : A & P y}
b: A
P b <~> a = b
  apply equiv_inverse.
A: Type
a: A
P: A -> Type
Prefl: P a
cp: Contr {y : A & P y}
b: A
a = b <~> P b
  srefine (Build_Equiv _ _ _ _).
A: Type
a: A
P: A -> Type
Prefl: P a
cp: Contr {y : A & P y}
b: A
a = b -> P b
A: Type
a: A
P: A -> Type
Prefl: P a
cp: Contr {y : A & P y}
b: A
IsEquiv ?equiv_fun
  {
A: Type
a: A
P: A -> Type
Prefl: P a
cp: Contr {y : A & P y}
b: A
a = b -> P b intros []; apply Prefl. }
A: Type
a: A
P: A -> Type
Prefl: P a
cp: Contr {y : A & P y}
b: A
IsEquiv
  (fun X : a = b =>
   match X in (_ = a0) return (P a0) with
   | 1 => Prefl
   end)
  revert b; apply isequiv_from_functor_sigma.
A: Type
a: A
P: A -> Type
Prefl: P a
cp: Contr {y : A & P y}
IsEquiv
  (functor_sigma idmap
     (fun (a0 : A) (X : a = a0) =>
      match X in (_ = a1) return (P a1) with
      | 1 => Prefl
      end))
  rapply isequiv_contr_contr.
Defined.

(** See Homotopy/EncodeDecode.v for a related characterization of identity types. *)

(** This is another result for characterizing the path type of [A] when given an equivalence [e : B <~> A], such as an [issig] lemma for [A]. It can help Coq to deduce the type family [P] if [revert] is used to move [a0] and [a1] into the goal, if needed. *)
Definition equiv_path_along_equiv {A B : Type} {P : A -> A -> Type}
           (e : B <~> A)
           (K : forall b0 b1 : B, P (e b0) (e b1) <~> b0 = b1)
  : forall a0 a1 : A, P a0 a1 <~> a0 = a1.
A, B: Type
P: A -> A -> Type
e: B <~> A
K: forall b0 b1 : B, P (e b0) (e b1) <~> b0 = b1
forall a0 a1 : A, P a0 a1 <~> a0 = a1
Proof.
A, B: Type
P: A -> A -> Type
e: B <~> A
K: forall b0 b1 : B, P (e b0) (e b1) <~> b0 = b1
forall a0 a1 : A, P a0 a1 <~> a0 = a1
  equiv_intros e b0 b1.
A, B: Type
P: A -> A -> Type
e: B <~> A
K: forall b0 b1 : B, P (e b0) (e b1) <~> b0 = b1
b0, b1: B
P (e b0) (e b1) <~> e b0 = e b1
  refine (_ oE K b0 b1).
A, B: Type
P: A -> A -> Type
e: B <~> A
K: forall b0 b1 : B, P (e b0) (e b1) <~> b0 = b1
b0, b1: B
b0 = b1 <~> e b0 = e b1
  apply equiv_ap'.
Defined.

(** This simply combines the two previous results, a common idiom. Again, it can help Coq to deduce the type family [P] if [revert] is used to move [a0] and [a1] into the goal, if needed. *)
Definition equiv_path_issig_contr {A B : Type} {P : A -> A -> Type}
           (e : B <~> A)
           (Prefl : forall b, P (e b) (e b))
           (cp : forall b1, Contr {b2 : B & P (e b1) (e b2)})
  : forall a0 a1 : A, P a0 a1 <~> a0 = a1.
A, B: Type
P: A -> A -> Type
e: B <~> A
Prefl: forall b : B, P (e b) (e b)
cp: forall b1 : B, Contr {b2 : B & P (e b1) (e b2)}
forall a0 a1 : A, P a0 a1 <~> a0 = a1
Proof.
A, B: Type
P: A -> A -> Type
e: B <~> A
Prefl: forall b : B, P (e b) (e b)
cp: forall b1 : B, Contr {b2 : B & P (e b1) (e b2)}
forall a0 a1 : A, P a0 a1 <~> a0 = a1
  apply (equiv_path_along_equiv e).
A, B: Type
P: A -> A -> Type
e: B <~> A
Prefl: forall b : B, P (e b) (e b)
cp: forall b1 : B, Contr {b2 : B & P (e b1) (e b2)}
forall b0 b1 : B, P (e b0) (e b1) <~> b0 = b1
  intro a0.
A, B: Type
P: A -> A -> Type
e: B <~> A
Prefl: forall b : B, P (e b) (e b)
cp: forall b1 : B, Contr {b2 : B & P (e b1) (e b2)}
a0: B
forall b1 : B, P (e a0) (e b1) <~> a0 = b1
  srapply equiv_path_from_contr.
A, B: Type
P: A -> A -> Type
e: B <~> A
Prefl: forall b : B, P (e b) (e b)
cp: forall b1 : B, Contr {b2 : B & P (e b1) (e b2)}
a0: B
(fun b : B => P (e a0) (e b)) a0
  apply Prefl.
Defined.

(** After [equiv_path_issig_contr], we are left showing the contractibility of a sigma-type whose base and fibers are large nested sigma-types of the same depth.  Moreover, we expect that the types appearing in those two large nested sigma-types "pair up" to form contractible based "path-types".  The following lemma "peels off" the first such pair, whose contractibility can often be found with typeclass search.  The remaining contractibility goal is then simplified by substituting the center of contraction of that first based "path-type", or more precisely a *specific* center that may or may not be the one given by the contractibility instance; the latter freedom sometimes makes things faster and simpler. *)
Definition contr_sigma_sigma (A : Type) (B : A -> Type)
           (C : A -> Type) (D : forall a, B a -> C a -> Type)
           {cac : Contr {x:A & C x} }
           (a : A) (c : C a)
           {ccd : Contr {y:B a & D a y c } }
  : Contr {ab : {x:A & B x} & {y:C ab.1 & D ab.1 ab.2 y} }.
A: Type
B, C: A -> Type
D: forall a : A, B a -> C a -> Type
cac: Contr {x : A & C x}
a: A
c: C a
ccd: Contr {y : B a & D a y c}
Contr
  {ab : {x : A & B x} & {y : C ab.1 & D ab.1 ab.2 y}}
Proof.
A: Type
B, C: A -> Type
D: forall a : A, B a -> C a -> Type
cac: Contr {x : A & C x}
a: A
c: C a
ccd: Contr {y : B a & D a y c}
Contr
  {ab : {x : A & B x} & {y : C ab.1 & D ab.1 ab.2 y}}
  pose (d := (center {y:B a & D a y c}).2).
A: Type
B, C: A -> Type
D: forall a : A, B a -> C a -> Type
cac: Contr {x : A & C x}
a: A
c: C a
ccd: Contr {y : B a & D a y c}
d:= (center {y : B a & D a y c}).2: (fun y : B a => D a y c)
  (center {y : B a & D a y c}).1
Contr
  {ab : {x : A & B x} & {y : C ab.1 & D ab.1 ab.2 y}}
  set (b := (center {y:B a & D a y c}).1) in *.
A: Type
B, C: A -> Type
D: forall a : A, B a -> C a -> Type
cac: Contr {x : A & C x}
a: A
c: C a
ccd: Contr {y : B a & D a y c}
b:= (center {y : B a & D a y c}).1: B a
d:= (center {y : B a & D a y c}).2: (fun y : B a => D a y c) b
Contr
  {ab : {x : A & B x} & {y : C ab.1 & D ab.1 ab.2 y}}
  apply (Build_Contr _ ((a;b);(c;d))).
A: Type
B, C: A -> Type
D: forall a : A, B a -> C a -> Type
cac: Contr {x : A & C x}
a: A
c: C a
ccd: Contr {y : B a & D a y c}
b:= (center {y : B a & D a y c}).1: B a
d:= (center {y : B a & D a y c}).2: (fun y : B a => D a y c) b
forall
y : {ab : {x : A & B x} &
    {y : C ab.1 & D ab.1 ab.2 y}}, ((a; b); c; d) = y
  intros [[a' b'] [c' d']]; cbn in *.
A: Type
B, C: A -> Type
D: forall a : A, B a -> C a -> Type
cac: Contr {x : A & C x}
a: A
c: C a
ccd: Contr {y : B a & D a y c}
b:= (center {y : B a & D a y c}).1: B a
d:= (center {y : B a & D a y c}).2: D a b c
a': A
b': B a'
c': C a'
d': D a' b' c'
((a; b); c; d) = ((a'; b'); c'; d')
  pose (ac' := (a';c')).
A: Type
B, C: A -> Type
D: forall a : A, B a -> C a -> Type
cac: Contr {x : A & C x}
a: A
c: C a
ccd: Contr {y : B a & D a y c}
b:= (center {y : B a & D a y c}).1: B a
d:= (center {y : B a & D a y c}).2: D a b c
a': A
b': B a'
c': C a'
d': D a' b' c'
ac':= (a'; c'): {x : _ & C x}
((a; b); c; d) = ((a'; b'); c'; d')
  pose (bd' := (b';d') : {y:B ac'.1 & D ac'.1 y ac'.2}).
A: Type
B, C: A -> Type
D: forall a : A, B a -> C a -> Type
cac: Contr {x : A & C x}
a: A
c: C a
ccd: Contr {y : B a & D a y c}
b:= (center {y : B a & D a y c}).1: B a
d:= (center {y : B a & D a y c}).2: D a b c
a': A
b': B a'
c': C a'
d': D a' b' c'
ac':= (a'; c'): {x : _ & C x}
bd':= (b'; d') : {y : B ac'.1 & D ac'.1 y ac'.2}: {y : B ac'.1 & D ac'.1 y ac'.2}
((a; b); c; d) = ((a'; b'); c'; d')
  change (((a;b);(c;d)) = ((ac'.1;bd'.1);(ac'.2;bd'.2))
          :> {ab : {x:A & B x} & {y:C ab.1 & D ab.1 ab.2 y} }).
A: Type
B, C: A -> Type
D: forall a : A, B a -> C a -> Type
cac: Contr {x : A & C x}
a: A
c: C a
ccd: Contr {y : B a & D a y c}
b:= (center {y : B a & D a y c}).1: B a
d:= (center {y : B a & D a y c}).2: D a b c
a': A
b': B a'
c': C a'
d': D a' b' c'
ac':= (a'; c'): {x : _ & C x}
bd':= (b'; d') : {y : B ac'.1 & D ac'.1 y ac'.2}: {y : B ac'.1 & D ac'.1 y ac'.2}
((a; b); c; d) = ((ac'.1; bd'.1); ac'.2; bd'.2)
  clearbody ac' bd'; clear a' b' c' d'.
A: Type
B, C: A -> Type
D: forall a : A, B a -> C a -> Type
cac: Contr {x : A & C x}
a: A
c: C a
ccd: Contr {y : B a & D a y c}
b:= (center {y : B a & D a y c}).1: B a
d:= (center {y : B a & D a y c}).2: D a b c
ac': {x : _ & C x}
bd': {y : B ac'.1 & D ac'.1 y ac'.2}
((a; b); c; d) = ((ac'.1; bd'.1); ac'.2; bd'.2)
  destruct (@path_contr {x:A & C x} _ (a;c) ac').
A: Type
B, C: A -> Type
D: forall a : A, B a -> C a -> Type
cac: Contr {x : A & C x}
a: A
c: C a
ccd: Contr {y : B a & D a y c}
b:= (center {y : B a & D a y c}).1: B a
d:= (center {y : B a & D a y c}).2: D a b c
bd': {y : B (a; c).1 & D (a; c).1 y (a; c).2}
((a; b); c; d) = (((a; c).1; bd'.1); (a; c).2; bd'.2)
  destruct (@path_contr {y:B a & D a y c} _ (b;d) bd').
A: Type
B, C: A -> Type
D: forall a : A, B a -> C a -> Type
cac: Contr {x : A & C x}
a: A
c: C a
ccd: Contr {y : B a & D a y c}
b:= (center {y : B a & D a y c}).1: B a
d:= (center {y : B a & D a y c}).2: D a b c
((a; b); c; d) =
(((a; c).1; (b; d).1); (a; c).2; (b; d).2)
  reflexivity.
Defined.

(** This tactic just applies the previous lemma, using a match to figure out the appropriate type families so the user doesn't have to specify them. *)
Ltac contr_sigsig a c :=
  match goal with
  | [ |- Contr (@sig (@sig ?A ?B) (fun ab => @sig (@?C ab) (@?D ab))) ] =>
    (* The lemma only applies when C depends only on the first component of ab, so we need to factor it somehow through pr1. *)
    let C' := fresh in
    transparent assert (C' : {C' : A -> Type & forall ab, C' ab.1 = C ab});
    [ eexists; intros ab; reflexivity
    | nrefine (contr_sigma_sigma A B C'.1 (fun a b => D (a;b)) a c);
      (** In practice, usually the first [Contr] hypothesis can be found by typeclass search, so we try that.  But we don't try on the second one, since often it can't be, and trying can be slow. *)
      [ try exact _ | subst C' ] ]
  end.

(** For examples of the use of this tactic, see for instance [Factorization] and [Idempotents]. *)