{- Path Type:
   Copyright (c) Groupoid Infinity, 2014-2018.

   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. -}

module path where
import proto_path

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)

pullback (A B C:U) (f: A -> C) (g: B -> C): U
    = (a: A)
    * (b: B)
    * (   Path C (f a) (g b))

p_1 (A B C: U) (f: A -> C) (g: B -> C): pullback A B C f g -> A = \(x: pullback A B C f g) -> x.1
p_2 (A B C: U) (f: A -> C) (g: B -> C): pullback A B C f g -> B = \(x: pullback A B C f g) -> x.2.1
p_3 (A B C: U) (f: A -> C) (g: B -> C): (x: pullback A B C f g) -> Path C (f x.1) (g x.2.1) = \(x: pullback A B C f g) -> x.2.2

--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])

-- 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