rename conj to conjunction

src/foundation/conjunction.lagda.md

@@ -28,33 +28,33 @@ and `Q` is the proposition that both `P` and `Q` hold.
 ## Definition
 
 ```agda
-conj-Prop = prod-Prop
+conjunction-Prop = prod-Prop
 
 infixr 15 _∧_
-_∧_ = conj-Prop
+_∧_ = conjunction-Prop
 ```
 
 **Note**: The symbol used for the conjunction `_∧_` is the
 [logical and](https://codepoints.net/U+2227) `∧` (agda-input: `\wedge` `\and`).
 
 ```agda
-type-conj-Prop : {l1 l2 : Level} → Prop l1 → Prop l2 → UU (l1 ⊔ l2)
-type-conj-Prop P Q = type-Prop (conj-Prop P Q)
+type-conjunction-Prop : {l1 l2 : Level} → Prop l1 → Prop l2 → UU (l1 ⊔ l2)
+type-conjunction-Prop P Q = type-Prop (conjunction-Prop P Q)
 
 abstract
-  is-prop-type-conj-Prop :
+  is-prop-type-conjunction-Prop :
     {l1 l2 : Level} (P : Prop l1) (Q : Prop l2) →
-    is-prop (type-conj-Prop P Q)
-  is-prop-type-conj-Prop P Q = is-prop-type-Prop (conj-Prop P Q)
+    is-prop (type-conjunction-Prop P Q)
+  is-prop-type-conjunction-Prop P Q = is-prop-type-Prop (conjunction-Prop P Q)
 
-conj-Decidable-Prop :
+conjunction-Decidable-Prop :
   {l1 l2 : Level} → Decidable-Prop l1 → Decidable-Prop l2 →
   Decidable-Prop (l1 ⊔ l2)
-pr1 (conj-Decidable-Prop P Q) =
-  type-conj-Prop (prop-Decidable-Prop P) (prop-Decidable-Prop Q)
-pr1 (pr2 (conj-Decidable-Prop P Q)) =
-  is-prop-type-conj-Prop (prop-Decidable-Prop P) (prop-Decidable-Prop Q)
-pr2 (pr2 (conj-Decidable-Prop P Q)) =
+pr1 (conjunction-Decidable-Prop P Q) =
+  type-conjunction-Prop (prop-Decidable-Prop P) (prop-Decidable-Prop Q)
+pr1 (pr2 (conjunction-Decidable-Prop P Q)) =
+  is-prop-type-conjunction-Prop (prop-Decidable-Prop P) (prop-Decidable-Prop Q)
+pr2 (pr2 (conjunction-Decidable-Prop P Q)) =
   is-decidable-prod
     ( is-decidable-Decidable-Prop P)
     ( is-decidable-Decidable-Prop Q)
@@ -65,31 +65,34 @@ pr2 (pr2 (conj-Decidable-Prop P Q)) =
 ### Introduction rule for conjunction
 
 ```agda
-intro-conj-Prop :
+intro-conjunction-Prop :
   {l1 l2 : Level} (P : Prop l1) (Q : Prop l2) →
-  type-Prop P → type-Prop Q → type-conj-Prop P Q
-pr1 (intro-conj-Prop P Q p q) = p
-pr2 (intro-conj-Prop P Q p q) = q
+  type-Prop P → type-Prop Q → type-conjunction-Prop P Q
+pr1 (intro-conjunction-Prop P Q p q) = p
+pr2 (intro-conjunction-Prop P Q p q) = q
 ```
 
 ### The universal property of conjunction
 
 ```agda
-iff-universal-property-conj-Prop :
+iff-universal-property-conjunction-Prop :
   {l1 l2 : Level} (P : Prop l1) (Q : Prop l2)
   {l3 : Level} (R : Prop l3) →
-  (type-hom-Prop R P × type-hom-Prop R Q) ↔ type-hom-Prop R (conj-Prop P Q)
-pr1 (iff-universal-property-conj-Prop P Q R) (f , g) r = (f r , g r)
-pr1 (pr2 (iff-universal-property-conj-Prop P Q R) h) r = pr1 (h r)
-pr2 (pr2 (iff-universal-property-conj-Prop P Q R) h) r = pr2 (h r)
-
-equiv-universal-property-conj-Prop :
+  ( type-hom-Prop R P × type-hom-Prop R Q) ↔
+  ( type-hom-Prop R (conjunction-Prop P Q))
+pr1 (pr1 (iff-universal-property-conjunction-Prop P Q R) (f , g) r) = f r
+pr2 (pr1 (iff-universal-property-conjunction-Prop P Q R) (f , g) r) = g r
+pr1 (pr2 (iff-universal-property-conjunction-Prop P Q R) h) r = pr1 (h r)
+pr2 (pr2 (iff-universal-property-conjunction-Prop P Q R) h) r = pr2 (h r)
+
+equiv-universal-property-conjunction-Prop :
   {l1 l2 : Level} (P : Prop l1) (Q : Prop l2)
   {l3 : Level} (R : Prop l3) →
-  (type-hom-Prop R P × type-hom-Prop R Q) ≃ type-hom-Prop R (conj-Prop P Q)
-equiv-universal-property-conj-Prop P Q R =
+  ( type-hom-Prop R P × type-hom-Prop R Q) ≃
+  ( type-hom-Prop R (conjunction-Prop P Q))
+equiv-universal-property-conjunction-Prop P Q R =
   equiv-iff'
-    ( conj-Prop (hom-Prop R P) (hom-Prop R Q))
-    ( hom-Prop R (conj-Prop P Q))
-    ( iff-universal-property-conj-Prop P Q R)
+    ( conjunction-Prop (hom-Prop R P) (hom-Prop R Q))
+    ( hom-Prop R (conjunction-Prop P Q))
+    ( iff-universal-property-conjunction-Prop P Q R)
 ```

src/foundation/disjunction.lagda.md

@@ -91,14 +91,14 @@ ev-disjunction-Prop :
   {l1 l2 l3 : Level} (P : Prop l1) (Q : Prop l2) (R : Prop l3) →
   type-hom-Prop
     ( hom-Prop (disjunction-Prop P Q) R)
-    ( conj-Prop (hom-Prop P R) (hom-Prop Q R))
+    ( conjunction-Prop (hom-Prop P R) (hom-Prop Q R))
 pr1 (ev-disjunction-Prop P Q R h) = h ∘ (inl-disjunction-Prop P Q)
 pr2 (ev-disjunction-Prop P Q R h) = h ∘ (inr-disjunction-Prop P Q)
 
 elim-disjunction-Prop :
   {l1 l2 l3 : Level} (P : Prop l1) (Q : Prop l2) (R : Prop l3) →
   type-hom-Prop
-    ( conj-Prop (hom-Prop P R) (hom-Prop Q R))
+    ( conjunction-Prop (hom-Prop P R) (hom-Prop Q R))
     ( hom-Prop (disjunction-Prop P Q) R)
 elim-disjunction-Prop P Q R (pair f g) =
   map-universal-property-trunc-Prop R (ind-coprod (λ t → type-Prop R) f g)
@@ -110,7 +110,7 @@ abstract
   is-equiv-ev-disjunction-Prop P Q R =
     is-equiv-is-prop
       ( is-prop-type-Prop (hom-Prop (disjunction-Prop P Q) R))
-      ( is-prop-type-Prop (conj-Prop (hom-Prop P R) (hom-Prop Q R)))
+      ( is-prop-type-Prop (conjunction-Prop (hom-Prop P R) (hom-Prop Q R)))
       ( elim-disjunction-Prop P Q R)
 ```
 

src/foundation/exclusive-disjunction.lagda.md

@@ -71,8 +71,8 @@ module _
   xor-Prop : Prop (l1 ⊔ l2)
   xor-Prop =
     coprod-Prop
-      ( conj-Prop P (neg-Prop Q))
-      ( conj-Prop Q (neg-Prop P))
+      ( conjunction-Prop P (neg-Prop Q))
+      ( conjunction-Prop Q (neg-Prop P))
       ( λ p q → pr2 q (pr1 p))
 
   type-xor-Prop : UU (l1 ⊔ l2)
@@ -252,7 +252,7 @@ module _
 {-
   eq-equiv-Prop
     ( ( ( equiv-coprod
-          ( ( ( left-unit-law-coprod (type-Prop (conj-Prop P (neg-Prop Q)))) ∘e
+          ( ( ( left-unit-law-coprod (type-Prop (conjunction-Prop P (neg-Prop Q)))) ∘e
               ( equiv-coprod
                 ( left-absorption-Σ
                   ( λ x →

src/foundation/existential-quantification.lagda.md

@@ -119,24 +119,26 @@ module _
   {l1 l2 l3 : Level} (P : Prop l1) {A : UU l2} (Q : A → Prop l3)
   where
 
-  iff-distributive-conj-exists-Prop :
-    (conj-Prop P (exists-Prop A Q)) ⇔ (exists-Prop A (λ a → conj-Prop P (Q a)))
-  pr1 iff-distributive-conj-exists-Prop (p , e) =
+  iff-distributive-conjunction-exists-Prop :
+    ( conjunction-Prop P (exists-Prop A Q)) ⇔
+    ( exists-Prop A (λ a → conjunction-Prop P (Q a)))
+  pr1 iff-distributive-conjunction-exists-Prop (p , e) =
     elim-exists-Prop Q
-      ( exists-Prop A (λ a → conj-Prop P (Q a)))
+      ( exists-Prop A (λ a → conjunction-Prop P (Q a)))
       ( λ x q → intro-∃ x (p , q))
       ( e)
-  pr2 iff-distributive-conj-exists-Prop =
+  pr2 iff-distributive-conjunction-exists-Prop =
     elim-exists-Prop
-      ( λ x → conj-Prop P (Q x))
-      ( conj-Prop P (exists-Prop A Q))
+      ( λ x → conjunction-Prop P (Q x))
+      ( conjunction-Prop P (exists-Prop A Q))
       ( λ x (p , q) → (p , intro-∃ x q))
 
-  distributive-conj-exists-Prop :
-    conj-Prop P (exists-Prop A Q) ＝ exists-Prop A (λ a → conj-Prop P (Q a))
-  distributive-conj-exists-Prop =
+  distributive-conjunction-exists-Prop :
+    conjunction-Prop P (exists-Prop A Q) ＝
+    exists-Prop A (λ a → conjunction-Prop P (Q a))
+  distributive-conjunction-exists-Prop =
     eq-iff'
-      ( conj-Prop P (exists-Prop A Q))
-      ( exists-Prop A (λ a → conj-Prop P (Q a)))
-      ( iff-distributive-conj-exists-Prop)
+      ( conjunction-Prop P (exists-Prop A Q))
+      ( exists-Prop A (λ a → conjunction-Prop P (Q a)))
+      ( iff-distributive-conjunction-exists-Prop)
 ```

src/foundation/impredicative-encodings.lagda.md

@@ -76,39 +76,39 @@ equiv-impredicative-trunc-Prop A =
 ### The impredicative encoding of conjunction
 
 ```agda
-impredicative-conj-Prop :
+impredicative-conjunction-Prop :
   {l1 l2 : Level} → Prop l1 → Prop l2 → Prop (lsuc (l1 ⊔ l2))
-impredicative-conj-Prop {l1} {l2} P1 P2 =
+impredicative-conjunction-Prop {l1} {l2} P1 P2 =
   Π-Prop
     ( Prop (l1 ⊔ l2))
     ( λ Q → function-Prop (type-Prop P1 → (type-Prop P2 → type-Prop Q)) Q)
 
-type-impredicative-conj-Prop :
+type-impredicative-conjunction-Prop :
   {l1 l2 : Level} → Prop l1 → Prop l2 → UU (lsuc (l1 ⊔ l2))
-type-impredicative-conj-Prop P1 P2 =
-  type-Prop (impredicative-conj-Prop P1 P2)
+type-impredicative-conjunction-Prop P1 P2 =
+  type-Prop (impredicative-conjunction-Prop P1 P2)
 
-map-impredicative-conj-Prop :
+map-impredicative-conjunction-Prop :
   {l1 l2 : Level} (P1 : Prop l1) (P2 : Prop l2) →
-  type-conj-Prop P1 P2 → type-impredicative-conj-Prop P1 P2
-map-impredicative-conj-Prop {l1} {l2} P1 P2 (pair p1 p2) Q f =
+  type-conjunction-Prop P1 P2 → type-impredicative-conjunction-Prop P1 P2
+map-impredicative-conjunction-Prop {l1} {l2} P1 P2 (pair p1 p2) Q f =
   f p1 p2
 
-inv-map-impredicative-conj-Prop :
+inv-map-impredicative-conjunction-Prop :
   {l1 l2 : Level} (P1 : Prop l1) (P2 : Prop l2) →
-  type-impredicative-conj-Prop P1 P2 → type-conj-Prop P1 P2
-inv-map-impredicative-conj-Prop P1 P2 H =
-  H (conj-Prop P1 P2) (λ p1 p2 → pair p1 p2)
+  type-impredicative-conjunction-Prop P1 P2 → type-conjunction-Prop P1 P2
+inv-map-impredicative-conjunction-Prop P1 P2 H =
+  H (conjunction-Prop P1 P2) (λ p1 p2 → pair p1 p2)
 
-equiv-impredicative-conj-Prop :
+equiv-impredicative-conjunction-Prop :
   {l1 l2 : Level} (P1 : Prop l1) (P2 : Prop l2) →
-  type-conj-Prop P1 P2 ≃ type-impredicative-conj-Prop P1 P2
-equiv-impredicative-conj-Prop P1 P2 =
+  type-conjunction-Prop P1 P2 ≃ type-impredicative-conjunction-Prop P1 P2
+equiv-impredicative-conjunction-Prop P1 P2 =
   equiv-iff
-    ( conj-Prop P1 P2)
-    ( impredicative-conj-Prop P1 P2)
-    ( map-impredicative-conj-Prop P1 P2)
-    ( inv-map-impredicative-conj-Prop P1 P2)
+    ( conjunction-Prop P1 P2)
+    ( impredicative-conjunction-Prop P1 P2)
+    ( map-impredicative-conjunction-Prop P1 P2)
+    ( inv-map-impredicative-conjunction-Prop P1 P2)
 ```
 
 ### The impredicative encoding of disjunction

src/foundation/intersections-subtypes.lagda.md

@@ -70,7 +70,7 @@ module _
   intersection-decidable-subtype :
     decidable-subtype l1 X → decidable-subtype l2 X →
     decidable-subtype (l1 ⊔ l2) X
-  intersection-decidable-subtype P Q x = conj-Decidable-Prop (P x) (Q x)
+  intersection-decidable-subtype P Q x = conjunction-Decidable-Prop (P x) (Q x)
 ```
 
 ### The intersection of a family of subtypes

src/foundation/large-locale-of-propositions.lagda.md

@@ -58,10 +58,10 @@ antisymmetric-leq-Large-Poset Prop-Large-Poset P Q = eq-iff
 ```agda
 has-meets-Prop-Large-Locale :
   has-meets-Large-Poset Prop-Large-Poset
-meet-has-meets-Large-Poset has-meets-Prop-Large-Locale = conj-Prop
+meet-has-meets-Large-Poset has-meets-Prop-Large-Locale = conjunction-Prop
 is-greatest-binary-lower-bound-meet-has-meets-Large-Poset
   has-meets-Prop-Large-Locale =
-  iff-universal-property-conj-Prop
+  iff-universal-property-conjunction-Prop
 ```
 
 ### The largest element in the large poset of propositions
@@ -113,7 +113,7 @@ is-large-meet-semilattice-Large-Frame Prop-Large-Frame =
 is-large-suplattice-Large-Frame Prop-Large-Frame =
   is-large-suplattice-Prop-Large-Locale
 distributive-meet-sup-Large-Frame Prop-Large-Frame =
-  distributive-conj-exists-Prop
+  distributive-conjunction-exists-Prop
 ```
 
 ### The large locale of propositions

src/orthogonal-factorization-systems/factorizations-of-maps-function-classes.lagda.md

@@ -65,7 +65,9 @@ module _
 
   is-function-class-factorization-Prop : Prop (lL ⊔ lR)
   is-function-class-factorization-Prop =
-    conj-Prop (L (left-map-factorization F)) (R (right-map-factorization F))
+    conjunction-Prop
+      ( L (left-map-factorization F))
+      ( R (right-map-factorization F))
 
   is-function-class-factorization : UU (lL ⊔ lR)
   is-function-class-factorization =