Local families

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-09-11.
Last modified on 2023-11-24.

module orthogonal-factorization-systems.local-families where
Imports
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.precomposition-functions
open import foundation.propositions
open import foundation.universe-levels

open import orthogonal-factorization-systems.local-types

Idea

A family B : A → UU l is said to be local at f : Y → X, or f-local, if every fiber is.

Definition

is-local-family :
  {l1 l2 l3 l4 : Level} {Y : UU l1} {X : UU l2}
  (f : Y  X) {A : UU l3}  (A  UU l4)  UU (l1  l2  l3  l4)
is-local-family f {A} B = (x : A)  is-local f (B x)

Properties

Being local is a property

module _
  {l1 l2 : Level} {Y : UU l1} {X : UU l2} (f : Y  X)
  where

  is-property-is-local-family :
    {l3 l4 : Level} {A : UU l3}
    (B : A  UU l4)  is-prop (is-local-family f B)
  is-property-is-local-family B =
    is-prop-Π  x  is-property-is-equiv (precomp f (B x)))

  is-local-family-Prop :
    {l3 l4 : Level} {A : UU l3}
    (B : A  UU l4)  Prop (l1  l2  l3  l4)
  pr1 (is-local-family-Prop B) = is-local-family f B
  pr2 (is-local-family-Prop B) = is-property-is-local-family B

A family is f-local if and only if it is f-orthogonal

This remains to be formalized.

See also

Recent changes