definitions6.ctt

module definitions6 where
import hott5

data S1 =
    base
  | loop <i> [ (i = 0) -> base, (i = 1) -> base ]
loopS1 : Path S1 base base = <i> loop{S1} @ i

data I =
    left
  | right
  | seg <i> [ (i = 0) -> left, (i = 1) -> right ]

recI (B : U) (b0 : B) (b1 : B) (s : Path B b0 b1) : I -> B = split
  left -> b0
  right -> b1
  seg @ i -> s @ i

funextFromI (A B : U) (f g : A -> B) (p : (x : A) -> Path B (f x) (g x)) :
  Path (A -> B) f g = <i> q (seg{I} @ i)
  where
    path (x : A) : I -> B = split
      left -> f x
      right -> g x
      seg @ i -> p x @ i
    q (i : I) : A -> B = \(x : A) -> path x i

circleIsNotTrivial : not (Path (Path S1 base base) loopS1 (refl S1 base)) =
  \(h : Path (Path S1 base base) loopS1 (refl S1 base)) ->
    universeNotSet
      (\(A B : U) (p q : Path U A B) ->
        indPath U
          (\(A B : U) (p : Path U A B) ->
            (q : Path U A B) -> Path (Path U A B) p q)
          (\(A : U) (p : Path U A A) ->
            <i> onlyRefl U A p h @ -i)
          A B p q)
  where
    f (A : U) (x : A) (p : Path A x x) : S1 -> A = split
      base -> x
      loop @ i -> p @ i
    onlyRefl (A : U) (x : A) (p : Path A x x)
             (h : Path (Path S1 base base) loopS1 (refl S1 base)) :
             Path (Path A x x) p (refl A x) =
      <i j> f A x p (h @ i @ j)

data Suspension (A : U) =
    north
  | south
  | merid (a : A) <i>
          [ (i = 0) -> north, (i = 1) -> south ]

SN : N -> U = split
  zero -> Bool
  succ n -> Suspension (SN n)

SuspensionOfEmptyEquivBool : BiinvEquiv (Suspension Empty) Bool =
  (f, pair (g, lem1) (g, lem2))
  where
    f : Suspension Empty -> Bool = split
      north -> false
      south -> true
      merid e @ i -> recEmpty (Path Bool false true) e @ i
    g : Bool -> Suspension Empty = split
      false -> north
      true -> south
    lem1 : (x : Bool) -> Path Bool (f (g x)) x = split
      false -> refl Bool false
      true -> refl Bool true
    lem2 : (x : Suspension Empty) -> Path (Suspension Empty) (g (f x)) x = ?

data Pushout (A B C : U) (f : C -> A) (g : C -> B) =
    inl (a : A)
  | inr (b : B)
  | gluePushout (c : C) <i>
                [ (i = 0) -> inl (f c),
                  (i = 1) -> inr (g c) ]

isEquivRel (A : U) (R : A -> A -> U) : U =
  (refl : (a : A) -> R a a) *
  (symm : (a b : A) -> R a b -> R b a) *
  ((a b c : A) -> Tuple (R a b) (R b c) -> R a c)