(A B : Type) : Pullback (const_tt A) (const_tt B) <~> A * B. Proof. simple refine (equiv_adjointify _ _ _ _). - intros [a [b _]]; exact (a , b). - intros [a b]; exact (a ; b ; 1). - intros [a b]; exact 1. - intros [a [b p]]; simpl. apply (path_sigma' _ 1); simpl. apply (path_sigma' _ 1); simpl. apply path_contr. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Homotopy.IdentitySystems Cubical.PathSquare. Require Import Diagrams.CommutativeSquares.