/-
Copyright (c) 2014 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Module: init.path
Author: Floris van Doorn

Theorems about functions with multiple arguments
-/

variables {A U V W X Y Z : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type}
          {E : Πa b c, D a b c → Type}
variables {a a' : A} {u u' : U} {v v' : V} {w w' : W} {x x' x'' : X} {y y' : Y} {z z' : Z}
          {b : B a} {b' : B a'}
          {c : C a b} {c' : C a' b'}
          {d : D a b c} {d' : D a' b' c'}
          {e : E a b c d} {e' : E a' b' c' d'}

namespace eq
  /-
    Naming convention:
      The theorem which states how to construct an path between two function applications is
        api₀i₁...iₙ.
      Here i₀, ... iₙ are digits, n is the arity of the function(s),
        and iⱼ specifies the dimension of the path between the jᵗʰ argument
        (i₀ specifies the dimension of the path between the functions).
      A value iⱼ ≡ 0 means that the jᵗʰ arguments are definitionally equal
      The functions are non-dependent, except when the theorem name contains trailing zeroes
        (where the function is dependent only in the arguments where it doesn't result in any
         transports in the theorem statement).
      For the fully-dependent versions (except that the conclusion doesn't contain a transport)
      we write
        apdi₀i₁...iₙ.

      For versions where only some arguments depend on some other arguments,
      or for versions with transport in the conclusion (like apd), we don't have a
      consistent naming scheme (yet).

      We don't prove each theorem systematically, but prove only the ones which we actually need.
  -/

  definition homotopy2 [reducible] (f g : Πa b, C a b)         : Type :=
  Πa b, f a b = g a b
  definition homotopy3 [reducible] (f g : Πa b c, D a b c)     : Type :=
  Πa b c, f a b c = g a b c
  definition homotopy4 [reducible] (f g : Πa b c d, E a b c d) : Type :=
  Πa b c d, f a b c d = g a b c d

  notation f `∼2`:50 g := homotopy2 f g
  notation f `∼3`:50 g := homotopy3 f g

  definition ap011 (f : U → V → W) (Hu : u = u') (Hv : v = v') : f u v = f u' v' :=
  by cases Hu; congruence; repeat assumption

  definition ap0111 (f : U → V → W → X) (Hu : u = u') (Hv : v = v') (Hw : w = w')
      : f u v w = f u' v' w' :=
  by cases Hu; congruence; repeat assumption

  definition ap01111 (f : U → V → W → X → Y) (Hu : u = u') (Hv : v = v') (Hw : w = w') (Hx : x = x')
      : f u v w x = f u' v' w' x' :=
  by cases Hu; congruence; repeat assumption

  definition ap011111 (f : U → V → W → X → Y → Z)
    (Hu : u = u') (Hv : v = v') (Hw : w = w') (Hx : x = x') (Hy : y = y')
      : f u v w x y = f u' v' w' x' y' :=
  by cases Hu; congruence; repeat assumption

  definition ap0111111 (f : U → V → W → X → Y → Z → A)
    (Hu : u = u') (Hv : v = v') (Hw : w = w') (Hx : x = x') (Hy : y = y') (Hz : z = z')
      : f u v w x y z = f u' v' w' x' y' z' :=
  by cases Hu; congruence; repeat assumption

  definition ap010 (f : X → Πa, B a) (Hx : x = x') : f x ∼ f x' :=
  by intros; cases Hx; reflexivity

  definition ap0100 (f : X → Πa b, C a b) (Hx : x = x') : f x ∼2 f x' :=
  by intros; cases Hx; reflexivity

  definition ap01000 (f : X → Πa b c, D a b c) (Hx : x = x') : f x ∼3 f x' :=
  by intros; cases Hx; reflexivity

  definition apd011 (f : Πa, B a → Z) (Ha : a = a') (Hb : (Ha ▹ b) = b')
      : f a b = f a' b' :=
  by cases Ha; cases Hb; reflexivity

  definition apd0111 (f : Πa b, C a b → Z) (Ha : a = a') (Hb : (Ha ▹ b) = b')
    (Hc : apd011 C Ha Hb ▹ c = c')
      : f a b c = f a' b' c' :=
  by cases Ha; cases Hb; cases Hc; reflexivity

  definition apd01111 (f : Πa b c, D a b c → Z) (Ha : a = a') (Hb : (Ha ▹ b) = b')
    (Hc : apd011 C Ha Hb ▹ c = c') (Hd : apd0111 D Ha Hb Hc ▹ d = d')
      : f a b c d = f a' b' c' d' :=
  by cases Ha; cases Hb; cases Hc; cases Hd; reflexivity

  definition apd011111 (f : Πa b c d, E a b c d → Z) (Ha : a = a') (Hb : (Ha ▹ b) = b')
    (Hc : apd011 C Ha Hb ▹ c = c') (Hd : apd0111 D Ha Hb Hc ▹ d = d')
    (He : apd01111 E Ha Hb Hc Hd ▹ e = e')
    : f a b c d e = f a' b' c' d' e' :=
  by cases Ha; cases Hb; cases Hc; cases Hd; cases He; reflexivity

  definition apd100 {f g : Πa b, C a b} (p : f = g) : f ∼2 g :=
  λa b, apd10 (apd10 p a) b

  definition apd1000 {f g : Πa b c, D a b c} (p : f = g) : f ∼3 g :=
  λa b c, apd100 (apd10 p a) b c

  /- some properties of these variants of ap -/

  -- we only prove what is needed somewhere

  definition ap010_con (f : X → Πa, B a) (p : x = x') (q : x' = x'') :
    ap010 f (p ⬝ q) a = ap010 f p a ⬝ ap010 f q a :=
  eq.rec_on q (eq.rec_on p idp)

  definition ap010_ap (f : X → Πa, B a) (g : Y → X) (p : y = y') :
    ap010 f (ap g p) a = ap010 (λy, f (g y)) p a :=
  eq.rec_on p idp

  /- the following theorems are function extentionality for functions with multiple arguments -/

  definition eq_of_homotopy2 {f g : Πa b, C a b} (H : f ∼2 g) : f = g :=
  eq_of_homotopy (λa, eq_of_homotopy (H a))

  definition eq_of_homotopy3 {f g : Πa b c, D a b c} (H : f ∼3 g) : f = g :=
  eq_of_homotopy (λa, eq_of_homotopy2 (H a))

  definition eq_of_homotopy2_id (f : Πa b, C a b)
    : eq_of_homotopy2 (λa b, idpath (f a b)) = idpath f :=
  begin
    transitivity eq_of_homotopy (λ a, idpath (f a)),
      {apply (ap eq_of_homotopy), apply eq_of_homotopy, intros, apply eq_of_homotopy_idp},
      apply eq_of_homotopy_idp
  end

  definition eq_of_homotopy3_id (f : Πa b c, D a b c)
    : eq_of_homotopy3 (λa b c, idpath (f a b c)) = idpath f :=
  begin
    transitivity _,
      {apply (ap eq_of_homotopy), apply eq_of_homotopy, intros, apply eq_of_homotopy2_id},
      apply eq_of_homotopy_idp
  end

end eq

open eq is_equiv
namespace funext
  definition is_equiv_apd100 [instance] (f g : Πa b, C a b) : is_equiv (@apd100 A B C f g) :=
  adjointify _
             eq_of_homotopy2
             begin
               intro H, esimp [apd100, eq_of_homotopy2, function.compose],
               apply eq_of_homotopy, intro a,
               apply concat, apply (ap (λx, apd10 (x a))), apply (right_inv apd10),
               apply (right_inv apd10)
             end
             begin
               intro p, cases p, apply eq_of_homotopy2_id
             end

  definition is_equiv_apd1000 [instance] (f g : Πa b c, D a b c)
    : is_equiv (@apd1000 A B C D f g) :=
  adjointify _
             eq_of_homotopy3
             begin
               intro H, apply eq_of_homotopy, intro a,
               apply concat,
                 {apply (ap (λx, @apd100 _ _ (λ(b : B a)(c : C a b), _) _ _ (x a))),
                   apply (right_inv apd10)},
--TODO: remove implicit argument after #469 is closed
               apply (@right_inv _ _ apd100 !is_equiv_apd100) --is explicit argument needed here?
             end
             begin
               intro p, cases p, apply eq_of_homotopy3_id
             end
end funext

namespace eq
  open funext
  local attribute funext.is_equiv_apd100 [instance]
  protected definition homotopy2.rec_on {f g : Πa b, C a b} {P : (f ∼2 g) → Type}
    (p : f ∼2 g) (H : Π(q : f = g), P (apd100 q)) : P p :=
  right_inv apd100 p ▹ H (eq_of_homotopy2 p)

  protected definition homotopy3.rec_on {f g : Πa b c, D a b c} {P : (f ∼3 g) → Type}
    (p : f ∼3 g) (H : Π(q : f = g), P (apd1000 q)) : P p :=
  right_inv apd1000 p ▹ H (eq_of_homotopy3 p)

  definition apd10_ap (f : X → Πa, B a) (p : x = x')
    : apd10 (ap f p) = ap010 f p :=
  eq.rec_on p idp

  definition eq_of_homotopy_ap010 (f : X → Πa, B a) (p : x = x')
    : eq_of_homotopy (ap010 f p) = ap f p :=
  inv_eq_of_eq !apd10_ap⁻¹

  definition ap_eq_ap_of_homotopy {f : X → Πa, B a} {p q : x = x'} (H : ap010 f p ∼ ap010 f q)
    : ap f p = ap f q :=
  calc
    ap f p = eq_of_homotopy (ap010 f p) : eq_of_homotopy_ap010
       ... = eq_of_homotopy (ap010 f q) : eq_of_homotopy H
       ... = ap f q                     : eq_of_homotopy_ap010

end eq