\import Equiv
\import Paths

{- | The type of squares
     ```
     U --> X
     |     |
     |     |
     V --> Y
     ```
-}
\record Square (U V X Y : \Type)
               (ux : U -> X) (vy : V -> Y) (uv : U -> V) (xy : X -> Y)
               (sqcomm : \Pi (u : U) -> vy (uv u) = xy (ux u))
  \where {
    \func pull (s : Square) {U' : \Type} (f : U' -> s.U) : Square => \new s {
      | U => U'
      | ux u' => s.ux (f u')
      | uv u' => s.uv (f u')
      | sqcomm z => s.sqcomm (f z)
    }

    \func push (s : Square) {Y' : \Type} (f : s.Y -> Y') : Square => \new s {
      | Y => Y'
      | vy v => f (s.vy v)
      | xy x => f (s.xy x)
      | sqcomm u => pmap f (s.sqcomm u)
    }
  }

\open Square(pull,push)

\class Pullback (square : Square)
  | pullback-univ {Z : \Type} : Equiv {Z -> square.U} {Square { | U => Z | V => square.V | X => square.X | Y => square.Y | vy => square.vy | xy => square.xy }} (pull square)

\func sigmaPullback {V X Y : \Type} (vy : V -> Y) (xy : X -> Y) : Pullback \cowith
  | square {
    | U => \Sigma (v : V) (x : X) (p : vy v = xy x)
    | V => V
    | X => X
    | Y => Y
    | ux p => p.
    | vy => vy
    | uv p => p.
    | xy => xy
    | sqcomm p => p.
  }
  | pullback-univ {Z} => \new QEquiv {
    | ret (s : Square) z => (s.uv z, s.ux z, s.sqcomm z)
    | ret_f _ => idp
    | f_sec _ => idp
  }

\func productPullback (A B : \Type) : Pullback \cowith
  | square {
    | U => \Sigma A B
    | V => A
    | X => B
    | Y => \Sigma
    | ux p => p.
    | vy _ => ()
    | uv p => p.
    | xy _ => ()
    | sqcomm _ => idp
  }
  | pullback-univ {Z} => \new QEquiv {
    | ret (s : Square) z => (s.uv z, s.ux z)
    | ret_f _ => idp
    | f_sec _ => idp
  }

\func pathPullback {A : \Type} (x y : A) : Pullback \cowith
  | square {
    | U => x = y
    | V => \Sigma
    | X => \Sigma
    | Y => A
    | ux _ => ()
    | vy _ => x
    | uv _ => ()
    | xy _ => y
    | sqcomm p => p
  }
  | pullback-univ {Z} => \new QEquiv {
    | ret (s : Square) => s.sqcomm
    | ret_f _ => idp
    | f_sec _ => idp
  }