{- 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)