index βˆ™ source

Imports 
open import Cat.Prelude hiding (J)
open import Cat.Diagram.Limit.Base
open import Cat.Instances.Discrete
open import Cat.Instances.Shape.Join
open import Cat.Instances.Product

open import Data.Sum

import Cat.Reasoning
import Cat.Functor.Reasoning
import Cat.Functor.Bifunctor

open Precategory
open Functor
open make-is-limit

This module formalises a few very interesting results from Jem Lord’s recent work on Easy Parametricity, presented at HoTT/UF 2025.

module EasyParametricity {u} where

U = Type u
𝟘 = Lift u βŠ₯
πŸ™ = Lift u ⊀

-- We think of functions f : U β†’ A as "bridges" from f 𝟘 to f πŸ™.
record Bridge {β„“} (A : Type β„“) (x y : A) : Type (β„“ βŠ” lsuc u) where
  no-eta-equality
  constructor bridge
  pattern
  field
    app  : U β†’ A
    app𝟘 : app 𝟘 ≑ x
    appπŸ™ : app πŸ™ ≑ y

-- Every function preserves bridges.
ap-bridge
  : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'} (f : A β†’ B) {x y : A}
  β†’ Bridge A x y β†’ Bridge B (f x) (f y)
ap-bridge f (bridge app app𝟘 appπŸ™) = bridge (f βŠ™ app) (ap f app𝟘) (ap f appπŸ™)

postulate
  -- An immediate consequence of Jem Lord's parametricity axiom: a function
  -- out of U into a U-small type cannot tell 0 and 1 apart; this is all we need here.
  -- In other words, U-small types are bridge-discrete.
  parametricity : βˆ€ {A : U} {x y : A} β†’ Bridge A x y β†’ x ≑ y

-- The type of formal composites r ∘ l : A β†’ B in C. We want to think of this
-- as the type of factorisations of some morphism f : A β†’ B, but it turns out
-- to be unnecessary to track f in the type.
record Factorisation {o β„“} (C : Precategory o β„“) (A B : C .Ob) : Type (o βŠ” β„“) where
  constructor factor
  module C = Precategory C
  field
    X : C.Ob
    l : C.Hom A X
    r : C.Hom X B

module _
  {o β„“} {C : Precategory o β„“}
  (let module C = Precategory C)
  where

  module _ {A B : C.Ob} (f : C.Hom A B) where

    -- The two factorisations id ∘ f and f ∘ id.
    _∘id id∘_ : Factorisation C A B
    _∘id = factor A C.id f
    id∘_ = factor B f C.id

  module _
    (C-complete : is-complete u lzero C)
    (C-category : is-category C)
    {A B : C.Ob} (f : C.Hom A B)
    where

    -- In a U-complete univalent category, every type of factorisations is bridge-codiscrete.
    -- We define a bridge from id ∘ f to f ∘ id.

    factorisation-bridge : Bridge (Factorisation C A B) (id∘ f) (f ∘id)
    factorisation-bridge = bridge b b0 b1 where

      b : U β†’ Factorisation C A B
      b P = fac (C-complete diagram) module b where

        -- This is the interesting part: given a type P : U, we construct the
        -- wide pullback of P-many copies of f.
        -- Since we only care about the cases where P is a proposition, we
        -- can just take the discrete or codiscrete category on P and adjoin a
        -- terminal object to get our diagram shape.
        J : Precategory u lzero
        J = Codisc' P β–Ή

        diagram : Functor J C
        diagram .Fβ‚€ (inl _) = A
        diagram .Fβ‚€ (inr _) = B
        diagram .F₁ {inl _} {inl _} _ = C.id
        diagram .F₁ {inl _} {inr _} _ = f
        diagram .F₁ {inr _} {inr _} _ = C.id
        diagram .F-id {inl _} = refl
        diagram .F-id {inr _} = refl
        diagram .F-∘ {inl _} {inl _} {inl _} _ _ = sym (C.idl _)
        diagram .F-∘ {inl _} {inl _} {inr _} _ _ = sym (C.idr _)
        diagram .F-∘ {inl _} {inr _} {inr _} _ _ = sym (C.idl _)
        diagram .F-∘ {inr _} {inr _} {inr _} _ _ = sym (C.idl _)

        -- Given a limit of this diagram (which exists by the assumption of U-completeness),
        -- we get a factorisation of f as the universal map followed by the projection to B.
        fac : Limit diagram β†’ Factorisation C A B
        fac lim = factor X l r where
          module lim = Limit lim
          X : C.Ob
          X = lim.apex
          l : C.Hom A X
          l = lim.universal (Ξ» { (inl _) β†’ C.id; (inr _) β†’ f }) Ξ» where
            {inl _} {inl _} _ β†’ C.idl _
            {inl _} {inr _} _ β†’ C.idr _
            {inr _} {inr _} _ β†’ C.idl _
          r : C.Hom X B
          r = lim.cone ._=>_.Ξ· (inr tt)

      -- We check that the endpoints of the bridge are what we expect: when P
      -- is empty, we are taking the limit of the single-object diagram B, so
      -- our factorisation is A β†’ B β†’ B.
      b0 : b 𝟘 ≑ id∘ f
      b0 = ap (b.fac 𝟘) (Limit-is-prop C-category (C-complete _) (to-limit lim)) where
        lim : is-limit (b.diagram 𝟘) B _
        lim = to-is-limit Ξ» where
          .ψ (inr _) β†’ C.id
          .commutes {inr _} {inr _} _ β†’ C.idl _
          .universal eps comm β†’ eps (inr _)
          .factors {inr _} eps comm β†’ C.idl _
          .unique eps comm other fac β†’ sym (C.idl _) βˆ™ fac (inr _)

      -- When P is contractible, we are taking the limit of the arrow diagram
      -- A β†’ B, so our factorisation is A β†’ A β†’ B.
      b1 : b πŸ™ ≑ f ∘id
      b1 = ap (b.fac πŸ™) (Limit-is-prop C-category (C-complete _) (to-limit lim)) where
        lim : is-limit (b.diagram πŸ™) A _
        lim = to-is-limit Ξ» where
          .ψ (inl _) β†’ C.id
          .ψ (inr _) β†’ f
          .commutes {inl _} {inl _} _ β†’ C.idl _
          .commutes {inl _} {inr _} _ β†’ C.idr _
          .commutes {inr _} {inr _} _ β†’ C.idl _
          .universal eps comm β†’ eps (inl (lift tt))
          .factors {inl _} eps comm β†’ C.idl _
          .factors {inr _} eps comm β†’ comm {inl _} {inr _} _
          .unique eps comm other fac β†’ sym (C.idl _) βˆ™ fac (inl _)

-- Theorem 1: let C be a U-complete univalent category and D a locally
-- U-small category.
module _
  {o o' β„“} {C : Precategory o β„“} {D : Precategory o' u}
  (let module C = Cat.Reasoning C) (let module D = Cat.Reasoning D)
  (C-complete : is-complete u lzero C)
  (C-category : is-category C)
  where

  -- 1.a: naturality of transformations between functors C β†’ D is free.
  -- (This is a special case of 1.b.)
  module _
    (F G : Functor C D)
    (let module F = Cat.Functor.Reasoning F) (let module G = Cat.Functor.Reasoning G)
    (Ξ· : βˆ€ x β†’ D.Hom (F.β‚€ x) (G.β‚€ x))
    where

    natural : is-natural-transformation F G Ξ·
    natural A B f = G.introl refl βˆ™ z0≑z1 βˆ™ (D.refl⟩∘⟨ F.elimr refl) where

      -- Given a factorisation A β†’ X β†’ B, we define the map
      --       F A
      --        ↓
      -- Ξ· X : F X β†’ G X
      --              ↓
      --             G B
      -- which recovers the naturality square for f as the factorisation varies
      -- from id ∘ f to f ∘ id.
      z : Factorisation C A B β†’ D.Hom (F.β‚€ A) (G.β‚€ B)
      z (factor X l r) = G.₁ r D.∘ Ξ· X D.∘ F.₁ l

      -- As a result, we get a bridge from one side of the naturality square
      -- to the other; since D is locally U-small, the Hom-sets of D are bridge-discrete,
      -- so we get the desired equality.
      z0≑z1 : z (id∘ f) ≑ z (f ∘id)
      z0≑z1 = parametricity (ap-bridge z (factorisation-bridge C-complete C-category f))

  -- 1.b: dinaturality of transformations between bifunctors C^op Γ— C β†’ D is free.
  module _
    (F G : Functor (C ^op Γ—αΆœ C) D)
    (let module F = Cat.Functor.Bifunctor F) (let module G = Cat.Functor.Bifunctor G)
    (Ξ· : βˆ€ x β†’ D.Hom (F.β‚€ (x , x)) (G.β‚€ (x , x)))
    where

    dinatural
      : βˆ€ A B (f : C.Hom A B)
      β†’ G.first f D.∘ Ξ· B D.∘ F.second f ≑ G.second f D.∘ Ξ· A D.∘ F.first f
    dinatural A B f = z0≑z1 where

      -- Given a factorisation A β†’ X β†’ B, we define the map
      --   F B A β†’ F X X β†’ G X X β†’ G A B
      -- which interpolates between the two sides of the dinaturality hexagon.
      z : Factorisation C A B β†’ D.Hom (F.β‚€ (B , A)) (G.β‚€ (A , B))
      z (factor X l r) = G.₁ (l , r) D.∘ Ξ· X D.∘ F.₁ (r , l)

      z0≑z1 : z (id∘ f) ≑ z (f ∘id)
      z0≑z1 = parametricity (ap-bridge z (factorisation-bridge C-complete C-category f))