Univalence in Formality

Univalence.fm

// based on https://arxiv.org/pdf/1803.02294.pdf

import Relation.Equality

K : { X : Type} -> Type
  {x : X, y : X, p : Path(X,x,y), q : Path(X,x,y)} -> Path(Path(X,x,y),p,q)

J :
  { X : Type
  , x : X
  , y : X
  , A : {X : Type, x : X, y : X, p : Path(X,x,y)} -> Type
  , f : {x : X} -> A(X,x,x,reflect(~X,~x))
  , p : Path(X,x,y)
  } -> A(X,x,y,p)
  (%p)(~A(X,x),f(x))

SingletonType : {X : Type, x : X} -> Type
  [y : X, Path(X,y,x)]

eta : {X : Type, x : X} -> SingletonType(X,x)
  [x, reflect(~X,~x)]

A : {X : Type, y : X, x : X, p : Path(X,y,x)} -> Type
  Path(SingletonType(X,x),eta(X,x),[y, p])

f : {X : Type, x : X} -> A(X,x,x,reflect(~X,~x))
  reflect(~SingletonType(X,x),~eta(X,x))

phi : { X : Type, y : X , x : X , p : Path(X,y,x) }
      -> Path(SingletonType(X,x), eta(X,x), [y, p])
  J(X,y,x,A,f(type(X)),p)


// This requires a proof that `[y,p] == s`, which currently seems
// not possible with the current `get` primitive. Here is a proposed change which would allow this.
//
//g : {X : Type, x : X, s : SingletonType(X,x)}
//    -> Path(SingletonType(X,x),eta(X,x),s)
//   get e : [y,p] is s
//   phi(X,y,x,p) :: rewrite t in Path(SingletonType(X,x), eta(X,x), t) with e
//
//split_join : {A : Type, B : Type, a : [A,B]} -> [fst(a), snd(a)] == a
//  get [l,r] = a with e
//  refl(~a) :: rewrite t in t == a with sym(~e)

h : { X : Type
    , x : X
    } -> let SX = SingletonType(X,x); [c : SX, {s : SX} -> Path(SX, c, s)]
    [eta(X,x), ?g]

IsSingleton : {X : Type} -> Type
  [c : X, {x : X} -> Path(X,c,x)]

SingletonTypeIsSingleton :
  { X : Type
  , x : X
  } -> IsSingleton(SingletonType(X,x))
  [eta(X,x), ?g]

Fiber : {X : Type, Y : Type, f : X -> Y, y : Y} -> Type
  [x : X, Path(Y, f(x), y)]

IsEquiv : {X : Type, Y : Type, f : X -> Y} -> Type
  {y : Y} -> IsSingleton(Fiber(X,Y,f,y))

Equiv : {X : Type, Y : Type} -> Type
  [f : X -> Y, IsEquiv(X,Y,f)]

id : {X : Type, x : X} -> X; x

idIsEquiv : {X : Type} -> IsEquiv(X,X,id(X))
  {y} SingletonTypeIsSingleton(X,y)

IdToEq : {X : Type, Y : Type, p : Path(Type,X,Y)} -> Eq(Type,X,Y)
  Path_to_Eq(~Type, ~X,~Y,p)

isUnivalent : Type
  {X : Type, Y : Type} -> IsEquiv(Path(Type,X,Y),Eq(Type,X,Y),IdToEq(X,Y))