\import Equiv
\import Logic
\import Paths

{- | The type of squares
     ```
     U --> X
     |     |
     |     |
     V --> Y
     ```
-}
\record Square.{u} (U V X Y : \Type u)
                   (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.{u} (s : Square.{u}) {U' : \Type u} (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.{u} (s : Square.{u}) {Y' : \Type u} (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.{u} (square : Square.{u})
  | pullback-univ {Z : \Type u} : IsEquiv {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.{u} {V X Y : \Type u} (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 => inP \new QEquiv {
    | ret (s : Square) z => (s.uv z, s.ux z, s.sqcomm z)
    | ret_f _ => idp
    | f_sec _ => idp
  }

\func productPullback.{u} (A B : \Type u) : 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 => inP \new QEquiv {
    | ret (s : Square) z => (s.uv z, s.ux z)
    | ret_f _ => idp
    | f_sec _ => idp
  }

\func pathPullback.{u} {A : \Type u} (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 => inP \new QEquiv {
    | ret (s : Square) => s.sqcomm
    | ret_f _ => idp
    | f_sec _ => idp
  }