work

UniMath · fredrik-bakke · Sep 24, 2024 · Sep 24, 2024 · Sep 28, 2024 · Oct 9, 2024
commit c12c18d04c43956068c0d41dc0d805141cf74c04
diff --git a/src/foundation/action-on-identifications-binary-dependent-functions.lagda.md b/src/foundation/action-on-identifications-binary-dependent-functions.lagda.md
@@ -8,7  8,7 @@ module foundation.action-on-identifications-binary-dependent-functions where
 
 ```agda
 open import foundation.action-on-identifications-dependent-functions
-open import foundation.doubly-dependent-identifications
 open import foundation.binary-dependent-identifications
 open import foundation.universe-levels
 
 open import foundation-core.identity-types
@@ -20,10  20,11 @@ open import foundation-core.identity-types
 
 Given a binary dependent function `f : (x : A) (y : B) → C x y` and
 [identifications](foundation-core.identity-types.md) `p : x ＝ x'` in `A` and
-`q : y ＝ y'` in `B`, we obtain a [doubly dependent identification](foundation.doubly-dependent-identifications.md)
 `q : y ＝ y'` in `B`, we obtain a
 [binary dependent identification](foundation.binary-dependent-identifications.md)
 
 ```text
-  apd-binary f p q : doubly-dependent-identification p q (f x y) (f x' y')
   apd-binary f p q : binary-dependent-identification p q (f x y) (f x' y')
 ```
 
 we call this the
@@ -41,8  42,8 @@ module _
 
   apd-binary :
     {x x' : A} (p : x ＝ x') {y y' : B} (q : y ＝ y') →
-    doubly-dependent-identification C p q (f x y) (f x' y')
-  apd-binary refl q = apd (f _) q
     binary-dependent-identification C p q (f x y) (f x' y')
   apd-binary refl refl = refl
 ```
 
 ## See also

diff --git a/src/foundation/binary-dependent-identifications.lagda.md b/src/foundation/binary-dependent-identifications.lagda.md
@@ -0,0  1,43 @@
 # Binary dependent identifications
 
 ```agda
 module foundation.binary-dependent-identifications where
 ```
 
 <details><summary>Imports</summary>
 
 ```agda
 open import foundation.binary-transport
 open import foundation.identity-types
 open import foundation.universe-levels
 ```
 
 </details>
 
 ## Idea
 
 Consider a family of types `C x y` indexed by `x : A` and `y : B`, and consider
 [identifications](foundation-core.identity-types.md) `p : x ＝ x'` and
 `q : y ＝ y'` in `A` and `B`, respectively. A
 {{#concept "binary dependent identification" Agda=binary-dependent-identification}}
 from `c : C x y` to `c' : C x' y'` over `p` and `q` is a
 [dependent identification](foundation.dependent-identifications.md)
 
 ```text
   r : dependent-identification (C x') p (tr (λ t → C t y) p c) c'.
 ```
 
 ## Definitions
 
 ### Doubly dependent identifications
 
 ```agda
 module _
   {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (C : A → B → UU l3)
   where
 
   binary-dependent-identification :
     {x x' : A} (p : x ＝ x') {y y' : B} (q : y ＝ y') →
     C x y → C x' y' → UU l3
   binary-dependent-identification p q c c' = binary-tr C p q c ＝ c'
 ```
diff --git a/src/foundation/binary-transport.lagda.md b/src/foundation/binary-transport.lagda.md
@@ -37,7  37,7 @@ module _
   where
 
   binary-tr : (p : x ＝ x') (q : y ＝ y') → C x y → C x' y'
-  binary-tr refl refl = id
   binary-tr p q c = tr (C _) q (tr (λ u → C u _) p c)
 
   is-equiv-binary-tr : (p : x ＝ x') (q : y ＝ y') → is-equiv (binary-tr p q)
   is-equiv-binary-tr refl refl = is-equiv-id

diff --git a/src/foundation/dependent-identifications.lagda.md b/src/foundation/dependent-identifications.lagda.md
@@ -305,4  305,4 @@ module _
 
 ## See also
 
-- [Doubly dependent identifications](foundation.doubly-dependent-identifications.md)
 - [Doubly dependent identifications](foundation.binary-dependent-identifications.md)
diff --git a/src/foundation/doubly-dependent-identifications.lagda.md b/src/foundation/doubly-dependent-identifications.lagda.md
diff --git a/src/foundation/reflexive-relations.lagda.md b/src/foundation/reflexive-relations.lagda.md
@@ -9,7  9,7 @@ module foundation.reflexive-relations where
 ```agda
 open import foundation.binary-relations
 open import foundation.dependent-pair-types
-open import foundation.doubly-dependent-identifications
 open import foundation.binary-dependent-identifications
 open import foundation.universe-levels
 
 open import foundation-core.identity-types
@@ -54,32  54,44 @@ Id-Reflexive-Relation A = (Id , (λ x → refl))
 
 ### A formulation of the dependent action on identifications of reflexivity
 
-Consider a reflexive relation `R` on a type `A` with reflexivity `r : (x : A) → R x x`, and consider an [identification](foundation-core.identity-types.md) `p : x ＝ y` in `A`. The usual [action on identifications](foundation.action-on-identifications-dependent-functions.md) yields a [dependent identification](foundation.dependent-identifications.md)
 Consider a reflexive relation `R` on a type `A` with reflexivity
 `r : (x : A) → R x x`, and consider an
 [identification](foundation-core.identity-types.md) `p : x ＝ y` in `A`. The
 usual
 [action on identifications](foundation.action-on-identifications-dependent-functions.md)
 yields a [dependent identification](foundation.dependent-identifications.md)
 
 ```text
   tr (λ u → R u u) p (r x) ＝ (r y).
 ```
 
-However, since `R` is a binary indexed family of types, there is also the [doubly dependent identity type](foundation.doubly-dependent-identifications.md), which can be used to express another version of the action on identifications of the reflexivity element `r`:
 However, since `R` is a binary indexed family of types, there is also the
 [binary dependent identity type](foundation.binary-dependent-identifications.md),
 which can be used to express another version of the action on identifications of
 the reflexivity element `r`:
 
 ```text
-  doubly-dependent-identification R p p (r x) (r y).
   binary-dependent-identification R p p (r x) (r y).
 ```
 
-This action on identifications can be seen as an instance of a dependent function over the diagonal map `Δ : A → A × A`, a situation wich can be generalized. At the present time, however, the library lacks infrastructure for the general formulation of the action on identifications of dependent functions over functions yielding doubly dependent identifications.
 This action on identifications can be seen as an instance of a dependent
 function over the diagonal map `Δ : A → A × A`, a situation wich can be
 generalized. At the present time, however, the library lacks infrastructure for
 the general formulation of the action on identifications of dependent functions
 over functions yielding binary dependent identifications.
 
 ```agda
 module _
   {l1 l2 : Level} {A : UU l1} (R : Reflexive-Relation l2 A)
   where
 
-  doubly-dependent-identification-refl-Reflexive-Relation :
   binary-dependent-identification-refl-Reflexive-Relation :
     {x y : A} (p : x ＝ y) →
-    doubly-dependent-identification
     binary-dependent-identification
       ( rel-Reflexive-Relation R)
       ( p)
       ( p)
       ( refl-Reflexive-Relation R x)
       ( refl-Reflexive-Relation R y)
-  doubly-dependent-identification-refl-Reflexive-Relation refl = refl
   binary-dependent-identification-refl-Reflexive-Relation refl = refl
 ```
diff --git a/src/graph-theory/morphisms-directed-graphs.lagda.md b/src/graph-theory/morphisms-directed-graphs.lagda.md
@@ -85,7  85,7 @@ module _
         ( λ y → edge-hom-Directed-Graph)
 ```
 
-### Composition of morphisms graphs
 ### Composition of morphisms of directed graphs
 
 ```agda
 module _
@@ -117,7  117,7 @@ module _
   pr2 (comp-hom-Directed-Graph g f) = edge-comp-hom-Directed-Graph g f
 ```
 
-### Identity morphisms graphs
 ### Identity morphisms of directed graphs
 
 ```agda
 module _

diff --git a/src/graph-theory/morphisms-reflexive-graphs.lagda.md b/src/graph-theory/morphisms-reflexive-graphs.lagda.md
@@ -7,6  7,7 @@ module graph-theory.morphisms-reflexive-graphs where
 <details><summary>Imports</summary>
 
 ```agda
 open import foundation.action-on-identifications-binary-dependent-functions
 open import foundation.action-on-identifications-functions
 open import foundation.binary-transport
 open import foundation.commuting-squares-of-identifications
@@ -99,7  100,7 @@ module _
     refl-hom-Reflexive-Graph = pr2 f
 ```
 
-### Composition of morphisms graphs
 ### Composition of morphisms of reflexive graphs
 
 ```agda
 module _
@@ -146,7  147,7 @@ module _
   pr2 comp-hom-Reflexive-Graph = refl-comp-hom-Reflexive-Graph
 ```
 
-### Identity morphisms graphs
 ### Identity morphisms of reflexive graphs
 
 ```agda
 module _
@@ -157,3  158,101 @@ module _
   pr1 id-hom-Reflexive-Graph = id-hom-Directed-Graph _
   pr2 id-hom-Reflexive-Graph _ = refl
 ```
 
 ### Homotopies of morphisms of reflexive graphs
 
 ```agda
 module _
   {l1 l2 l3 l4 : Level} (G : Reflexive-Graph l1 l2) (H : Reflexive-Graph l3 l4)
   (f g : hom-Reflexive-Graph G H)
   where
 
   htpy-hom-Reflexive-Graph : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
   htpy-hom-Reflexive-Graph =
     Σ ( htpy-hom-Directed-Graph
         ( directed-graph-Reflexive-Graph G)
         ( directed-graph-Reflexive-Graph H)
         ( hom-directed-graph-hom-Reflexive-Graph G H f)
         ( hom-directed-graph-hom-Reflexive-Graph G H g))
       ( λ (h₀ , h₁) →
         (x : vertex-Reflexive-Graph G) →
         coherence-square-identifications
           ( ap
             ( binary-tr (edge-Reflexive-Graph H) (h₀ x) (h₀ x))
             ( refl-hom-Reflexive-Graph G H f x))
           ( h₁ x x (refl-Reflexive-Graph G x))
           ( binary-dependent-identification-refl-Reflexive-Graph H (h₀ x))
           ( refl-hom-Reflexive-Graph G H g x))
 ```
 
 ### The reflexive homotopy of morphisms of reflexive graphs
 
 ```agda
 module _
   {l1 l2 l3 l4 : Level} (G : Reflexive-Graph l1 l2) (H : Reflexive-Graph l3 l4)
   (f : hom-Reflexive-Graph G H)
   where
 
   refl-htpy-hom-Reflexive-Graph : htpy-hom-Reflexive-Graph G H f f
   pr1 refl-htpy-hom-Reflexive-Graph =
     refl-htpy-hom-Directed-Graph
       ( directed-graph-Reflexive-Graph G)
       ( directed-graph-Reflexive-Graph H)
       ( hom-directed-graph-hom-Reflexive-Graph G H f)
   pr2 refl-htpy-hom-Reflexive-Graph x =
     inv (right-unit ∙ ap-id _)
 ```
 
 ## Properties
 
 ### Extensionality of morphisms of reflexive graphs
 
 ```agda
 module _
   {l1 l2 l3 l4 : Level} (G : Reflexive-Graph l1 l2) (H : Reflexive-Graph l3 l4)
   (f : hom-Reflexive-Graph G H)
   where
 
   is-torsorial-htpy-hom-Reflexive-Graph :
     is-torsorial (htpy-hom-Reflexive-Graph G H f)
   is-torsorial-htpy-hom-Reflexive-Graph =
     is-torsorial-Eq-structure
       ( is-torsorial-htpy-hom-Directed-Graph
         ( directed-graph-Reflexive-Graph G)
         ( directed-graph-Reflexive-Graph H)
         ( hom-directed-graph-hom-Reflexive-Graph G H f))
       ( hom-directed-graph-hom-Reflexive-Graph G H f ,
         refl-htpy-hom-Directed-Graph
           ( directed-graph-Reflexive-Graph G)
           ( directed-graph-Reflexive-Graph H)
           ( hom-directed-graph-hom-Reflexive-Graph G H f))
       ( is-torsorial-htpy' _)
 
   htpy-eq-hom-Reflexive-Graph :
     (g : hom-Reflexive-Graph G H) →
     f ＝ g → htpy-hom-Reflexive-Graph G H f g
   htpy-eq-hom-Reflexive-Graph g refl =
     refl-htpy-hom-Reflexive-Graph G H f
 
   is-equiv-htpy-eq-hom-Reflexive-Graph :
     (g : hom-Reflexive-Graph G H) →
     is-equiv (htpy-eq-hom-Reflexive-Graph g)
   is-equiv-htpy-eq-hom-Reflexive-Graph =
     fundamental-theorem-id
       is-torsorial-htpy-hom-Reflexive-Graph
       htpy-eq-hom-Reflexive-Graph
 
   extensionality-hom-Reflexive-Graph :
     (g : hom-Reflexive-Graph G H) →
     (f ＝ g) ≃ htpy-hom-Reflexive-Graph G H f g
   pr1 (extensionality-hom-Reflexive-Graph g) =
     htpy-eq-hom-Reflexive-Graph g
   pr2 (extensionality-hom-Reflexive-Graph g) =
     is-equiv-htpy-eq-hom-Reflexive-Graph g
 
   eq-htpy-hom-Reflexive-Graph :
     (g : hom-Reflexive-Graph G H) →
     htpy-hom-Reflexive-Graph G H f g → f ＝ g
   eq-htpy-hom-Reflexive-Graph g =
     map-inv-equiv (extensionality-hom-Reflexive-Graph g)
 ```
diff --git a/src/graph-theory/reflexive-graphs.lagda.md b/src/graph-theory/reflexive-graphs.lagda.md
@@ -8,7  8,7 @@ module graph-theory.reflexive-graphs where
 
 ```agda
 open import foundation.dependent-pair-types
-open import foundation.doubly-dependent-identifications
 open import foundation.binary-dependent-identifications
 open import foundation.identity-types
 open import foundation.reflexive-relations
 open import foundation.universe-levels
@@ -53,13  53,13 @@ module _
   pr1 reflexive-relation-Reflexive-Graph = edge-Reflexive-Graph
   pr2 reflexive-relation-Reflexive-Graph = refl-Reflexive-Graph
 
-  doubly-dependent-identification-refl-Reflexive-Graph :
   binary-dependent-identification-refl-Reflexive-Graph :
     {x y : vertex-Reflexive-Graph} (p : x ＝ y) →
-    doubly-dependent-identification edge-Reflexive-Graph p p
     binary-dependent-identification edge-Reflexive-Graph p p
       ( refl-Reflexive-Graph x)
       ( refl-Reflexive-Graph y)
-  doubly-dependent-identification-refl-Reflexive-Graph =
-    doubly-dependent-identification-refl-Reflexive-Relation
   binary-dependent-identification-refl-Reflexive-Graph =
     binary-dependent-identification-refl-Reflexive-Relation
       reflexive-relation-Reflexive-Graph
 ```
 

diff --git a/src/graph-theory/sections-dependent-reflexive-graphs.lagda.md b/src/graph-theory/sections-dependent-reflexive-graphs.lagda.md
@@ -34,8  34,9 @@ open import graph-theory.sections-dependent-directed-graphs
 
 ## Idea
 
-Consider a [dependent reflexive graph](graph-theory.dependent-reflexive-graphs.md)
-`B` over a [reflexive graph](graph-theory.reflexive-graphs.md) `A`. A
 Consider a
 [dependent reflexive graph](graph-theory.dependent-reflexive-graphs.md) `B` over
 a [reflexive graph](graph-theory.reflexive-graphs.md) `A`. A
 {{#concept "section" Disambiguation="dependent reflexive graph" Agda=section-Dependent-Reflexive-Graph}}
 `f` of `B` consists of
 
@@ -185,7  186,7 @@ module _
                 ( H₀ x)))
             ( refl-section-Dependent-Reflexive-Graph B f x))
           ( H₁ (refl-Reflexive-Graph A x))
-          ( doubly-dependent-identification-refl-Reflexive-Relation
           ( binary-dependent-identification-refl-Reflexive-Relation
             ( edge-Dependent-Reflexive-Graph B (refl-Reflexive-Graph A x) ,
               refl-Dependent-Reflexive-Graph B)
             ( H₀ x))
Original file line number	Diff line number	Diff line change
Expand Up		@@ -305,4 305,4 @@ module _

		## See also

		- [Doubly dependent identifications](foundation.doubly-dependent-identifications.md)
		- [Doubly dependent identifications](foundation.binary-dependent-identifications.md)