{- Set Theory:
   - Injectivity;
   Copyright (c) Groupoid Infinity, 2014-2018.

   HoTT 3.1 Sets and n-types -}

module set where
import proto
import path
import prop
import pi
import sigma
import equiv

-- Contractible is a Prop

setIsProp (A : U) : isProp (isSet A) =
 \(f g : isSet A) -> <i> \(a b :A) ->
   propIsProp (Path A a b) (f a b) (g a b) @ i

setUnit : isSet unit = propSet unit propUnit

setInj (A B : U) (f : A -> B) (sA : isSet A) (sB : isSet B) : U
  = (b : B) -> isProp ((a : A) * Path B (f a) b)

prop_inj (A B: U) (f: A -> B) (sA: isSet A) (sB: isSet B): isProp (setInj A B f sA sB)
  = propPi B Q h where
    P: B -> U = \(b: B) -> (a: A) * Path B (f a) b
    Q: B -> U = \(b: B) -> isProp (P b)
    h: (b: B) -> isProp (Q b) = \(b: B) -> propIsProp (P b)

{-
sqDepPath (A:U) (F:A->U) (sF: (x:A) ->  (F x)) (a0 a1:A) (p: Path A a0 a1) (u0 : F a0) (u1 : F a1)
          (q r : PathP (<i> F (p@i)) u0 u1)
 : Path (PathP (<i> F (p@i)) u0 u1) q r = <i j> rem @ j @ i
 where
  rem : PathP (<i> Path (F (p@i)) (q@i) (r@i)) (<i>u0) (<i>u1)
   = <i> let xi : A = p@i
             ui0 : F xi = transport (<j>F (p @ i/\j)) u0
             ui1 : F xi = transport (<j>F (p @ i\/-j)) u1
             qi : Id (F xi) ui0 ui1 = <j>transport (<k>F (p@(i/\-j/\k)\/(i/\j)\/(j/\-k)\/(i/\k))) (q@j)
             ri : Id (F xi) ui0 ui1 = <j>transport (<k>F (p@(i/\-j/\k)\/(i/\j)\/(j/\-k)\/(i/\k))) (r@j)
    in <j>(sF xi ui0 ui1 qi ri @ j @ i)
-}