The 1Lab🔗

Open source, combination wiki (à la nLab) + Agda library.

• Reimplementations of everything we need, e.g.

  open import 1Lab.Path

contains basic results about identity.

• Lots of category theory (e.g. Elephant, Borceux)

• Very basic results in algebra + synthetic homotopy theory (e.g. HoTT ch. 8)

This talk is a module in the 1Lab!

The 1Lab as a library🔗

• Constructive but impredicative (propositional resizing); homotopical features used freely

• Type classes for automation, but only of properties; equipping a type with structure (e.g. algebraic) is always explicit.

• Playground for new Agda features, e.g. opaque, OVERLAPPING instances

This talk🔗

_ = uaβ

• HoTT simplifies Martin-Löf type theory by giving universes a nice universal property (univalence)

• Cubical type theory complicates type theory to make this compute (uaβ)

Lots of work has gone into usability of traditional proof assistants; but what about higher dimensional proof assistants?

Working with the interval🔗

module _ where private

  cong : (f : A → B) (x y : A) → x ≡ y → f x ≡ f y
  cong f x y p = λ i → f (p i)

  sym : (x y : A) → x ≡ y → y ≡ x
  sym x y p = λ i → p (~ i)

  funext : (f g : A → B) (h : ∀ x → f x ≡ g x) → f ≡ g
  funext f g h = λ i → λ x → h x i

  subst : (P : A → Type) {x y : A} (p : x ≡ y) → P x → P y
  subst P p x = transport (λ i → P (p i)) x

We can even explain things like pattern matching on HITs:

module _ where private

  example : (p : S¹) → S¹
  example base = base
  example (loop i) = {! !}
  -- Goal: S¹
  --  i = i0 ⊢ base
  --  i = i1 ⊢ base

  example' : (p : S¹) → P p → S¹
  example' base x = base
  example' (loop i) x = {!   !}

It’s not all perfect🔗

Introducing path abstractions does a number on inference:

module _ where private

  what : ((x y : A) → x ≡ y) → (x y : A) → x ≡ y
  what h x y i = h _ _ i

Agda generates constraints:

  _x h x y (i = i0) = x
  _y h x y (i = i1) = y

Neither of these is fully determined!
Both metas go unsolved.

Surprisingly, we can use type classes!

open 1Lab.Prelude using (funext)

module _ where private

  record Extensional (A : Type) : Type (lsuc lzero) where
    field
      _≈_     : A → A → Type
      to-path : ∀ {x y : A} → x ≈ y → x ≡ y

  open Extensional ⦃ ... ⦄ renaming (to-path to ext) using ()
  open Extensional

  instance
    ext-fun : ⦃ Extensional B ⦄ → Extensional (A → B)
    ext-fun ⦃ e ⦄ = record
      { _≈_     = λ f g → ∀ x → e ._≈_ (f x) (g x)
      ; to-path = λ h → funext λ x → e .to-path (h x)
      }

    ext-base : Extensional A
    ext-base = record { to-path = λ x → x }
    {-# OVERLAPPABLE ext-base #-}

We can test that this works by asking Agda to check ext at various types:

  _ : {A B : Type} {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g
  _ = ext

  _ : {A B C : Type} {f g : A → B → C} → (∀ x y → f x y ≡ g x y) → f ≡ g
  _ = ext

  _ : {A : Type} {x y : A} → x ≡ y → x ≡ y
  _ = ext

  instance
    ext-uncurry : ⦃ Extensional (A → B → C) ⦄ → Extensional (A × B → C)
    ext-uncurry ⦃ e ⦄ = record
      { _≈_     = λ f g → e ._≈_ (curry f) (curry g)
      ; to-path = λ h i (x , y) → e .to-path h i x y
      }
    {-# OVERLAPPING ext-uncurry #-}

  _ : {A B C D : Type} {f g : A × B → C → D}
    → (∀ a b c → f (a , b) c ≡ g (a , b) c)
    → f ≡ g
  _ = ext

open 1Lab.Prelude using (ext)

module _ where private

The real implementation handles maps of algebraic structures, e.g. groups,

  _ : {G H : Group lzero} {f g : Groups.Hom G H}
    → ((x : ⌞ G ⌟) → f # x ≡ g # x) → f ≡ g
  _ = ext

maps from certain higher inductive types, e.g. generic set-quotients, or abelian group homomorphisms from a tensor product,

  _ : {A B C : Abelian-group lzero} {f g : Ab.Hom (A ⊗ B) C}
    → ((x : ⌞ A ⌟) (y : ⌞ B ⌟) → f # (x , y) ≡ g # (x , y))
    → f ≡ g
  _ = ext

and also: natural transformations, maps in slice categories, in comma categories, in categories of elements, in wide and full subcategories, in categories of monad algebras, type-theoretic equivalences and embeddings, monotone maps, &c., &c.

Univalence says $(A\equiv B)$ is equivalent to $(A\simeq B)\text{:}$

• Just as much control over $p:A\equiv B$ as we would have over $f:A\simeq B\text{;}$

  • E.g. exactly two inhabitants $\mathrm{ua}(\mathrm{id})\text{,}$ $\mathrm{ua}(\mathrm{not})$ in $\{0,1\}\equiv \{0,1\}$

Funny looking consequences: e.g. $\mathbb{Z}\simeq \mathbb{N}\text{,}$ and “$\mathbb{Z}$ is a group”, so transport lets us conclude “$\mathbb{N}$ is a group.”

Implications for library design?

Stuff vs. structure vs. property🔗

The traditional approach for doing algebra in a proof assistant is by letting the elaborator fill in the structure

• E.g. mathlib4 (Lean): extensive use of type classes
• E.g. mathcomp (Rocq): canonical structures

Technically different approaches, but, in effect, you can say $x,y:\mathbb{Z}$ and write “$x+y$” to mean “the addition on $\mathbb{Z}$”

From a user’s POV, great! Can write maths “as on paper” and the system does “the right thing”.

But it’s actually pretty funny if you think about it:

• “Additive” monoid vs “multiplicative” monoid; the same algebraic structure, but the entire hierarchy is duplicated

• Type synonyms like OrderDual: $P^{\mathrm{od}}$ is definitionally $P\text{,}$ but type class search doesn’t respect that

• Requires careful setup to avoid diamonds

• Mostly sensible for concrete types, but “the” order on $X\times Y$ is a choice!

In effect, mathematical vernacular makes explicit the stuff, leaves the structure implicit, and hardly ever mentions the properties.

Our approach is to always bundle types with the structure under consideration. Three-layered approach:

record is-ring {A : Type} (1r : A) (_*_ _+_ : A → A → A) : Type where
  -- _*_ is a monoid, _+_ is an abelian group, distributivity

record Ring-on (A : Type) : Type where
  field
    1r      : A
    _*_ _+_ : A → A → A

    has-is-ring : is-ring 1r _*_ _+_

Ring : Type₁
Ring = Σ[ T ∈ Type ] Ring-on T -- almost

_ = is-group
_ = Group-on
_ = Monoid-on

Similarly is-group/Group-on/Group, is-monoid/Monoid-on/Monoid, etc.

This layered approach still requires a bit of choosing. Categorically, the guidelines are:

• Forgetting the properties should be fully faithful
• Forgetting the structure should be faithful

Type-theoretically, we can say:

• The properties should be a family of propositions
• The structure should preserve h-level

These sometimes conflict: once we fix the multiplication, a monoid has…

• exactly one identity element (so we could put it in the properties), but
• multiplication-preserving maps of monoids don’t necessarily preserve the identity (so it’s actually a structure).

Identity of structures🔗

Simplifying a bit, a monoid $M$ is a tuple $(M_0,\ast ,1,\lambda ,\rho ,\alpha )$ consisting of

• The stuff: $M_0\text{;}$
• The structure: the binary operator and the identity;
• The property: the proofs of identity on the left, on the right, and of associativity.

When are two monoids the same?

Let’s make it a bit more formal: we define the property, parametrised over the stuff and the structure;

is-monoid : (M : Type) → (M → M → M) → M → Type
is-monoid M m u =
  is-set M            -- required so is-monoid is a property
  × (∀ x → m u x ≡ x) -- left identity
  × (∀ x → m x u ≡ x) -- right identity
  × (∀ x y z → m x (m y z) ≡ m (m x y) z) -- associativity

We’ll need that it’s an actual property:

is-monoid-is-prop : ∀ M m u → is-prop (is-monoid M m u)

is-monoid-is-prop _ _ _ = Σ-is-hlevel 1 (is-hlevel-is-prop 2) λ mset →
  let instance _ = hlevel-instance {n = 2} mset in hlevel 1

Then we sum it all:

Monoid : Type₁
Monoid =
  Σ[ M ∈ Type ]                   -- stuff
  Σ[ m ∈ (M → M → M) ] Σ[ u ∈ M ] -- structure
    (is-monoid M m u)             -- property

Completely formally, a Monoid has 7 fields, but we’ve shown that 4 don’t matter.

Then we can compute the identity type: If we have monoids $M=(M_0,m,u,\alpha )$ and $N=(N_0,n,v,\beta )\text{,}$ what is $M\equiv N\text{?}$

module _ (M@(M₀ , m , u , α) N@(N₀ , n , v , β) : Monoid) where

  Step₁ : Type₁
  Step₁ = Σ[ p ∈ M₀ ≡ N₀ ]
    ( PathP (λ i → p i → p i → p i) m n
    × PathP (λ i → p i) u v
    )

  step₁ : Step₁ → M ≡ N
  step₁ (p , q , r) i = p i , q i , r i ,
    is-prop→pathp (λ i → is-monoid-is-prop (p i) (q i) (r i)) α β i

Step 2: we can simplify the PathPs to talk about transport instead:

  Step₂ : Type₁
  Step₂ = Σ[ p ∈ M₀ ≡ N₀ ]
    ( (∀ x y → transport p (m x y) ≡ n (transport p x) (transport p y))
    × transport p u ≡ v
    )

  step₂ : Step₂ → Step₁
  step₂ (p , q , r) = p , q' , to-pathp r where
    -- q' actually pretty complicated...
    q' = funext-dep λ α → funext-dep λ β →
      to-pathp (q _ _ ∙ ap₂ n (from-pathp α) (from-pathp β))

Step 3: we know what identity of types is!

  Step₃ : Type
  Step₃ = Σ[ p ∈ M₀ ≃ N₀ ] -- equivalence!
    ( (∀ x y → p .fst (m x y) ≡ n (p .fst x) (p .fst y))
    × p .fst u ≡ v
    )

Takes a bit of massaging…

  step₃ : Step₃ → Step₂
  step₃ (p , q , r) = ua p , q' , r' where
    r' = transport (ua p) u ≡⟨ uaβ p u ⟩
         p .fst u           ≡⟨ r ⟩
         v                  ∎

    q' : ∀ x y → _
    q' x y =
      transport (ua p) (m x y)                    ≡⟨ uaβ p (m x y) ⟩
      p .fst (m x y)                              ≡⟨ q x y ⟩
      n (p .fst x) (p .fst y)                     ≡⟨ ap₂ n (sym (uaβ p x)) (sym (uaβ p y)) ⟩
      n (transport (ua p) x) (transport (ua p) y) ∎

The conclusion: identity in the type Monoid is exactly¹ monoid isomorphism!

The idea: turn fibers into families.

  record Displayed o' ℓ' : Type (o ⊔ ℓ ⊔ lsuc (o' ⊔ ℓ')) where
    field
      Ob[_]  : ⌞ C ⌟ → Type o'
      Hom[_] : (f : Hom x y) → Ob[ x ] → Ob[ y ] → Type ℓ'

      id'  : {x' : Ob[ x ]} → Hom[ id ] x' x'
      _∘'_
        : {x' : Ob[ x ]} {y' : Ob[ y ]} {z' : Ob[ z ]}
        → {f : Hom y z} (f' : Hom[ f ] y' z')
        → {g : Hom x y} (g' : Hom[ g ] x' y')
        → Hom[ f ∘ g ] x' z'

If we start with a displayed category $\mathcal{E}\mathcal{C}\text{,}$ we can put together a category with objects ${\sum }_{x:\mathcal{C}}\mathrm{Ob}[x]$ — the total category $\int \mathcal{E}\text{.}$

Similarly, each $x:\mathcal{C}$ gives a category ${\mathcal{E}}^{\ast }(x)$ with objects $\mathrm{Ob}[x]$ and maps $\mathrm{Hom}[\mathrm{id}](-,-)$ — the fibre over $x\text{.}$

Properties of the functor $\pi :\int \mathcal{E}\to \mathcal{C}$ map very nicely to properties of $\mathcal{E}\text{!}$

That last row is important!

If we start with a functor, then $\mathrm{Ob}[x]$ is the type ${\sum }_{y:\mathcal{D}}\pi (y)\cong x\text{;}$ the “fibre” of $\pi$ over $x\text{.}$

private module _ {o ℓ o' ℓ' : Level} {C : Precategory o ℓ} {D : Precategory o' ℓ'} (π : Functor D C) where private
  private
    module C = Cat C
    module D = Cat D
    module π = Functor π
    open C using (_∘_ ; id ; _≅_)

    open C._≅_
  open Displayed

  Street : Displayed C _ _
  Street .Ob[_] x = Σ[ y ∈ D ] (π.₀ y ≅ x)

The maps over are more complicated:

  Street .Hom[_] f (x' , i) (y' , j) = Σ[ g ∈ D.Hom x' y' ]
    (π.₁ g ≡ j .from ∘ f ∘ i .to)

Accordingly, the structure is pretty annoying:

  Street .id' {x} {x' , i} = record { snd =
    π.₁ D.id               ≡⟨ π.F-id ⟩
    id                     ≡˘⟨ i .invr ⟩
    i .from ∘ i .to        ≡˘⟨ ap₂ _∘_ refl (C.idl _) ⟩
    i .from ∘ id C.∘ i .to ∎ }
  Street ._∘'_ = _ -- even worse!

We can present a concrete, univalent category as a displayed category.

• Concrete: the base is $\mathbf{Sets}$ and each $\mathrm{Hom}[-](-,-)$ is a proposition.
• Univalent: each ${\mathcal{E}}^{\ast }(x)$ is a partial order.

Then we define the structure:

record Semigroup-on (A : Type ℓ) : Type ℓ where
  field
    _⋆_              : A → A → A
    has-is-semigroup : is-semigroup _⋆_
  open is-semigroup has-is-semigroup public

… and what it means for functions to preserve it:

record is-semigroup-hom (f : A → B) (S : Semigroup-on A) (T : Semigroup-on B)
  : Type (level-of A ⊔ level-of B) where

  private
    module S = Semigroup-on S
    module T = Semigroup-on T

  field
    pres-⋆ : ∀ x y → f (x S.⋆ y) ≡ f x T.⋆ f y

private
  unquoteDecl eqv = declare-record-iso eqv (quote Semigroup-on)
  unquoteDecl eqv' = declare-record-iso eqv' (quote is-semigroup-hom)

instance
  H-Level-is-semigroup : ∀ {n} {s : A → A → A} → H-Level (is-semigroup s) (suc n)
  H-Level-is-semigroup = prop-instance is-semigroup-is-prop

  H-Level-is-semigroup-hom
    : ∀ {n} {f : A → B} {S : Semigroup-on A} {T : Semigroup-on B}
    → H-Level (is-semigroup-hom f S T) (suc n)
  H-Level-is-semigroup-hom {T = T} = prop-instance (Iso→is-hlevel 1 eqv' (hlevel 1))
    where instance _ = hlevel-instance {n = 2} (T .Semigroup-on.has-is-set)

open is-semigroup-hom

We can then fill in the four bullet points. $F$ is Semigroup-on, $\mathrm{Hom}[-](-,-)$ is is-semigroup-hom,

Semigroup-structure : ∀ {ℓ} → Thin-structure ℓ Semigroup-on
Semigroup-structure .is-hom f S T = el! (is-semigroup-hom f S T)

… identities and composites are respected …

Semigroup-structure .id-is-hom .pres-⋆ x y = refl
Semigroup-structure .∘-is-hom f g α β .pres-⋆ x y =
  ap f (β .pres-⋆ x y) ∙ α .pres-⋆ _ _

and, finally, the univalence condition:

Semigroup-structure .id-hom-unique p q = Iso.injective eqv $ Σ-prop-path! $
  ext λ a b → p .pres-⋆ a b