Sorial type families

Content created by Egbert Rijke, Fredrik Bakke, Julian KG, fernabnor and louismntnu.

Created on 2023-06-14.
Last modified on 2023-06-25.

module foundation.sorial-type-families where
open import foundation.universe-levels

open import foundation-core.equivalences

open import structured-types.pointed-types


The notion of sorial type family is a generalization of the notion of torsorial type family. Recall that if a type family E over a pointed type B is torsorial, then we obtain in a canonical way, for each x : B an action

  E x → (E pt ≃ E x)

A sorial type family is a type family E over a pointed type B for which we have such an action.


Sorial type families

module _
  {l1 l2 : Level} (B : Pointed-Type l1) (E : type-Pointed-Type B  UU l2)

  is-sorial-family-of-types : UU (l1  l2)
  is-sorial-family-of-types =
    (x : type-Pointed-Type B)  E x  (E (point-Pointed-Type B)  E x)

Recent changes