Functoriality of disjunction

Content created by Louis Wasserman.

Created on 2025-03-27.
Last modified on 2025-03-27.

module foundation.functoriality-disjunction where
Imports 
open import foundation.disjunction
open import foundation.function-types
open import foundation.propositions
open import foundation.universe-levels

Idea

Any two implications f : A ⇒ B and g : C ⇒ D induce an implication map-disjunction f g : (A ∨ B) ⇒ (C ∨ D).

Definitions

The functorial action of disjunction

module _
  {l1 l2 l3 l4 : Level} (A : Prop l1) (B : Prop l2) (C : Prop l3) (D : Prop l4)
  (f : type-Prop (A ⇒ B)) (g : type-Prop (C ⇒ D))
  where

  map-disjunction : type-Prop ((A ∨ C) ⇒ (B ∨ D))
  map-disjunction =
    elim-disjunction (B ∨ D) (inl-disjunction ∘ f) (inr-disjunction ∘ g)

Recent changes