Is this a good definition of dependent n-loops

[Kabelo Moiloa]

I will write given an n-loop l : Ω^n(A, a), I denote the type of dependent n-loops over l from u : P(a) to itself by Ω_d^n(l, u). I define it inductively as follows:

Ω_d^n :  Ω^n(A, a) -> P(a) -> U is freely generated by:

reflD : (a : A) -> (u : P(a)) ->  Ω^d_n(refl_a, u).

I initially thought this type would satisfy some version of axiom K, where every dependent n-loop is equal to reflD, but this is not the case and this gives me hope. Tomorrow, I may try to prove it's equivalence with the transport based definition for dimensions 1 and 2, and if I fail I'll check this thread.

[Kabelo Moiloa]

I can't seem to prove that the induction principle satisfied by these "dependent n-loops" is satisfied for dependent 1-loops defined in terms of transport. I'm running out of options, maybe I should use induction-induction or something similar.

[evanc...@gmail.com]

With your definition, Ω_d^n(l, u) ≃ (refl_a = l), which is not what you want. If you squint you can see they are essentially the same inductive type: Ω_d^n( - , u) corresponds to (refl_a = -) and reflD a u to refl_{refl_a}.

Evan

[Kabelo Moiloa]

So, I tried again with the following mutual inductive definition of "dependent n-path". I don't even know if it makes sense but I'm desperate right now:

Given A : U and P : A-> U, define n-paths in A as follows:

_-path : Nat -> U -> U

0-path(A) := A

succ(n)-path(A) := ∑(bd : n-path(A) * n-path(A)) pr1(bd) = pr2(bd)

Define dependent n-boundaries and dependent n-paths denoted as n-pathD as follows:

_-boundaryD : Nat -> U

0-boundaryD : ∑ (a, b : A) P(a) * P(b)

succ(n)-boundaryD: ∑ (p : n-path(A)) (q : n-path(A))  n-pathD(A,P,p) * n-pathD(A,P,q)

_-pathD : (n : N) -> n-boundaryD(A,P) -> succ(n)-path(A) 

0-pathD is freely generated by

reflD0 : (a : A) -> (u : P(a)) -> 0-pathD((a,a,u,u))

succ(n)-pathD is freely generated by 

reflD : (p : n-path(A)) -> (p' : n-pathD(A,P,p)) -> succ(n)-pathD((p,p,p',p'))

On Sunday, August 30, 2015 at 10:51:04 PM UTC+2, Kabelo Moiloa wrote:

[Kabelo Moiloa]

Btw there's a typo instead of ... -> succ(n)-path(A), I meant to say ... -> succ(n)-path(A) -> U.

[Kabelo Moiloa]

Now I have a really elegant definition than I'm sure is correct:

Given A : U and P : A-> U, define n-paths in A as follows:

_-path : Nat -> U -> U

0-path(A) := A

succ(n)-path(A) := ∑(bd : n-path(A) * n-path(A)) pr1(bd) = pr2(bd)

This function generalises pr1 to n-paths:

proj1 : (n : Nat) -> n-path(∑ (x : A) P(x)) -> n-path(A) by induction on n:

proj1(0) := pr1

proj1(succ(n), ((bd1, bd2), p)) := (proj1(n, bd1), proj1(n, bd2), ap(proj1(n, _), p)

We can then define a dependent n-path over p : n-path(A) as literally the type of n-paths which lie over p:

n-pathD(A,P,p) := ∑ (w : n-path(∑ (x : A) P(x))) proj1(w) = p

On Sunday, August 30, 2015 at 10:51:04 PM UTC+2, Kabelo Moiloa wrote:

[Kabelo Moiloa]

Never mind, since based path spaces are contractible the below definition is incorrect.

On Sunday, August 30, 2015 at 10:51:04 PM UTC+2, Kabelo Moiloa wrote:

[evanc...@gmail.com]

Is

Ω_d^n(l, u) :≡ Σq : Ωⁿ(Σa:A.P(a), (a,u)). apⁿ(π₁,q) = l

useful for your purposes, or are you looking for something else? You can define apⁿ : (Σf:A->B.fa = b) -> Ωⁿ(A,a) -> Ωⁿ(B,b) by induction.

Evan

[Kabelo Moiloa]

This is indeed useful for my purposes, thank you. It's quite cool that if you forgo the requirement to keep track of the boundary data required to define n-paths instead of n-loops, an approach similar to my last attempt works.