# Library UniMath.MoreFoundations.PathsOver

This file contains the definition of paths over a path, together with some facts about them developed by Marc Bezem and Ulrik Buchholtz.

## Paths over paths in families of types

Local Set Implicit Arguments.
Local Unset Strict Implicit.

Declare Scope pathsover.
Delimit Scope pathsover with pathsover.
Local Open Scope pathsover.

Definition PathOver {X:Type} {x x':X} {Y : X Type} (y : Y x) (y' : Y x') (p:x=x') : Type.
Proof.
induction p.
exact (y=y').
Defined.

Definition PathOverToPathPair {X:Type} {x x':X} {Y : X Type} (y : Y x) (y' : Y x') (p:x=x') :
PathOver y y' p PathPair (x,,y) (x',,y').
Proof.
intros q. induction p. (idpath x). cbn. exact q.
Defined.

Definition apd {X:Type} {Y : X Type} (s : x, Y x) {x x':X} (p : x = x') :
PathOver (s x) (s x') p.
Proof.
now induction p.
Defined.

Definition PathOverToTotalPath {X:Type} {x x':X} {Y : X Type} (y : Y x) (y' : Y x') (p:x=x') :
PathOver y y' p (x,,y) = (x',,y').
Proof.
intros q.
exact (invmap (total2_paths_equiv Y (x,, y) (x',, y'))
(PathOverToPathPair q)).
Defined.

Lemma PathOverUniqueness {X:Type} {x x':X} {Y : X Type} (y : Y x) (p:x=x') :
∃! (y' : Y x'), PathOver y y' p.
Proof.
induction p. apply iscontrcoconusfromt.
Defined.

Definition PathOver_inConstantFamily (X Y:Type) (x x':X) (y y':Y) (p:x=x') :
y = y' PathOver (Y := (λ x, Y)) y y' p.
Proof.
intros q.
unfold PathOver.
induction p.
change (y=y').
exact q.
Defined.

Definition stdPathOver {X:Type} {x x':X} {Y : X Type} (y : Y x) (p:x=x')
: PathOver y (transportf Y p y) p.
Proof.
induction p. reflexivity.
Defined.

Definition stdPathOver' {X:Type} {x x':X} {Y : X Type} (y' : Y x') (p:x=x')
: PathOver (transportb Y p y') y' p.
Proof.
now induction p.
Defined.

Definition identityPathOver {X:Type} {x:X} {Y : X Type} (y : Y x) : PathOver y y (idpath x)
:= idpath y.

Definition pathOverIdpath {X:Type} {x:X} {Y : X Type} (y y' : Y x) : PathOver y y' (idpath x) = (y = y')
:= idpath _.

Definition toPathOverIdpath {X:Type} {x:X} {Y : X Type} (y y' : Y x) : y = y' PathOver y y' (idpath x)
:= idfun _.

Local Notation "'∇' q" := (toPathOverIdpath q) (at level 10) : pathsover.

Definition fromPathOverIdpath {X:Type} {x:X} {Y : X Type} (y y' : Y x) : PathOver y y' (idpath x) y = y'
:= idfun _.

Local Notation "'Δ' q" := (fromPathOverIdpath q) (at level 10) : pathsover.

Definition inductionPathOver {X:Type} {x:X} {Y : X Type} (y : Y x)
(T : x' (y' : Y x') (p : x = x'), PathOver y y' p Type)
(t : T x y (idpath x) (identityPathOver y)) :
x' (y' : Y x') (p : x = x') (q : PathOver y y' p), T x' y' p q.
Proof.
intros. induction p, q. exact t.
Defined.

Definition transportPathOver {X:Type} {x x':X} {Y : X Type} (y : Y x) (y' : Y x') (p:x=x')
(q : PathOver y y' p)
(T : (a:X) (b:Y a), Type) : T x y T x' y'.
Proof.
now induction p, q.
Defined.

Definition transportPathOver' {X:Type} {x x':X} {Y : X Type} (y : Y x) (y' : Y x') (p:x=x')
(q : PathOver y y' p)
(T : (a:X) (b:Y a), Type) : T x' y' T x y.
Proof.
now induction p, q.
Defined.

Definition composePathOver {X:Type} {x x' x'':X} {Y : X Type} {y : Y x} {y' : Y x'} {y'' : Y x''}
{p:x=x'} {p':x'=x''} : PathOver y y' p PathOver y' y'' p' PathOver y y'' (p @ p').
Proof.
induction p, p'. exact pathscomp0.
Defined.

Local Notation "x * y" := (composePathOver x y) : pathsover.

Definition composePathOverPath {X:Type} {x x':X} {Y : X Type} {y : Y x} {y' y'' : Y x'}
{p:x=x'} : PathOver y y' p y' = y'' PathOver y y'' p.
Proof.
intros q e. now induction e.
Defined.

Local Notation "q ⟥ e" := (composePathOverPath q e) (at level 56, left associativity) : pathsover.

Definition composePathPathOver {X:Type} {x' x'':X} {Y : X Type} {y y': Y x'} {y'' : Y x''}
{p:x'=x''} : y = y' PathOver y' y'' p PathOver y y'' p.
Proof.
intros e q. now induction e.
Defined.

Local Notation "e ⟤ q" := (composePathPathOver e q) (at level 56, left associativity) : pathsover.

Definition composePathOverLeftUnit {X:Type} {x x':X} {Y : X Type} (y : Y x) (y' : Y x') (p:x=x') (q:PathOver y y' p) :
identityPathOver y × q = q.
Proof.
now induction p.
Defined.

Definition composePathOverRightUnit {X:Type} {x x':X} {Y : X Type} (y : Y x) (y' : Y x') (p:x=x') (q:PathOver y y' p) :
q × identityPathOver y' = transportb (PathOver y y') (pathscomp0rid _) q.
Proof.
now induction p, q.
Defined.

Definition assocPathOver {X:Type} {x x' x'' x''':X}
{Y : X Type} {y : Y x} {y' : Y x'} {y'' : Y x''} {y''' : Y x'''}
{p:x=x'} {p':x'=x''} {p'':x''=x'''}
(q : PathOver y y' p) (q' : PathOver y' y'' p') (q'' : PathOver y'' y''' p'') :
transportf _ (path_assoc p p' p'') (q × composePathOver q' q'')
=
composePathOver q q' × q''.
Proof.
induction p, p', p'', q, q', q''. reflexivity.
Defined.

Definition inversePathOver {X:Type} {x x':X} {Y : X Type} {y : Y x} {y' : Y x'} {p:x=x'} :
PathOver y y' p PathOver y' y (!p).
Proof.
intros q. induction p, q. reflexivity.
Defined.

Definition inversePathOver' {X:Type} {x x':X} {Y : X Type} {y : Y x} {y' : Y x'} {p:x'=x} :
PathOver y y' (!p) PathOver y' y p.
Proof.
intros q. induction p, q. reflexivity.
Defined.

Local Notation "q '^-1'" := (inversePathOver q) : pathsover.

Definition inversePathOverIdpath {X:Type} {x:X} {Y : X Type} (y y' : Y x) (e : y = y') :
inversePathOver ( e) = (!e).
Proof.
reflexivity.
Defined.

Definition inversePathOverIdpath' {X:Type} {x:X} {Y : X Type} (y y' : Y x) (e : y = y') :
inversePathOver' ( e : PathOver y y' (! idpath x)) = (!e).
Proof.
reflexivity.
Defined.

Definition inverseInversePathOver {X:Type} {Y : X Type} {x:X} {y : Y x} :
{x':X} {y' : Y x'} {p:x=x'} (q : PathOver y y' p),
transportf _ (pathsinv0inv0 p) (q^-1^-1) = q.
Proof.
now use inductionPathOver.
Defined.

Lemma Lemma023 (A:Type) (B:AType) (a1 a2 a3:A)
(b1:B a1) (b2:B a2) (b3:B a3)
(p1:a1=a2) (p2:a2=a3)
(q:PathOver b1 b2 p1) :
isweq (composePathOver q : PathOver b2 b3 p2 PathOver b1 b3 (p1@p2)).
Proof.
induction p1, p2, q. apply idisweq.
Defined.

Definition composePathOver_weq (A:Type) (a1 a2 a3:A) (B:AType)
(b1:B a1) (b2:B a2) (b3:B a3)
(p1:a1=a2) (p2:a2=a3)
(q:PathOver b1 b2 p1)
: PathOver b2 b3 p2 PathOver b1 b3 (p1@p2)
:= make_weq (composePathOver q) (Lemma023 _).

Lemma Lemma0_2_4 (A:Type) (B:AType) (a1 a2:A)
(b1:B a1) (b2:B a2) (p q:a1=a2) (α : p=q) :
isweq ((transportf (PathOver b1 b2) α) : PathOver b1 b2 p PathOver b1 b2 q).
Proof.
induction α. apply idisweq.
Defined.

Definition cp
(A:Type) (a1 a2:A) (p q:a1=a2) (α : p=q)
(B:AType) (b1:B a1) (b2:B a2) :
PathOver b1 b2 p PathOver b1 b2 q
:= make_weq (transportf _ α) (Lemma0_2_4 α).

Arguments cp {_ _ _ _ _} _ {_ _ _}.

Definition composePathOverPath_compute {X:Type} {x x':X} {Y : X Type} {y : Y x} {y' y'' : Y x'}
{p:x=x'} (q : PathOver y y' p) (e : y' = y'') :
q e = cp (pathscomp0rid p) (q × e).
Proof.
now induction p, q, e.
Defined.

Definition composePathPathOver_compute {X:Type} {x' x'':X} {Y : X Type} {y y': Y x'} {y'' : Y x''}
{p:x'=x''} (e : y = y') (q : PathOver y' y'' p) :
e q = e × q.
Proof.
now induction p.
Defined.

Definition cp_idpath
(A:Type) (a1 a2:A) (p:a1=a2)
(B:AType) (b1:B a1) (b2:B a2) (u:PathOver b1 b2 p) :
cp (idpath p) u = u.
Proof.
reflexivity.
Defined.

Definition cp_left
(A:Type) (a2 a3:A) (p p':a2=a3) (α:p=p')
(B:AType) (b1 b2:B a2) (b3:B a3)
(r:PathOver b1 b2 (idpath a2))
(q:PathOver b2 b3 p) :
r × cp α q = cp α (r×q).
Proof.
now induction r, α.
Defined.

Definition cp_right
(A:Type) (a1 a2:A) (p p':a1=a2) (α:p=p')
(B:AType) (b1:B a1) (b2 b3:B a2)
(q:PathOver b1 b2 p)
(r:PathOver b2 b3 (idpath a2)) :
cp α q × r = cp (maponpaths (λ p, p @ idpath a2) α) (q×r).
Proof.
now induction r, α.
Defined.

Definition cp_in_family
(A:Type) (a1 a2:A)
(T:Type) (t0 t1:T) (v:t0=t1) (p:Ta1=a2)
(B:AType) (b1:B a1) (b2:B a2) (s : t, PathOver b1 b2 (p t)) :
cp (maponpaths p v) (s t0) = s t1.
Proof.
now induction v.
Defined.

Definition cp_irrelevance
(A:Type) (B:AType) (a1 a2:A) (b1:B a1) (b2:B a2) (p q:a1=a2) (α β: p=q) :
isofhlevel 3 A cp (b1:=b1) (b2:=b2) α = cp (b1:=b1) (b2:=b2) β.
Proof.
intros ih. apply (maponpaths (λ α, cp α)). apply ih.
Defined.

Local Goal (A:Type) (B:AType) (a1 a2:A) (b1:B a1) (b2:B a2) (p q:a1=a2) (α : p=q)
(r : PathOver b1 b2 p) (s : PathOver b1 b2 q),
(cp α r = s) = (PathOver r s α).
Proof.
intros. induction α, p. reflexivity.
Defined.

Definition inverse_cp_p
(A:Type) (B:AType) (a1 a2:A) (b1:B a1) (b2:B a2)
(p q:a1=a2) (α : p=q) (t : PathOver b1 b2 p) :
cp (! α) (cp α t) = t.
Proof.
now induction α.
Defined.

Definition inverse_cp_p'
(A:Type) (B:AType) (a1 a2:A) (b1:B a1) (b2:B a2)
(p q:a1=a2) (α : p=q)
(t : PathOver b1 b2 p) (u : PathOver b1 b2 q) :
PathOver t u α PathOver u t (!α).
Proof.
exact inversePathOver.
Defined.

Definition inverse_cp_p''
(A:Type) (B:AType) (a1 a2:A) (b1:B a1) (b2:B a2)
(p q:a1=a2) (α : p=q)
(t : PathOver b1 b2 p) (u : PathOver b1 b2 q) :
PathOver t u α PathOver u t (!α).
Proof.
intros k. induction α, p, k. reflexivity.
Defined.

Lemma inverse_cp_p_compare
(A:Type) (B:AType) (a1 a2:A) (b1:B a1) (b2:B a2)
(p q:a1=a2) (α : p=q)
(t : PathOver b1 b2 p) (u : PathOver b1 b2 q)
(k : PathOver t u α) :
inverse_cp_p' k = inverse_cp_p'' k.
Proof.
induction α,p. reflexivity.
Defined.

Definition cp_inverse_cp
(A:Type) (B:AType) (a1 a2:A) (b1:B a1) (b2:B a2)
(p q:a1=a2) (α : p=q) (t : PathOver b1 b2 q) :
cp α (cp (! α) t) = t.
Proof.
now induction α.
Defined.

Definition composePathOverRightInverse {X:Type} {x x':X} {Y : X Type}
{y : Y x} {y' : Y x'} {p:x=x'} (q : PathOver y y' p) :
q × q^-1 = cp (!pathsinv0r p) (identityPathOver y).
Proof.
now induction p, q.
Defined.

Definition composePathOverLeftInverse {X:Type} {x x':X} {Y : X Type}
{y : Y x} {y' : Y x'} {p:x=x'} (q : PathOver y y' p) :
q^-1 × q = cp (!pathsinv0l p) (identityPathOver y').
Proof.
now induction p, q.
Defined.

Lemma cp_pathscomp0
(A:Type) (B:AType) (a1 a2:A)
(b1:B a1) (b2:B a2) (p q r:a1=a2) (α : p=q) (β : q=r)
(s : PathOver b1 b2 p) :
cp (b1:=b1) (b2:=b2) (α @ β) s = cp β (cp α s).
Proof.
now induction α.
Defined.

Definition apstar
(A:Type) (a1 a2 a3:A) (p p':a1=a2) (q q':a2=a3) :
p=p' q=q' p @ q = p' @ q'.
Proof.
intros α β. induction α, p. exact β.
Defined.

Definition cp_apstar
(A:Type) (B:AType) (a1 a2 a3:A)
(p p':a1=a2) (q q':a2=a3) (α : p=p') (β : q=q')
(b1:B a1) (b2:B a2) (b3:B a3)
(pp : PathOver b1 b2 p) (qq : PathOver b2 b3 q) :
cp (apstar α β) (pp × qq) = cp α pp × cp β qq.
Proof.
now induction p, α, β.
Defined.

Definition cp_apstar'
(A:Type) (B:AType) (a1 a2:A)
(p:a2=a1) (p':a1=a2) (α : !p=p')
(b1:B a1) (b2:B a2)
(pp : PathOver (Y:=B) b2 b1 p) :
cp α (pp^-1) = inversePathOver' (cp (invrot α) pp).
Proof.
now induction α, p.
Defined.

Module PathsOverNotations.
Notation "'Δ' q" := (fromPathOverIdpath q) (at level 10) : pathsover.
Notation "'∇' q" := (toPathOverIdpath q) (at level 10) : pathsover.
Notation "x * y" := (composePathOver x y) : pathsover.
Notation "q ⟥ e" := (composePathOverPath q e) (at level 56, left associativity) : pathsover.
Notation "e ⟤ q" := (composePathPathOver e q) (at level 56, left associativity) : pathsover.
Notation "q '^-1'" := (inversePathOver q) : pathsover.
End PathsOverNotations.