Etale Map

[5HT]

Please forgive me this waterfall, I have another question! I'm trying to encode Etale Maps from Felix Wellen dissertation (port from Agda) and it seems like nominal typing error for me:

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

pb1 (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
pb2 (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
pb3 (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

induced (Z A B C: U) (f: A -> C) (g: B -> C)
        (z1: Z -> A) (z2: Z -> B)
        (h: (z:Z) -> Path C ((o Z A C f z1) z) (((o Z B C g z2)) z))
      : Z -> pullback A B C f g
      = \(z: Z) -> ((z1 z),(z2 z),h z)

pullbackSq (Z A B C: U) (f: A -> C) (g: B -> C) (z1: Z -> A) (z2: Z -> B): U
         = (h: (z:Z) -> Path C ((o Z A C f z1) z) (((o Z B C g z2)) z))
         * isEquiv Z (pullback A B C f g) (induced Z A B C f g z1 z2 h)

isPullbackSq (Z A B C: U) (f: A -> C) (g: B -> C) (z1: Z -> A) (z2: Z -> B)
             (h: (z:Z) -> Path C ((o Z A C f z1) z) (((o Z B C g z2)) z)): U
           = isEquiv Z (pullback A B C f g) (induced Z A B C f g z1 z2 h)

-- \Im modality, represents infinitesimal shape constructions

Im : U -> U = undefined
ImUnit (A: U) : A -> Im A = undefined

isCoreduced (A:U): U = isEquiv A (Im A) (ImUnit A)
ImCoreduced (A:U): isCoreduced (Im A) = undefined

ImRecursion (A B: U) (c: isCoreduced B) (f: A -> B) 
  : Im A -> B = undefined
ImComputeRecursion(A B:U)(c:isCoreduced B)(f: A->B)(a:A)
  : PathP(<i>B)((ImRecursion A B c f)(ImUnit A a))(f a) = undefined

ImApp (A B: U) (f: A -> B): Im A -> Im B 
  = ImRecursion A (Im B) (ImCoreduced B) (o A B (Im B) (ImUnit B) f)
ImNaturality (A B: U) (f: A -> B): (a: A)
  -> Path (Im B) ((ImUnit B) (f a)) ((ImApp A B f) (ImUnit A a)) 
  = undefined

ImInduction (A:U)(B:Im A->U)(x: (a: Im A)->isCoreduced(B a)) (y:(a: A)->B(ImUnit A a))
  : (a:Im A)->B a = undefined
ImComputeInduction (A:U)(B:Im A->U) (c:(a:Im A)
  -> isCoreduced(B a)) (f:(a:A)->B(ImUnit A a))(a:A)
  : Path (B (ImUnit A a)) (f a) ((ImInduction A B c f) (ImUnit A a)) = undefined

isÉtaleMap (A B: U) (f: A -> B): U
  = isPullbackSq A iA B (Im B) x y w f h where
  iA : U = Im A
  iB : U = Im B
  x: iA -> iB = ImApp  A B f
  y:  B -> iB = ImUnit B
  w:  A -> iA = ImUnit A
  c1: A -> iB = o A iA iB x w
  c2: A -> iB = o A B  iB y f
  T2: U = (a:A) -> Path iB (c1 a) (c2 a)
  h: T2 = ImNaturality A B f

-- Checking: isÉtaleMap
-- Type checking failed: check conv:
-- Pi A ((\(a : A) -> Path (Im B) (ImUnit B (f a))
            (ImApp A B f (ImUnit A a))) (A = A, B = B, f = f))
-- /=
-- Pi A ((\(a : A) -> Path N (c1 a) (c2 a)) (A = A, B = B, f = f))
-- >

Have I mistaken? Here is the idea that we use undefined for infinitesimal constructions without proofs and try to reason with them.

[mortberg]

You have the ImNaturality Path the wrong way around. If I do:

  h: T2 = \(a : A) -> <i> ImNaturality A B f a @ -i

it works. I would suggest you write:

ImNaturality (A B: U) (f: A -> B): (a: A)
  -> Path (Im B) ((ImApp A B f) (ImUnit A a)) ((ImUnit B) (f a)) 
  = undefined

I wonder if all of these undefined are necessary? Aren't Im definable as a HIT? You would have one constructor for the unit and a higher constructor for the fact that it's an equivalence. If you do that this would be more interesting as everything will compute.

[5HT]

I will try!

[mortberg]

I'll close this issue now as it was just a Path being defined the wrong way, but feel free to keep discussing in this thread.

[mortberg]

I discussed this with Felix now and it's more complicated than I thought. The HIT will be some form localization, but you will need to either postulate or construct something to localize at... I know very little about this stuff, but maybe you know more and can figure it out