Skip to content

Commit

Permalink
Equivalence injective type families (#1009)
Browse files Browse the repository at this point in the history
I was checking out Agdas `INJECTIVE` pragma. Here are some edits I made
while exploring.
  • Loading branch information
fredrik-bakke authored Jan 28, 2024
1 parent 5f73def commit c339bac
Show file tree
Hide file tree
Showing 11 changed files with 184 additions and 41 deletions.
14 changes: 8 additions & 6 deletions src/elementary-number-theory/integers.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,8 @@ open import foundation.identity-types
open import foundation.injective-maps
open import foundation.negated-equality
open import foundation.propositions
open import foundation.retractions
open import foundation.sections
open import foundation.sets
open import foundation.unit-type
open import foundation.universe-levels
Expand Down Expand Up @@ -160,17 +162,17 @@ pr2 ℤ-Set = is-set-ℤ

```agda
abstract
is-retraction-pred-ℤ : (pred-ℤ ∘ succ-ℤ) ~ id
is-retraction-pred-ℤ : is-retraction succ-ℤ pred-ℤ
is-retraction-pred-ℤ (inl zero-ℕ) = refl
is-retraction-pred-ℤ (inl (succ-ℕ x)) = refl
is-retraction-pred-ℤ (inr (inl star)) = refl
is-retraction-pred-ℤ (inr (inl _)) = refl
is-retraction-pred-ℤ (inr (inr zero-ℕ)) = refl
is-retraction-pred-ℤ (inr (inr (succ-ℕ x))) = refl

is-section-pred-ℤ : (succ-ℤ pred-ℤ) ~ id
is-section-pred-ℤ : is-section succ-ℤ pred-ℤ
is-section-pred-ℤ (inl zero-ℕ) = refl
is-section-pred-ℤ (inl (succ-ℕ x)) = refl
is-section-pred-ℤ (inr (inl star)) = refl
is-section-pred-ℤ (inr (inl _)) = refl
is-section-pred-ℤ (inr (inr zero-ℕ)) = refl
is-section-pred-ℤ (inr (inr (succ-ℕ x))) = refl

Expand Down Expand Up @@ -213,7 +215,7 @@ has-no-fixed-points-succ-ℤ (inr (inl star)) ()
### The negative function is an involution

```agda
neg-neg-ℤ : (neg-ℤ ∘ neg-ℤ) ~ id
neg-neg-ℤ : neg-ℤ ∘ neg-ℤ ~ id
neg-neg-ℤ (inl n) = refl
neg-neg-ℤ (inr (inl star)) = refl
neg-neg-ℤ (inr (inr n)) = refl
Expand Down Expand Up @@ -419,7 +421,7 @@ decide-is-nonnegative-ℤ {inl x} = inr star
decide-is-nonnegative-ℤ {inr x} = inl star

is-zero-is-nonnegative-neg-is-nonnegative-ℤ :
(x : ℤ) (is-nonnegative-ℤ x) (is-nonnegative-ℤ (neg-ℤ x)) is-zero-ℤ x
(x : ℤ) is-nonnegative-ℤ x is-nonnegative-ℤ (neg-ℤ x) is-zero-ℤ x
is-zero-is-nonnegative-neg-is-nonnegative-ℤ (inr (inl star)) nonneg nonpos =
refl
```
Expand Down
16 changes: 8 additions & 8 deletions src/elementary-number-theory/modular-arithmetic.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -100,15 +100,15 @@ has-decidable-equality-ℤ-Mod zero-ℕ = has-decidable-equality-ℤ
has-decidable-equality-ℤ-Mod (succ-ℕ k) = has-decidable-equality-Fin (succ-ℕ k)
```

### The integers modulo k are a discrete type
### The integers modulo `k` are a discrete type

```agda
ℤ-Mod-Discrete-Type : (k : ℕ) Discrete-Type lzero
ℤ-Mod-Discrete-Type zero-ℕ = ℤ-Discrete-Type
ℤ-Mod-Discrete-Type (succ-ℕ k) = Fin-Discrete-Type (succ-ℕ k)
```

### The integers modulo k form a set
### The integers modulo `k` form a set

```agda
abstract
Expand All @@ -134,7 +134,7 @@ pr1 (ℤ-Mod-𝔽 k H) = ℤ-Mod k
pr2 (ℤ-Mod-𝔽 k H) = is-finite-ℤ-Mod H
```

## The inclusion of the integers modulo k into ℤ
## The inclusion of the integers modulo `k` into ℤ

```agda
int-ℤ-Mod : (k : ℕ) ℤ-Mod k
Expand Down Expand Up @@ -162,7 +162,7 @@ int-ℤ-Mod-bounded (succ-ℕ k) (inr x) = is-nonnegative-succ-ℤ
(is-nonnegative-eq-ℤ (inv (left-inverse-law-add-ℤ (inl k))) star)
```

## The successor and predecessor functions on the integers modulo k
## The successor and predecessor functions on the integers modulo `k`

```agda
succ-ℤ-Mod : (k : ℕ) ℤ-Mod k ℤ-Mod k
Expand Down Expand Up @@ -265,7 +265,7 @@ pr1 (equiv-neg-ℤ-Mod k) = neg-ℤ-Mod k
pr2 (equiv-neg-ℤ-Mod k) = is-equiv-neg-ℤ-Mod k
```

## Laws of addition modulo k
## Laws of addition modulo `k`

```agda
associative-add-ℤ-Mod :
Expand Down Expand Up @@ -347,7 +347,7 @@ is-left-add-neg-one-pred-ℤ-Mod' zero-ℕ = is-right-add-neg-one-pred-ℤ
is-left-add-neg-one-pred-ℤ-Mod' (succ-ℕ k) = is-add-neg-one-pred-Fin' k
```

## Multiplication modulo k
## Multiplication modulo `k`

```agda
mul-ℤ-Mod : (k : ℕ) ℤ-Mod k ℤ-Mod k ℤ-Mod k
Expand All @@ -363,7 +363,7 @@ ap-mul-ℤ-Mod :
ap-mul-ℤ-Mod k p q = ap-binary (mul-ℤ-Mod k) p q
```

## Laws of multiplication modulo k
## Laws of multiplication modulo `k`

```agda
associative-mul-ℤ-Mod :
Expand Down Expand Up @@ -414,7 +414,7 @@ is-left-mul-neg-one-neg-ℤ-Mod' zero-ℕ = is-right-mul-neg-one-neg-ℤ
is-left-mul-neg-one-neg-ℤ-Mod' (succ-ℕ k) = is-mul-neg-one-neg-Fin' k
```

## Congruence classes of integers modulo k
## Congruence classes of integers modulo `k`

```agda
mod-ℕ : (k : ℕ) ℤ-Mod k
Expand Down
8 changes: 8 additions & 0 deletions src/foundation-core/function-types.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,14 @@ map-Π' :
((j : J) A (α j))
((j : J) B (α j))
map-Π' α f = map-Π (f ∘ α)

map-implicit-Π :
{l1 l2 l3 : Level}
{I : UU l1} {A : I UU l2} {B : I UU l3}
(f : (i : I) A i B i)
({i : I} A i)
({i : I} B i)
map-implicit-Π f h {i} = map-Π f (λ i h {i}) i
```

## See also
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,7 @@ compute-fiber-map-Π' α f = compute-fiber-map-Π (f ∘ α)
abstract
is-equiv-map-Π-is-fiberwise-equiv :
{l1 l2 l3 : Level} {I : UU l1} {A : I UU l2} {B : I UU l3}
{f : (i : I) A i B i} (is-equiv-f : is-fiberwise-equiv f)
{f : (i : I) A i B i} is-fiberwise-equiv f
is-equiv (map-Π f)
is-equiv-map-Π-is-fiberwise-equiv is-equiv-f =
is-equiv-is-contr-map
Expand All @@ -80,15 +80,26 @@ abstract
equiv-Π-equiv-family :
{l1 l2 l3 : Level} {I : UU l1} {A : I UU l2} {B : I UU l3}
(e : (i : I) (A i) ≃ (B i)) ((i : I) A i) ≃ ((i : I) B i)
pr1 (equiv-Π-equiv-family e) = map-Π (λ i map-equiv (e i))
pr1 (equiv-Π-equiv-family e) =
map-Π (λ i map-equiv (e i))
pr2 (equiv-Π-equiv-family e) =
is-equiv-map-Π-is-fiberwise-equiv
( λ i is-equiv-map-equiv (e i))
is-equiv-map-Π-is-fiberwise-equiv (λ i is-equiv-map-equiv (e i))
```

### Families of equivalences induce equivalences of implicit dependent function types

```agda
is-equiv-map-implicit-Π-is-fiberwise-equiv :
{l1 l2 l3 : Level} {I : UU l1} {A : I UU l2} {B : I UU l3}
{f : (i : I) A i B i} is-fiberwise-equiv f
is-equiv (map-implicit-Π f)
is-equiv-map-implicit-Π-is-fiberwise-equiv is-equiv-f =
is-equiv-comp _ _
( is-equiv-explicit-implicit-Π)
( is-equiv-comp _ _
( is-equiv-map-Π-is-fiberwise-equiv is-equiv-f)
( is-equiv-implicit-explicit-Π))

equiv-implicit-Π-equiv-family :
{l1 l2 l3 : Level} {I : UU l1} {A : I UU l2} {B : I UU l3}
(e : (i : I) (A i) ≃ (B i)) ({i : I} A i) ≃ ({i : I} B i)
Expand Down
1 change: 1 addition & 0 deletions src/foundation.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -130,6 +130,7 @@ open import foundation.equality-fibers-of-maps public
open import foundation.equivalence-classes public
open import foundation.equivalence-extensionality public
open import foundation.equivalence-induction public
open import foundation.equivalence-injective-type-families public
open import foundation.equivalence-relations public
open import foundation.equivalences public
open import foundation.equivalences-arrows public
Expand Down
110 changes: 110 additions & 0 deletions src/foundation/equivalence-injective-type-families.lagda.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,110 @@
# Equivalence injective type families

```agda
module foundation.equivalence-injective-type-families where
```

<details><summary>Imports</summary>

```agda
open import foundation.dependent-pair-types
open import foundation.functoriality-dependent-function-types
open import foundation.iterated-dependent-product-types
open import foundation.univalence
open import foundation.universal-property-equivalences
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.identity-types
open import foundation-core.injective-maps
open import foundation-core.propositions
open import foundation-core.sets
```

</details>

## Idea

We say a type family `P` is
{{#concept "equivalence injective" Disambiguation="type family" Agda=is-equivalence-injective}}
if for every [equivalence of types](foundation-core.equivalences.md) `P x ≃ P y`
we have `x = y `. By [univalence](foundation-core.univalence.md), the
[structure](foundation.structure.md) of being equivalence injective is
equivalent to being [injective as a map](foundation-core.injective-maps.md), but
more generally every equivalence injective type family must always be injective
as a map.

**Note.** The concept of equivalence injective type family as considered here is
unrelated to the concept of "injective type" as studied by Martín Escardó in
_Injective types in univalent mathematics_
([arXiv:1903.01211](https://arxiv.org/abs/1903.01211),
[TypeTopology](https://www.cs.bham.ac.uk/~mhe/TypeTopology/InjectiveTypes.index.html)).

## Definition

### Equivalence injective type families

```agda
is-equivalence-injective :
{l1 l2 : Level} {A : UU l1} (A UU l2) UU (l1 ⊔ l2)
is-equivalence-injective {A = A} P = {x y : A} P x ≃ P y x = y
```

## Properties

### Equivalence injective type families are injective as maps

```agda
module _
{l1 l2 : Level} {A : UU l1} {P : A UU l2}
where

is-injective-is-equivalence-injective :
is-equivalence-injective P is-injective P
is-injective-is-equivalence-injective H = H ∘ equiv-eq

is-equivalence-injective-is-injective :
is-injective P is-equivalence-injective P
is-equivalence-injective-is-injective H = H ∘ eq-equiv

is-equiv-is-injective-is-equivalence-injective :
is-equiv is-injective-is-equivalence-injective
is-equiv-is-injective-is-equivalence-injective =
is-equiv-map-implicit-Π-is-fiberwise-equiv
( λ x
is-equiv-map-implicit-Π-is-fiberwise-equiv
( λ y
is-equiv-precomp-is-equiv
( equiv-eq)
( univalence (P x) (P y))
( x = y)))

equiv-is-injective-is-equivalence-injective :
is-equivalence-injective P ≃ is-injective P
pr1 equiv-is-injective-is-equivalence-injective =
is-injective-is-equivalence-injective
pr2 equiv-is-injective-is-equivalence-injective =
is-equiv-is-injective-is-equivalence-injective

equiv-is-equivalence-injective-is-injective :
is-injective P ≃ is-equivalence-injective P
equiv-is-equivalence-injective-is-injective =
inv-equiv equiv-is-injective-is-equivalence-injective
```

### For a type family over a set, being equivalence injective is a property

```agda
module _
{l1 l2 : Level} {A : UU l1} (is-set-A : is-set A) (P : A UU l2)
where

is-prop-is-equivalence-injective : is-prop (is-equivalence-injective P)
is-prop-is-equivalence-injective =
is-prop-iterated-implicit-Π 2 (λ x y is-prop-function-type (is-set-A x y))

is-equivalence-injective-Prop : Prop (l1 ⊔ l2)
pr1 is-equivalence-injective-Prop = is-equivalence-injective P
pr2 is-equivalence-injective-Prop = is-prop-is-equivalence-injective
```
6 changes: 4 additions & 2 deletions src/group-theory/symmetric-groups.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -147,8 +147,10 @@ module _

iso-symmetric-group-equiv-Set :
iso-Group (symmetric-Group X) (symmetric-Group Y)
pr1 iso-symmetric-group-equiv-Set = hom-symmetric-group-equiv-Set
pr1 (pr2 iso-symmetric-group-equiv-Set) = hom-inv-symmetric-group-equiv-Set
pr1 iso-symmetric-group-equiv-Set =
hom-symmetric-group-equiv-Set
pr1 (pr2 iso-symmetric-group-equiv-Set) =
hom-inv-symmetric-group-equiv-Set
pr1 (pr2 (pr2 iso-symmetric-group-equiv-Set)) =
is-section-hom-inv-symmetric-group-equiv-Set
pr2 (pr2 (pr2 iso-symmetric-group-equiv-Set)) =
Expand Down
4 changes: 2 additions & 2 deletions src/univalent-combinatorics/double-counting.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -30,8 +30,8 @@ abstract
{l1 l2 : Level} {A : UU l1} {B : UU l2} (count-A : count A)
(count-B : count B) (e : A ≃ B)
Id (number-of-elements-count count-A) (number-of-elements-count count-B)
double-counting-equiv (pair k f) (pair l g) e =
is-injective-Fin ((inv-equiv g ∘e e) ∘e f)
double-counting-equiv (k , f) (l , g) e =
is-equivalence-injective-Fin (inv-equiv g ∘e e ∘e f)

abstract
double-counting :
Expand Down
Loading

0 comments on commit c339bac

Please sign in to comment.