From 0434f46f3493c557cd5bebb8112de97e8b5098a4 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Wed, 22 Mar 2023 00:33:58 -0500 Subject: [PATCH] z --- src/Path2.lagda.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Path2.lagda.md b/src/Path2.lagda.md index efdeb81..108d508 100644 --- a/src/Path2.lagda.md +++ b/src/Path2.lagda.md @@ -3,6 +3,7 @@ Path2
Basics (Path, transport, ap, etc.) + ``` {-# OPTIONS --without-K --rewriting #-} @@ -72,8 +73,12 @@ apd {A} {B} f p = path-ind D d p d : (x : A) → D x x (refl x) d x = refl (f x) ``` +
+Path products +--- + ``` -- Path products pr₁ : {A B : Type} {a₁ a₂ : A} {b₁ b₂ : B}