Homotopy Type Theory
filter > history (changes)
Showing changes from revision #1 to #2:
Added | Removed | Changed
Definition
< filter
Let S S be a set , Prop 𝒰 ( i ) Prop_{\mathcal{U}(i)} be the type of propositions? in a universe , and Prop 𝒰 ( s ( i ) ) Prop_{\mathcal{U}(s(i))} be the type of propositions in a successor universe. Then a filter on S S is a predicate F : ( S → Prop 𝒰 ( i ) ) → Prop 𝒰 ( s ( i ) ) F:(S \to Prop_{\mathcal{U}(i)}) \to Prop_{\mathcal{U}(s(i))} with dependent functions
p : ∏ a : S → Prop 𝒰 ( i ) ∏ b : S → Prop 𝒰 ( i ) ( a = a ∧ b ) × 𝒯 𝒰 ( i ) ( F ( a ) ) → 𝒯 𝒰 ( i ) ( F ( b ) ) p:\prod_{a:S \to Prop_{\mathcal{U}(i)}} \prod_{b:S \to Prop_{\mathcal{U}(i)}} (a = a \wedge b) \times \mathcal{T}_{\mathcal{U}(i)}(F(a)) \to \mathcal{T}_{\mathcal{U}(i)}(F(b)) p : [ ∑ a : S → Prop 𝒰 ( i ) 𝒯 𝒰 ( i ) ( F ( a ) ) ] p:\left[\sum_{a:S \to Prop_{\mathcal{U}(i)}} \mathcal{T}_{\mathcal{U}(i)}(F(a))\right] p : [ ∑ a : S → Prop 𝒰 ( i ) ∑ b : S → Prop 𝒰 ( i ) 𝒯 𝒰 ( i ) ( F ( a ) ) × 𝒯 𝒰 ( i ) ( F ( b ) ) → [ ∑ c : S → Prop 𝒰 ( i ) 𝒯 𝒰 ( i ) ( F ( c ) ) × ( c = c ∧ a ) × ( c = c ∧ b ) ] ] p:\left[\sum_{a:S \to Prop_{\mathcal{U}(i)}} \sum_{b:S \to Prop_{\mathcal{U}(i)}} \mathcal{T}_{\mathcal{U}(i)}(F(a)) \times \mathcal{T}_{\mathcal{U}(i)}(F(b)) \to \left[\sum_{c:S \to Prop_{\mathcal{U}(i)}} \mathcal{T}_{\mathcal{U}(i)}(F(c)) \times (c = c \wedge a) \times (c = c \wedge b)\right]\right]
The filter properties could also be turned into structure:
A filter structure on S S predicate F : ( S → Prop 𝒰 ( i ) ) → Prop 𝒰 ( s ( i ) ) F:(S \to Prop_{\mathcal{U}(i)}) \to Prop_{\mathcal{U}(s(i))}
p : ∏ a : S → Prop 𝒰 ( i ) ∏ b : S → Prop 𝒰 ( i ) ( a = a ∧ b ) × 𝒯 𝒰 ( i ) ( F ( a ) ) → 𝒯 𝒰 ( i ) ( F ( b ) ) p:\prod_{a:S \to Prop_{\mathcal{U}(i)}} \prod_{b:S \to Prop_{\mathcal{U}(i)}} (a = a \wedge b) \times \mathcal{T}_{\mathcal{U}(i)}(F(a)) \to \mathcal{T}_{\mathcal{U}(i)}(F(b)) p : ∑ a : S → Prop 𝒰 ( i ) 𝒯 𝒰 ( i ) ( F ( a ) ) p:\sum_{a:S \to Prop_{\mathcal{U}(i)}} \mathcal{T}_{\mathcal{U}(i)}(F(a)) p : ∑ a : S → Prop 𝒰 ( i ) ∑ b : S → Prop 𝒰 ( i ) 𝒯 𝒰 ( i ) ( F ( a ) ) × 𝒯 𝒰 ( i ) ( F ( b ) ) → ∑ c : S → Prop 𝒰 ( i ) 𝒯 𝒰 ( i ) ( F ( c ) ) × ( c = c ∧ a ) × ( c = c ∧ b ) p:\sum_{a:S \to Prop_{\mathcal{U}(i)}} \sum_{b:S \to Prop_{\mathcal{U}(i)}} \mathcal{T}_{\mathcal{U}(i)}(F(a)) \times \mathcal{T}_{\mathcal{U}(i)}(F(b)) \to \sum_{c:S \to Prop_{\mathcal{U}(i)}} \mathcal{T}_{\mathcal{U}(i)}(F(c)) \times (c = c \wedge a) \times (c = c \wedge b)
See also
Last revised on June 9, 2022 at 23:50:38.
See the history of this page for a list of all contributions to it.