Some HoTT notes in Arend.

HoTTestArend.ard

\import Logic
\import Paths

\data Circle
  | base
  | loop I \with {
    | left => base
    | right => base
  }

\data Susp (A : \Type)
  | south
  | north
  | merid A (i : I) \elim i {
    | left => north
    | right => south
  }

\func Sphere (_ : Nat) : \Type \lp \oo
  | 0 => Susp Empty
  | suc n => Susp (Sphere n)

\func CircleToSphere1 (x : Circle) : Sphere 1
  | base => north
  | loop i => (path (merid north) *> inv (path (merid south))) @ i

\func Sphere1ToCircle (s : Sphere 1) : Circle
  | south => base
  | north => base
  | merid south i => base
  | merid north i => loop i
  | merid (merid () _) _

\data Torus
  | point
  | line1  I \with { left => point | right => point }
  | line2  I \with { left => point | right => point }
  | face I I \with {
    | left, i  => line2 i
    | right, i => line2 i
    | i, left  => line1 i
    | i, right => line1 i
  }