Product

\import Category
\import Equiv (QEquiv, ret)
\import Paths
\import Paths.Meta
\open Precat

\instance ProductPrecat (C D : Precat) : Precat
  | Ob => \Sigma C.Ob D.Ob
  | Hom X Y => \Sigma (C.Hom X.1 Y.1) (D.Hom X.2 Y.2)
  | id X => (id X.1, id X.2)
  | o f g => (f.1 ∘ g.1, f.2 ∘ g.2)
  | id-left => rewrite (id-left, id-left) idp
  | id-right => rewrite (id-right, id-right) idp
  | o-assoc => rewrite (o-assoc, o-assoc) idp
  \where {
    \func iso-first {C D : Precat} {a b : Ob {ProductPrecat C D}}
                    (iso : Iso {ProductPrecat C D} {a} {b}) : Iso {C} {a.1} {b.1} => \new Iso {
      | f => iso.f.1
      | hinv => iso.hinv.1
      | hinv_f => pmap (\lam x => x.1) iso.hinv_f
      | f_hinv => pmap (\lam x => x.1) iso.f_hinv
    }

    \func iso-second {C D : Precat} {a b : Ob {ProductPrecat C D}}
                     (iso : Iso {ProductPrecat C D} {a} {b}) : Iso {D} {a.2} {b.2} => \new Iso {
      | f => iso.f.2
      | hinv => iso.hinv.2
      | hinv_f => pmap (\lam x => x.2) iso.hinv_f
      | f_hinv => pmap (\lam x => x.2) iso.f_hinv
    }
  }

\instance ProductCat (C D : Cat) : Cat
  | Precat => ProductPrecat C D
  | univalence => \new QEquiv {
    | ret iso =>
      exts (ret {univalence} (ProductPrecat.iso-first iso), ret {univalence} (ProductPrecat.iso-second iso))
    | ret_f _ => idp
    | f_sec _ => idp
  } \where {
}