Sigma bases

src/1Lab/Function/Embedding.lagda.md

@@ -211,7 +211,7 @@ module _ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {f : A → B} where
     .is-iso.linv → J (λ y p → ap fst (emb (f y) (x , ap f p) (y , refl)) ≡ p)
       (ap-square fst (is-prop→is-set (emb (f x)) _ _ (emb (f x) (x , refl) (x , refl)) refl))
 
-  equiv→cancellable : is-equiv f → ∀ {x y} → is-equiv {B = f x ≡ f y} (ap f)
+  equiv→cancellable : ∀ {x y} → is-equiv f → is-equiv {B = f x ≡ f y} (ap f)
   equiv→cancellable eqv = embedding→cancellable (is-equiv→is-embedding eqv)
 ```
 

src/1Lab/HLevel/Closure.lagda.md

@@ -282,6 +282,25 @@ non-dependent sum is a product.
 ×-is-hlevel n ahl bhl = Σ-is-hlevel n ahl (λ _ → bhl)
 ```
 
+We can also give a more refined characterisation of contractibility
+of $\Sigma$ types: if $A$ is contractible and $B$ is contractible
+at the centre of contraction of $A$, then $\Sigma~ A~ B$ is contractible.
+
+```agda
+Σ-is-contr
+  : {A : Type ℓ} {B : A → Type ℓ'}
+  → (A-contr : is-contr A)
+  → (B-contr : is-contr (B (A-contr .centre)))
+  → is-contr (Σ A B)
+Σ-is-contr {A = A} {B = B} A-contr B-contr .centre =
+  A-contr .centre , B-contr .centre
+Σ-is-contr {A = A} {B = B} A-contr B-contr .paths (a , b) =
+  A-contr .paths a ,ₚ
+  is-contr→pathp (λ i → coe0→i (λ i → is-contr (B (A-contr .paths a i))) i B-contr)
+    (B-contr .centre)
+    b
+```
+
 Similarly, `Lift`{.Agda} does not induce a change of h-levels, i.e. if
 $A$ is an $n$-type in a universe $U$, then it's also an $n$-type in any
 successor universe:

src/1Lab/Path/IdentitySystem.lagda.md

@@ -119,21 +119,32 @@ to-path-over-refl {a = a} ids = ap (ap snd) $ to-path-refl-coh ids a
 Note that for any $(R, r)$, the type of identity system data on $(R, r)$
 is a [[proposition]]. This is because it is exactly equivalent to the type
 $\sum_a (R a)$ being contractible for every $a$, which is a proposition
-by standard results. One direction is `is-contr-ΣR`{.Agda}; we prove
-the converse direction now.
+by standard results.
+
+First, a general observation: $(R, r)$ is an identity system if the type
+$\Sigma~ A~ (R a)$ of "$R$-singletons" is a proposition for every $a : A$.
 
 ```agda
-contr→identity-system
+singleton-prop→identity-system
   : ∀ {ℓ ℓ'} {A : Type ℓ} {R : A → A → Type ℓ'} {r : ∀ a → R a a}
-  → (∀ {a} → is-contr (Σ _ (R a)))
+  → (∀ {a} → is-prop (Σ A (R a)))
   → is-identity-system R r
-contr→identity-system {R = R} {r} c = ids where
-  paths' : ∀ {a} (p : Σ _ (R a)) → (a , r a) ≡ p
-  paths' _ = is-contr→is-prop c _ _
+singleton-prop→identity-system {r = r} fib-prop .to-path {a = a} {b = b} p =
+  ap fst (fib-prop (a , r a) (b , p))
+singleton-prop→identity-system {r = r} fib-prop .to-path-over {a = a} {b = b} p =
+  ap snd (fib-prop (a , r a) (b , p))
+```
 
-  ids : is-identity-system R r
-  ids .to-path p = ap fst (paths' (_ , p))
-  ids .to-path-over p = ap snd (paths' (_ , p))
+Every contractible type is a proposition, so the converse direction
+of our equivalence follows immediately.
+
+```agda
+contr→identity-system
+  : ∀ {ℓ ℓ'} {A : Type ℓ} {R : A → A → Type ℓ'} {r : ∀ a → R a a}
+  → (∀ {a} → is-contr (Σ A (R a)))
+  → is-identity-system R r
+contr→identity-system {R = R} {r} c =
+  singleton-prop→identity-system (is-contr→is-prop c)
 ```
 
 If we have a relation $R$ together with reflexivity witness $r$, then

src/1Lab/Prelude.agda

@@ -40,6 +40,7 @@ open import 1Lab.Univalence.SIP
 
 open import 1Lab.Type.Pi public
 open import 1Lab.Type.Sigma public
+open import 1Lab.Type.Sigma.Basis public
 open import 1Lab.Type.Pointed public
 
 open import 1Lab.HIT.Truncation

src/1Lab/Type.lagda.md

@@ -134,6 +134,29 @@ case x return P of f = f x
 {-# INLINE case_of_        #-}
 {-# INLINE case_return_of_ #-}
 
+←⟨⟩-syntax
+  : ∀ {ℓa ℓb} {A : Type ℓa}
+  → (B : Type ℓb)
+  → (x : A)
+  → (f : A → B)
+  → B
+←⟨⟩-syntax B x f = f x
+
+←⟨⟩∎-syntax
+  : ∀ {ℓa}
+  → (A : Type ℓa)
+  → A
+  → A
+←⟨⟩∎-syntax A x = x
+
+{-# INLINE ←⟨⟩-syntax #-}
+{-# INLINE ←⟨⟩∎-syntax #-}
+
+syntax ←⟨⟩-syntax B x f = B ←⟨ f ⟩ x
+syntax ←⟨⟩∎-syntax A x = A ←⟨ x ⟩∎
+infixr 2 ←⟨⟩-syntax
+infix 3 ←⟨⟩∎-syntax
+
 instance
   Number-Lift : ∀ {ℓ ℓ'} {A : Type ℓ} → ⦃ Number A ⦄ → Number (Lift ℓ' A)
   Number-Lift {ℓ' = ℓ'} ⦃ a ⦄ .Number.Constraint n = Lift ℓ' (a .Number.Constraint n)

src/1Lab/Type/Pi.lagda.md

@@ -260,5 +260,16 @@ flip
   : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : A → B → Type ℓ''}
   → (∀ a b → C a b) → (∀ b a → C a b)
 flip f b a = f a b
+
+precompose-is-equiv
+  : {f : B → C}
+  → is-equiv f
+  → is-equiv {A = A → B} (f ∘_)
+precompose-is-equiv {f = f} f-eqv =
+  is-iso→is-equiv λ where
+    .is-iso.from → f.from ∘_
+    .is-iso.rinv g → funext λ x → f.ε (g x)
+    .is-iso.linv g → funext λ x → f.η (g x)
+  where module f = Equiv (f , f-eqv)
 ```
 -->

src/1Lab/Type/Sigma.lagda.md

@@ -14,9 +14,10 @@ module 1Lab.Type.Sigma where
 <!--
 ```agda
 private variable
-  ℓ ℓ₁ : Level
-  A A' X X' Y Y' Z Z' : Type ℓ
+  ℓ ℓ' ℓ'' : Level
+  T A A' X X' Y Y' Z Z' : Type ℓ
   B P Q : A → Type ℓ
+  C : (x : A) → B x → Type ℓ
 ```
 -->
 
@@ -34,7 +35,7 @@ structure of their domain types:
 
 ```agda
 Σ-pathp≃
-  : {A : I → Type ℓ} {B : (i : I) → A i → Type ℓ₁}
+  : {A : I → Type ℓ} {B : (i : I) → A i → Type ℓ'}
     {x : Σ (A i0) (B i0)} {y : Σ (A i1) (B i1)}
   → (Σ[ p ∈ PathP A (x .fst) (y .fst) ]
       (PathP (λ i → B i (p i)) (x .snd) (y .snd)))
@@ -117,23 +118,6 @@ they are included for completeness. </summary>
         k (i = i0) → ctrP (~ k)
         k (i = i1) → σ (~ k)
         k (k = i0) → b
-
-Σ-assoc : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : A → Type ℓ'} {C : (x : A) → B x → Type ℓ''}
-        → (Σ[ x ∈ A ] Σ[ y ∈ B x ] C x y) ≃ (Σ[ x ∈ Σ _ B ] (C (x .fst) (x .snd)))
-Σ-assoc .fst (x , y , z) = (x , y) , z
-Σ-assoc .snd = is-iso→is-equiv λ where
-  .is-iso.from ((x , y) , z) → x , y , z
-  .is-iso.linv p → refl
-  .is-iso.rinv p → refl
-
-Σ-Π-distrib : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : A → Type ℓ'} {C : (x : A) → B x → Type ℓ''}
-            → ((x : A) → Σ[ y ∈ B x ] C x y)
-            ≃ (Σ[ f ∈ ((x : A) → B x) ] ((x : A) → C x (f x)))
-Σ-Π-distrib .fst f = (λ x → f x .fst) , λ x → f x .snd
-Σ-Π-distrib .snd = is-iso→is-equiv λ where
-  .is-iso.from (f , r) x → f x , r x
-  .is-iso.linv p → refl
-  .is-iso.rinv p → refl
 ```
 </details>
 
@@ -252,9 +236,6 @@ If `B` is a family of contractible types, then `Σ B ≃ A`:
 Σ-map₂ : ({x : A} → P x → Q x) → Σ _ P → Σ _ Q
 Σ-map₂ f (x , y) = (x , f y)
 
-⟨_,_⟩ : (X → Y) → (X → Z) → X → Y × Z
-⟨ f , g ⟩ x = f x , g x
-
 ×-map : (A → A') → (X → X') → A × X → A' × X'
 ×-map f g (x , y) = (f x , g y)
 
@@ -316,13 +297,73 @@ infixr 4 _,ₚ_
 ```
 -->
 
-<!--
+## The universal property of sigma types {defines="universal-property-of-sigma-types"}
+
+Like all good type formers, $\Sigma$ types obey a universal property.
+First, observe that every pair of functions $f : (x : A) \to B\; x$,
+$g : (x : A) \to C\; x\; (f\; x)$ induces a map
+$$\langle f , g \rangle : (x : A) \to \Sigma\; (B\; x)\; (C\; x\; (f\; x))$$
+
 ```agda
-module _ {ℓ ℓ' ℓ''} {X : Type ℓ} {Y : X → Type ℓ'} {Z : (x : X) → Y x → Type ℓ''} where
-  curry : ((p : Σ X Y) → Z (p .fst) (p .snd)) → (x : X) → (y : Y x) → Z x y
-  curry f a b = f (a , b)
+⟨_,_⟩
+  : (f : (x : A) → B x)
+  → (g : (x : A) → C x (f x))
+  → (x : A) → Σ (B x) (C x)
+⟨ f , g ⟩ x = f x , g x
+```
 
-  uncurry : ((x : X) → (y : Y x) → Z x y) → (p : Σ X Y) → Z (p .fst) (p .snd)
-  uncurry f (a , b) = f a b
+Moreover, this map is part of an equivalence between functions
+$(x : A) \to \Sigma\; (B\; x)\; (C\; x\; (f\; x)$ into a $\Sigma$ type
+and pairs of functions into the components of the $\Sigma$ type.
+
+```agda
+Σ-Π-distrib
+  : ((x : A) → Σ[ y ∈ B x ] C x y)
+  ≃ (Σ[ f ∈ ((x : A) → B x) ] ((x : A) → C x (f x)))
+Σ-Π-distrib .fst f = (λ x → f x .fst) , (λ x → f x .snd)
+Σ-Π-distrib .snd = is-iso→is-equiv λ where
+  .is-iso.from (f , g) → ⟨ f , g ⟩
+  .is-iso.linv p → refl
+  .is-iso.rinv p → refl
+```
+
+However, this isn't the only universal property that $\Sigma$ types enjoy.
+Our previous universal property let us characterise maps *into* $\Sigma$
+types: we also have a universal characterisation of maps *out* of $\Sigma$ types.
+
+First, observe that we can pass between functions $(ab : \Sigma\; A\; B) \to C\; (\pi_1\; ab)\; (\pi_2\; ab)$
+and functions $(a : A) \to (b : B\; a) \to C\; a\; b$.
+
+```agda
+curry : ((ab : Σ A B) → C (ab .fst) (ab .snd)) → (x : A) → (y : B x) → C x y
+curry f a b = f (a , b)
+
+uncurry : ((x : A) → (y : B x) → C x y) → (ab : Σ A B) → C (ab .fst) (ab .snd)
+uncurry f (a , b) = f a b
+```
+
+We can then assemble these two maps into an equivalence.
+
+```agda
+Π-Σ-distrib
+  : ((ab : Σ A B) → C (ab .fst) (ab .snd))
+  ≃ (((x : A) → (y : B x) → C x y))
+Π-Σ-distrib .fst = curry
+Π-Σ-distrib .snd = is-iso→is-equiv λ where
+  .is-iso.from → uncurry
+  .is-iso.rinv f → refl
+  .is-iso.linv f → refl
+```
+
+## The type arithmetic of sigma types
+
+$\Sigma$ types are associative up to equivalence.
+
+```agda
+Σ-assoc : (Σ[ x ∈ A ] Σ[ y ∈ B x ] C x y) ≃ (Σ[ x ∈ Σ _ B ] (C (x .fst) (x .snd)))
+Σ-assoc .fst (x , y , z) = (x , y) , z
+Σ-assoc .snd = is-iso→is-equiv λ where
+  .is-iso.from ((x , y) , z) → x , y , z
+  .is-iso.linv p → refl
+  .is-iso.rinv p → refl
 ```
--->