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
Imports 
open import foundation.universe-levels

open import foundation-core.equivalences

open import structured-types.pointed-types

Idea

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.

Definitions

Sorial type families

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

  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