{- Path Type:
   - Reflexivity, Symmetry, Composition, Kan;
   - Connections;
   - Congruence and Respect;
   - Contractability of Singletons;
   - Substitution, Transport, J.

   HoTT 1.12 Identity types
   HoTT 1.12.1 Path induction
   HoTT 2.1 Types are higher groupoids
   HoTT 2.11 Identity type
   HoTT 3.11 Contractibility
   HoTT 6.2 Induction principles and dependent paths.

   Copyright (c) Groupoid Infinity, 2014-2018. -}

module path where

-- Path type and its eliminators
Path     (A: U) (a b: A): U = PathP (<i> A) a b
HPath  (A B: U) (a: A) (b: B) (P: Path U A B) : U = PathP P a b
refl     (A: U) (a: A): Path A a a = <i> a
singl    (A: U) (a: A): U = (x: A) * Path A a x
eta      (A: U) (a: A): singl A a = (a,refl A a)
contr    (A: U) (a b: A) (p: Path A a b): Path (singl A a) (eta A a) (b,p) = <i> (p @ i,<j> p @ i/\j)
sym      (A: U) (a b: A) (p: Path A a b): Path A b a = <i> p @ -i
cong   (A B: U) (f: A->B) (a b: A) (p: Path A a b): Path B (f a) (f b) = <i> f (p @ i)
ap       (A: U) (a x:A) (B:A->U) (f: A->B a) (b: B a) (p: Path A a x): Path (B a) (f a) (f x) = <i> f (p @ i)
trans  (A B: U) (p: Path U A B) (a : A): B = transport p a -- comp p a []
subst    (A: U) (P: A->U) (a b: A) (p: Path A a b) (e: P a): P b = comp (<i> P (p @ i)) e []
inv      (A: U) (a b: A) (p: Path A a b): Path A b a = <i> p @ -i
coerce (A B: U) (p: Path U A B): A -> B = \ (x: A) -> trans A B p x

-- Path induction from HoTT
J   (A: U) (a: A)
    (C: (x : A) -> Path A a x -> U)
    (d: C a (refl A a)) (x: A) (p: Path A a x): C x p
--  = comp  (<i> C (p @ i) (<j> p @ i /\ j)) d [] -- normal form
    = subst (singl A a) T (eta A a) (x, p) (contr A a x p) d
           where T (z : singl A a) : U = C (z.1) (z.2)

-- Computational Rules
trans_comp (A : U) (a : A) : Path A a (trans A A (<_> A) a) = fill (<_> A) a []
subst_comp (A : U) (P : A -> U) (a : A) (e : P a): Path (P a) e (subst A P a a (refl A a) e) = trans_comp (P a) e
J_comp     (A : U) (a : A) (C : (x : A) -> Path A a x -> U)
        (d : C a (refl A a)) : Path (C a (refl A a)) d (J A a C d a (refl A a))
      = subst_comp (singl A a) T (a, refl A a) d where
        T (z : singl A a) : U = C (z.1) (z.2)

symJ (A: U) (a b: A) (p: Path A a b): Path A b a
  = J A a T (refl A a) b p where T (x: A) (_: Path A a x): U = Path A x a

transJ (A: U) (a b c: A) (p: Path A a b) (q: Path A b c): Path A a c
  = undefined

composeUniv (A B C: U) (p: Path U A B) (q: Path U B C): Path U A C
    = comp (<i> Path U A (q @ i)) p []

-- composition operation
composition (A: U) (a b c: A) (p: Path A a b) (q: Path A b c): Path A a c
    = comp (<i> Path A a (q @ i)) p []
--  = subst A (Path A a) b c q p
--  = <i> comp (<j>A) (p @ i) [(i=0) -> <j> a, (i=1) -> q ]

compositionInv (A: U) (a b c: A) (p: Path A a b) (q: Path A b c): Path A c a
    = inv A a c (composition A a b c p q)

join (A: U) (a b: A) (p: Path A a b)
  : PathP (<x> Path A (p @ x) b) p (<_> b)
  = <y x> p @ (x \/ y)

meet (A: U) (a b: A) (p: Path A a b)
  : PathP (<x> Path A a (p @ x)) (<_> a) p
  = <x y> p @ (x /\ y)

app0 (A: U) (a b: A) (p: Path A a b): A = p @ 0
app1 (A: U) (a b: A) (p: Path A a b): A = p @ 1

-- Kan filling operation
kan (A: U) (a b c d: A) (p: Path A a b) (q: Path A a c) (r: Path A b d): Path A c d
    = <i> comp (<j>A) (p @ i) [(i=0) -> q, (i=1) -> r ]

kanOp (A: U) (a: A) (p: Path A a a) (b: A) (q: Path A a b)
  : Path A b b
  = kan A a a b b p q q

kanOpRefl (A: U) (a b: A) (q: Path A a b)
  : Path (Path A b b) (kanOp A a (refl A a) b q) (refl A b)
  = <j i> comp (refl U A) (q @ j) [ (i = 0) -> <k> q @ j \/ k,
                                    (i = 1) -> <k> q @ j \/ k,
                                    (j = 1) -> <k> b ]

transC    (A:U) (a:A) : A = comp (<_>A) a []
lemTransC (A:U) (a:A) : Path A (transC A a) a = <i>comp (<_>A) a [(i=1) -> <_>a]

{-
compInv' (A:U) (a:A)
  : (x:A) (p:Path A a x)
 -> Path (Path A x x) (<_>x) (composition A x a x (<i>p@-i) p)
  = J A a (\  (x:A) (p:Path A a x)
 -> Path (Path A x x) (<_>x) (composition A x a x (<i>p@-i) p)) rem where
    rem : Path (Path A a a) (<_>a) (<i>comp (<_>A) a [(i=0) -> <_>a,
                                                      (i=1) -> <_>a])
        = <j i>comp (<_>A) a [(j=0) -> <_>a,
                              (i=0) -> <_>a,
                              (i=1) -> <_>a]
-}

compInv (A:U) (a b:A) (q:Path A a b)
  : (x:A) (p:Path A b x)
 -> Path (Path A a b) q (composition A a x b (composition A a b x q p) (<i>p@-i))
  = J A b (\ (x:A) (p: Path A b x)
    -> Path (Path A a b) q (composition A a x b (composition A a b x q p) (<i>p@-i))) rem where
    rem : Path (Path A a b) q (<i>comp  (<_>A) (comp (<_>A)(q@i) [(i=0) -> <_>a,
                                                                  (i=1)-><_>b])
                                                                 [(i=0)-><_>a,
                                                                  (i=1)-><_>b])
        = <j i>comp (<_>A) (comp (<_>A)(q@i) [(j=0)-><_>q@i,
                                              (i=0)-><_>a,
                                              (i=1)-><_>b])
                                             [(j=0)-><_>q@i,
                                              (i=0)-><_>a,
                                              (i=1)-><_>b]

-- f o f^-1 = 1_a
compPathInv (A: U) (a b: A) (p: Path A a b) :
  Path (Path A a a) (composition A a b a p (<i> p @ -i)) (<_> a) =
    <k j> comp (<_>A) (p @ j /\ -k)
                    [ (j=0) -> <_> a,
                      (j=1) -> <i> p @ -i /\ -k,
                      (k=1) -> <_> a ]

-- f^-1 o f = 1_b
compInvPath (A: U) (a b: A) (p: Path A a b)
  : Path (Path A b b) (composition A b a b (<i> p @ -i) p)  (<_> b)
  = <j i> comp (<_>A) (p @ -i \/ j)
                    [ (i=0) -> <_> b,
                      (j=1) -> <_> b,
                      (i=1) -> <k> p @ j \/ k ]

-- Groupoid Interpretation

-- id_a o f = f
compPathL (A:U) (a b:A) (p: Path A a b)
  : Path (Path A a b) p (composition A a a b (<_>a) p)
  = <j i> comp (<_>A) a
                    [ (i=0) -> <_> a,
                      (i=1) -> p,
                      (j=0) -> <k>(p@i/\k) ]

-- f o id_b = f
compPathR (A:U) (a b:A) (p: Path A a b)
  : Path (Path A a b) p (composition A a b b p (<_>b))
  = <j i> comp (<_>A) (p@i)
                    [ (i=0) -> <_> a,
                      (i=1) -> <_>b,
                      (j=0) -> <_>(p@i) ]

compPathQ (A:U) (a b c d:A) (f: Path A a b) (g: Path A b c) (h: Path A c d)
        : Path (Path A a d) (composition A a c d (composition A a b c f g) h)
                            (composition A a b d f (composition A b c d g h)) =
  J A a
    (\(b : A) (f : Path A a b) ->
      (c d : A) -> (g : Path A b c) -> (h : Path A c d) ->
        Path (Path A a d) (composition A a c d (composition A a b c f g) h)
                          (composition A a b d f (composition A b c d g h)))
    (\(c d : A) (g : Path A a c) (h : Path A c d) ->
      <i> comp (<_> Path A a d) (composition A a c d g h)
               [ (i = 0) -> <j> composition A a c d (compPathL A a c g @ j) h,
                 (i = 1) -> compPathL A a d (composition A a c d g h) ])
    b f c d g h


isConst (A: U) (f: A -> A): U = (x y: A) -> Path A (f x) (f y)

exConst (A: U): U = (f: A -> A) * isConst A f

mapOnPath (A B: U) (f: A -> B) (a b: A) (p: Path A a b): Path B (f a) (f b)
--  = cong A B f a b p
    = <i> f (p @ i)

mapOverComp (A B : U) (f : A -> B) (a b c : A) (p : Path A a b) (q : Path A b c) :
  Path (Path B (f a) (f c))
       (composition B (f a) (f b) (f c) (<i> f (p @ i)) (<i> f (q @ i)))
       (<i> f (composition A a b c p q @ i)) =
  J A b
    (\(z : A) (r : Path A b z) ->
      Path (Path B (f a) (f z))
           (composition B (f a) (f b) (f z) (<i> f (p @ i)) (<i> f (r @ i)))
           (<i> f (composition A a b z p r @ i)))
    (J A a
      (\(z : A) (p : Path A a z) ->
         Path (Path B (f a) (f z))
              (composition B (f a) (f z) (f z) (<i> f (p @ i)) (<_> f z))
              (<i> f (composition A a z z p (<_> z) @ i)))
      (<i> comp (<_> Path B (f a) (f a)) (<_> f a)
                [ (i = 0) -> <j> kanOpRefl B (f a) (f a) (<_> f a) @ -j,
                  (i = 1) -> <j> mapOnPath A B f a a (kanOpRefl A a a (<_> a) @ -j) ])
      b p) c q

-- subst (A: U) (P: A -> U) (a b: A) (p: Path A a b) (e: P a): P b
--  = comp (<i> P (p @ i)) e [] -- normal form
--  = trans (P a) (P b) (mapOnPath A U P a b p) e

substInv (A: U) (P: A -> U) (a b: A) (p: Path A a b): P b -> P a
    = subst A P b a (<i> p @ -i)

transRefl (A: U) (a: A): Path A (transport (<_> A) a) a
    = <i> comp (<_> A) a [(i=1) -> <_>a]

substPathP (A B: U) (p: Path U A B) (x: A) (y: B) (q: Path B (transport p x) y): PathP p x y
    = transport (<i> PathP p x (q@i)) (<i> comp (<j> p @ (i /\ j)) x [(i=0) -> <_> x])

substToComp (A : U) (a b c : A) (p : Path A b c) (q : Path A a b) :
  Path (Path A a c) (transport (<i> Path A a (p @ i)) q) (composition A a b c q p) =
  <_> composition A a b c q p

-- J is formulated in a form of Paulin-Mohring and implemented
-- using two facts that singleton are contractible and dependent function transport.
JPM (A: U) (a b: A) (P: singl A a -> U) (u: P (eta A a)) (p: Path A a b): P (b,p)
    = subst (singl A a) T (eta A a) (b,p) (contr A a b p) u where T (z : singl A a) : U = P z

data N = Z  | S (n: N)

-- is-n-Type predicate
n_grpd (A: U) (n: N): U = (a b: A) -> rec A a b n where
   rec (A: U) (a b: A) : (k: N) -> U
     = split { Z -> Path A a b ; S n -> n_grpd (Path A a b) n }

isContr     (A: U): U = (x: A) * ((y: A) -> Path A x y)
isProp      (A: U): U = n_grpd A Z
isSet       (A: U): U = n_grpd A (S Z)
isGroupoid  (A: U): U = n_grpd A (S (S Z))
isGrp2      (A: U): U = n_grpd A (S (S (S Z)))
isGrp3      (A: U): U = n_grpd A (S (S (S (S Z))))

-- ∞-Groupoid
inf_grpd (A: U): U
  = (carrier: A)
  * (eq: (a b: A) -> Path A a b)
  * ((a b: A) -> inf_grpd (Path A a b))

isInfinityGroupoid (A: U): U = inf_grpd A

-- n-Types
PROP         : U = (X:U) * isProp X
SET          : U = (X:U) * isSet X
GROUPOID     : U = (X:U) * isGroupoid X
INF_GROUPOID : U = (X:U) * isInfinityGroupoid X

-- if there's a path from a type then there is a path from every element
elemPathP (A B: U) (p: Path U A B) (a: A): (p': Path U A B) * (b: B) * PathP p' a b
  = comp (<i> P (p @ i)) (refl U A, a, refl A a) [] where
  P (X: U): U = (p: Path U A X) * (x: X) * PathP p a x

isContrSingl (A:U) (a:A): isContr (singl A a)
  = ((a,refl A a),\ (z:singl A a) -> contr A a z.1 z.2)

singl' (A: U) (a: A): U = (x:A) * Path A x a
contr' (A: U) (a b: A) (p: Path A a b): Path (singl' A b) (b,refl A b) (a,p) = <i> (p @ -i,<j> p @ -i\/j)
isContrSingl' (A:U) (a:A): isContr (singl' A a)
  = ((a,refl A a),\ (z:singl' A a) -> contr' A z.1 a z.2)

isContrPath (A: U): isContr ((B: U) * Path U A B) = (ctr,ctrpath) where
  ctr: (B: U) * Path U A B = (A,<_> A)
  ctrpath (q: (B: U) * Path U A B): Path ((B: U) * Path U A B) ctr q = <i> (q.2 @ i,<j> q.2 @ i/\j)

isPathContr (A: U) (cA: isContr A) (x y:A) : isContr (Path A x y) = (p0,q) where
  a: A = cA.1
  f: (x:A) -> Path A a x = cA.2
  p0: Path A x y = <i>comp (<j>A) a [(i=0) -> f x,(i=1) -> f y]
  q (p:Path A x y): Path (Path A x y) p0 p
    = <j i>comp (<k>A) a [(i=0) -> f x,
                          (i=1) -> f y,
                          (j=1) -> f (p@i),
                          (j=0) -> <k>comp (<l>A) a [(k=0) -> <l>a,
                                                     (i=0) -> <l>f x@k/\l,
                                                     (i=1) -> <l>f y@k/\l] ]

lemFib1 (A:U) (F G : A -> U) (a:A) (fa : F a -> G a)
      : (x:A) (p : Path A a x) -> (fx : F x -> G x) ->
        Path U (Path (F a -> G x) (\ (u:F a) -> subst A G a x p (fa u)) (\ (u:F a) -> fx (subst A F a x p u)))
               (PathP (<i>F (p@i) -> G (p@i)) fa fx)
      = J A a (\ (x:A) (p : Path A a x) -> (fx : F x -> G x) ->
        Path U (Path (F a -> G x) (\ (u:F a) -> subst A G a x p (fa u)) (\ (u:F a) -> fx (subst A F a x p u)))
               (PathP (<i>F (p@i) -> G (p@i)) fa fx)) r where
      r (ga: F a -> G a)
            : Path U (Path (F a -> G a) (\ (u:F a) -> transC (G a) (fa u)) (\ (u:F a) -> ga (transC (F a) u)))
                     (Path (F a -> G a) fa ga)
        = <j>Path (F a -> G a) (\ (u:F a) -> lemTransC (G a) (fa u)@j) (\ (u : F a) -> ga (lemTransC (F a) u@j))

lemFib2 (A:U) (F:A->U) (a b:A) (p:Path A a b) (u:F a)
      : (c:A) (q:Path A b c) -> Path (F c) (subst A F b c q (subst A F a b p u)) (subst A F a c (composition A a b c p q) u)
      = J A b (\ (c:A) (q:Path A b c) -> Path (F c) (subst A F b c q (subst A F a b p u)) (subst A F a c (composition A a b c p q) u)) r where
      x : Path (F b) (subst A F a b p u) (subst A F b b (<_>b) (subst A F a b p u)) =  <i>lemTransC (F b) (subst A F a b p u) @ -i
      y : Path (F b) (subst A F a b p u) (subst A F a b (composition A a b b p (<_>b)) u) = <i>subst A F a b (compPathR A a b p @ i) u
      r : Path (F b) (subst A F b b (<_>b) (subst A F a b p u)) (subst A F a b (composition A a b b p (<_>b)) u)
        = comp (<i>Path (F b) (x@i) (y@i)) (<_>subst A F a b p u) []

corFib1 (A: U) (F G: A -> U) (a: A) (fa ga: F a -> G a) (p: Path A a a)
        (h: (u: F a) -> Path (G a) (subst A G a a p (fa u)) (ga (subst A F a a p u)))
      : PathP (<i>F (p@i) -> G (p@i)) fa ga
      = comp (lemFib1 A F G a fa a p ga) (<i>\ (u:F a) -> h u @ i) []

-- not used here
lem1 (B:U) (F: B -> U) (y: B) (x: F y)
       : PathP (<i>U) (PathP (<i>F ((refl B y)@i)) x x)
                (Path (F y) (transport (<i>F((refl B y)@i)) x) x)
       = <j> PathP (<i>F ((refl B y)@j\/i))
                   (comp (<i>F ((refl B y)@j/\i)) x [(j=0)-><_>x]) x