hott3.ctt

module hott3 where
import definitions3

-- exercise 3.1
setFromEquiv (A B : U) (set : isSet A) (equiv : Equiv A B) : isSet B =
  transport (<i> isSet (ua A B equiv @ i)) set

-- exercise 3.4
idContrImpliesProp (A : U) (contr : isContr (A -> A)) : isProp A =
  \(x y : A) -> <i>
    (propFromContr (A -> A) contr (\(_ : A) -> x) (\(_ : A) -> y) @ i) x

propImpliesIdContr (A : U) (p : isProp A) : isContr (A -> A) =
  (idfun A, \(f : A -> A) -> <i> \(x : A) -> p x (f x) @ i)

-- weak iff
iff (A B : U) : U = Tuple (A -> B) (B -> A)
-- proof, that this is analogues for not-Prop
iffFromFuncs (A B : Prop) (f : A.1 -> B.1) (g : B.1 -> A.1) : Iff A.1 B.1 =
  ua A.1 B.1 (equivFromBiinvEquiv A.1 B.1 (propBiinvEquiv A B f g))

idContrIffProp (A : U) : iff (isContr (A -> A)) (isProp A) =
  pair (idContrImpliesProp A) (propImpliesIdContr A)

-- exercise 3.6
propImpliesCoproductProp (A : U) (p : isProp A) :
  isProp (Coproduct A (not A)) = split
  inl x -> split@((y : Coproduct A (A -> Empty)) ->
                  Path (Coproduct A (A -> Empty)) (inl x) y) with
    inl y -> <i> inl (p x y @ i)
    inr y -> recEmpty (Path (Coproduct A (A -> Empty)) (inl x) (inr y)) (y x)
  inr x -> split@((y : Coproduct A (A -> Empty)) ->
                  Path (Coproduct A (A -> Empty)) (inr x) y) with
    inl y -> recEmpty (Path (Coproduct A (A -> Empty)) (inr x) (inl y)) (x y)
    inr y -> <i> inr (\(a : A) -> recEmpty (Path Empty (x a) (y a)) (x a) @ i)

-- exercise 3.9
propEquivBool (h : LEM) : BiinvEquiv Prop Bool =
  (lem2,
   pair (lem3, lem4) (lem3, lem5))
  where
    lem1 (A : U) : Coproduct A (not A) -> Bool = split
      inl a -> true
      inr b -> false
    lem2 (p : Prop) : Bool = lem1 p.1 (h p)
    lem3 : Bool -> Prop = split
      false -> (Empty, \(x : Empty) ->
        recEmpty ((y : Empty) -> Path Empty x y) x)
      true -> (Unit, unitIsProp)
    lem4 : (x : Bool) -> Path Bool (lem2 (lem3 x)) x = split
      false -> ?
      true -> ?
    lem5 (p : Prop) : Path Prop (lem3 (lem2 p)) p = ?

-- exercise 3.11
cannotConstructFromTrunc (A : U) : not (trunc A -> A) =
  \(f : trunc A -> A) -> ?