{-# OPTIONS --cubical-compatible --safe #-}
module Univalence-axiom.Isomorphism-is-equality.More.Examples where
open import Equality.Propositional renaming (equality-with-J to eq)
open import Equivalence eq hiding (id)
open import Extensionality eq
open import Function-universe eq hiding (id)
open import H-level.Closure eq
open import Prelude hiding (id)
open import Univalence-axiom.Isomorphism-is-equality.More
magma : Code
magma = ε ▻ A-type ▻ N-ary [0] 2
Magma : Type₁
Magma = ⟦ magma ⟧
private
Magma-unfolded :
Magma ≡ Σ (Σ (↑ _ ⊤) λ _ →
Type ) λ { (_ , A) →
↑ _ A → ↑ _ A → ↑ _ A }
Magma-unfolded = refl
Isomorphic-magma-unfolded :
∀ {ass A₁ f₁ A₂ f₂} →
Isomorphic ass magma ((_ , A₁) , f₁) ((_ , A₂) , f₂) ≡
Σ (Σ (↑ _ ⊤) λ _ →
↑ _ (A₁ ≃ A₂) ) λ { (_ , lift A₁≃A₂) →
let open _≃_ (↑-cong A₁≃A₂) in
∀ x y → to (f₁ x y) ≡ f₂ (to x) (to y) }
Isomorphic-magma-unfolded = refl
semigroup : Code
semigroup =
ε
▻ A-type
▻ Is-a-set [0]
▻ N-ary (1+ [0]) 2
▻ Proposition
(λ { (_ , _∙_) →
∀ x y z → (x ∙ (y ∙ z)) ≡ ((x ∙ y) ∙ z) })
assoc-prop
where
assoc-prop = λ { ass ((_ , A-set) , _) →
let open Assumptions ass in
Π-closure ext₁ 1 λ _ →
Π-closure ext₁ 1 λ _ →
Π-closure ext₁ 1 λ _ →
A-set }
Semigroup : Type₁
Semigroup = ⟦ semigroup ⟧
private
Semigroup-unfolded :
Semigroup ≡ Σ (Σ (Σ (Σ (↑ _ ⊤) λ _ →
Type ) λ { (_ , A) →
Is-set (↑ _ A) }) λ { ((_ , A) , _) →
↑ _ A → ↑ _ A → ↑ _ A }) λ { (_ , _∙_) →
∀ x y z → (x ∙ (y ∙ z)) ≡ ((x ∙ y) ∙ z) }
Semigroup-unfolded = refl
Isomorphic-semigroup-unfolded :
∀ {ass A₁} {is₁ : Is-set (↑ _ A₁)} {_∙₁_ assoc₁}
{A₂} {is₂ : Is-set (↑ _ A₂)} {_∙₂_ assoc₂} →
Isomorphic ass semigroup ((((_ , A₁) , is₁) , _∙₁_) , assoc₁)
((((_ , A₂) , is₂) , _∙₂_) , assoc₂) ≡
Σ (Σ (Σ (Σ (↑ _ ⊤) λ _ →
↑ _ (A₁ ≃ A₂) ) λ { _ →
↑ _ ⊤ }) λ { ((_ , lift A₁≃A₂) , _) →
let open _≃_ (↑-cong A₁≃A₂) in
∀ x y → to (x ∙₁ y) ≡ (to x ∙₂ to y) }) λ { _ →
↑ _ ⊤ }
Isomorphic-semigroup-unfolded = refl
set-with-fixed-point-operator : Code
set-with-fixed-point-operator =
ε
▻ A-type
▻ Is-a-set [0]
▻ Simple ((base (1+ [0]) ⟶ base (1+ [0])) ⟶ base (1+ [0]))
▻ Proposition
(λ { (_ , fix) →
∀ f → fix f ≡ f (fix f) })
fix-point-prop
where
fix-point-prop = λ { ass ((_ , A-set) , _) →
let open Assumptions ass in
Π-closure ext₁ 1 λ _ →
A-set }
Set-with-fixed-point-operator : Type₁
Set-with-fixed-point-operator = ⟦ set-with-fixed-point-operator ⟧
private
Set-with-fixed-point-operator-unfolded :
Set-with-fixed-point-operator ≡ Σ (Σ (Σ (Σ (↑ _ ⊤) λ _ →
Type ) λ { (_ , A) →
Is-set (↑ _ A) }) λ { ((_ , A) , _) →
(↑ _ A → ↑ _ A) → ↑ _ A }) λ { (_ , fix) →
∀ f → fix f ≡ f (fix f) }
Set-with-fixed-point-operator-unfolded = refl
Isomorphic-set-with-fixed-point-operator-unfolded :
∀ {ass A₁} {is₁ : Is-set (↑ _ A₁)} {fix₁ fixed-point₁}
{A₂} {is₂ : Is-set (↑ _ A₂)} {fix₂ fixed-point₂} →
Isomorphic ass set-with-fixed-point-operator
((((_ , A₁) , is₁) , fix₁) , fixed-point₁)
((((_ , A₂) , is₂) , fix₂) , fixed-point₂) ≡
Σ (Σ (Σ (Σ (↑ _ ⊤) λ _ →
↑ _ (A₁ ≃ A₂) ) λ { _ →
↑ _ ⊤ }) λ { ((_ , lift A₁≃A₂) , _) →
let open _≃_ (↑-cong A₁≃A₂) in
∀ f g →
(∀ x y → to x ≡ y → to (f x) ≡ g y) →
to (fix₁ f) ≡ fix₂ g }) λ { _ →
↑ _ ⊤ }
Isomorphic-set-with-fixed-point-operator-unfolded = refl
abelian-group : Code
abelian-group =
ε
▻ A-type
▻ Is-a-set [0]
▻ N-ary (1+ [0]) 2
▻ Comm
▻ Assoc
▻ N-ary (1+ 1+ 1+ 1+ [0]) 0
▻ Left-identity
▻ Right-identity
▻ N-ary (1+ 1+ 1+ 1+ 1+ 1+ 1+ [0]) 1
▻ Left-inverse
▻ Right-inverse
where
Comm = Proposition
(λ { (_ , _∙_) →
∀ x y → (x ∙ y) ≡ (y ∙ x) })
(λ { ass ((_ , A-set) , _) →
let open Assumptions ass in
Π-closure ext₁ 1 λ _ →
Π-closure ext₁ 1 λ _ →
A-set
})
Assoc = Proposition
(λ { ((_ , _∙_) , _) →
∀ x y z → (x ∙ (y ∙ z)) ≡ ((x ∙ y) ∙ z) })
(λ { ass (((_ , A-set) , _) , _) →
let open Assumptions ass in
Π-closure ext₁ 1 λ _ →
Π-closure ext₁ 1 λ _ →
Π-closure ext₁ 1 λ _ →
A-set
})
Left-identity = Proposition
(λ { ((((_ , _∙_) , _) , _) , e) →
∀ x → (e ∙ x) ≡ x })
(λ { ass (((((_ , A-set) , _) , _) , _) , _) →
let open Assumptions ass in
Π-closure ext₁ 1 λ _ →
A-set
})
Right-identity = Proposition
(λ { (((((_ , _∙_) , _) , _) , e) , _) →
∀ x → (x ∙ e) ≡ x })
(λ { ass ((((((_ , A-set) , _) , _) , _) , _) , _) →
let open Assumptions ass in
Π-closure ext₁ 1 λ _ →
A-set
})
Left-inverse = Proposition
(λ { (((((((_ , _∙_) , _) , _) , e) , _) , _) , _⁻¹) →
∀ x → ((x ⁻¹) ∙ x) ≡ e })
(λ { ass ((((((((_ , A-set) , _) , _) , _) , _) , _) , _) , _) →
let open Assumptions ass in
Π-closure ext₁ 1 λ _ →
A-set
})
Right-inverse = Proposition
(λ { ((((((((_ , _∙_) , _) , _) , e) , _) , _) , _⁻¹) , _) →
∀ x → (x ∙ (x ⁻¹)) ≡ e })
(λ { ass (((((((((_ , A-set) , _) , _) , _) , _) , _) , _) , _) , _) →
let open Assumptions ass in
Π-closure ext₁ 1 λ _ →
A-set
})
Abelian-group : Type₁
Abelian-group = ⟦ abelian-group ⟧
private
Abelian-group-unfolded :
Abelian-group ≡ Σ (Σ (Σ (Σ (Σ (Σ (Σ (Σ (Σ (Σ (Σ (↑ _ ⊤) λ _ →
Type ) λ { (_ , A) →
Is-set (↑ _ A) }) λ { ((_ , A) , _) →
↑ _ A → ↑ _ A → ↑ _ A }) λ { (_ , _∙_) →
∀ x y → (x ∙ y) ≡ (y ∙ x) }) λ { ((_ , _∙_) , _) →
∀ x y z → (x ∙ (y ∙ z)) ≡ ((x ∙ y) ∙ z) }) λ { (((((_ , A) , _) , _ ) , _) , _) →
↑ _ A }) λ { ((((_ , _∙_) , _) , _) , e) →
∀ x → (e ∙ x) ≡ x }) λ { (((((_ , _∙_) , _) , _) , e) , _) →
∀ x → (x ∙ e) ≡ x }) λ { ((((((((_ , A) , _) , _ ) , _) , _) , _) , _) , _) →
↑ _ A → ↑ _ A }) λ { (((((((_ , _∙_) , _) , _) , e) , _) , _) , _⁻¹) →
∀ x → ((x ⁻¹) ∙ x) ≡ e }) λ { ((((((((_ , _∙_) , _) , _) , e) , _) , _) , _⁻¹) , _) →
∀ x → (x ∙ (x ⁻¹)) ≡ e }
Abelian-group-unfolded = refl
Isomorphic-abelian-group-unfolded :
∀ {ass A₁} {is₁ : Is-set (↑ _ A₁)}
{_∙₁_ comm₁ assoc₁ e₁ lid₁ rid₁ _⁻¹₁ linv₁ rinv₁}
{A₂} {is₂ : Is-set (↑ _ A₂)}
{_∙₂_ comm₂ assoc₂ e₂ lid₂ rid₂ _⁻¹₂ linv₂ rinv₂} →
Isomorphic ass abelian-group
(((((((((((_ , A₁) , is₁) , _∙₁_) , comm₁) ,
assoc₁) , e₁) , lid₁) , rid₁) , _⁻¹₁) , linv₁) , rinv₁)
(((((((((((_ , A₂) , is₂) , _∙₂_) , comm₂) ,
assoc₂) , e₂) , lid₂) , rid₂) , _⁻¹₂) , linv₂) , rinv₂) ≡
Σ (Σ (Σ (Σ (Σ (Σ (Σ (Σ (Σ (Σ (Σ (↑ _ ⊤) λ _ →
↑ _ (A₁ ≃ A₂) ) λ { _ →
↑ _ ⊤ }) λ { ((_ , lift A₁≃A₂) , _) →
let open _≃_ (↑-cong A₁≃A₂) in
∀ x y → to (x ∙₁ y) ≡ (to x ∙₂ to y) }) λ { _ →
↑ _ ⊤ }) λ { _ →
↑ _ ⊤ }) λ { (((((_ , lift A₁≃A₂) , _) , _) , _) , _) →
let open _≃_ (↑-cong A₁≃A₂) in
to e₁ ≡ e₂ }) λ { _ →
↑ _ ⊤ }) λ { _ →
↑ _ ⊤ }) λ { ((((((((_ , lift A₁≃A₂) , _) , _) , _) , _) , _) , _) , _) →
let open _≃_ (↑-cong A₁≃A₂) in
∀ x → to (x ⁻¹₁) ≡ (to x ⁻¹₂) }) λ { _ →
↑ _ ⊤ }) λ { _ →
↑ _ ⊤ }
Isomorphic-abelian-group-unfolded = refl
Nat : Type₁
Nat = (A : Type) → ↑ (# 1) A → (↑ (# 1) A → ↑ (# 1) A) → ↑ (# 1) A
Zero : Nat
Zero = λ A z s → z
Suc : Nat → Nat
Suc = λ n A z s → s (n A z s)
inductive-natural-numbers : Code
inductive-natural-numbers =
ε
▻ Dep (Π set (Π (base ⟨0⟩)
(Π (Π (base (1+ ⟨0⟩)) (base (1+ 1+ ⟨0⟩)))
(base (1+ 1+ ⟨0⟩)))))
▻ Proposition
(λ { (_ , n) →
(P : Nat → Type) →
Is-proposition (P n) →
P Zero →
(∀ m → P m → P (Suc m)) →
P n })
(λ ass _ →
let open Assumptions ass in
Π-closure ext₁ 1 λ _ →
Π-closure (lower-extensionality (# 1) (# 0) ext₁) 1 λ Pn-prop →
Π-closure (lower-extensionality (# 1) (# 0) ext₁) 1 λ _ →
Π-closure (lower-extensionality (# 0) (# 1) ext₁) 1 λ _ →
Pn-prop)
where open Dependent
private
⟦inductive-natural-numbers⟧ :
⟦ inductive-natural-numbers ⟧
≡
Σ (Σ (↑ _ ⊤) λ _ →
Nat ) λ { (_ , n) →
(P : Nat → Type) →
Is-proposition (P n) →
P Zero →
(∀ m → P m → P (Suc m)) →
P n }
⟦inductive-natural-numbers⟧ = refl
Isomorphic-inductive-natural-numbers :
∀ {ass : Assumptions}
{n₁ n₂ : Nat}
{prop₁ : (P : Nat → Type) → Is-proposition (P n₁) →
P Zero → (∀ m → P m → P (Suc m)) → P n₁}
{prop₂ : (P : Nat → Type) → Is-proposition (P n₂) →
P Zero → (∀ m → P m → P (Suc m)) → P n₂} →
Isomorphic ass inductive-natural-numbers
((_ , n₁) , prop₁) ((_ , n₂) , prop₂)
≡
Σ (Σ (↑ (# 1) ⊤) λ _ →
((A₁ A₂ : Type) → (A₁≃A₂ : ↑ (# 1) (A₁ ≃ A₂)) →
let cast = _≃_.from (↑-cong (lower A₁≃A₂)) in
(z₁ : ↑ (# 1) A₁) (z₂ : ↑ (# 1) A₂) →
z₁ ≡ cast z₂ →
(s₁ : ↑ (# 1) A₁ → ↑ (# 1) A₁) (s₂ : ↑ (# 1) A₂ → ↑ (# 1) A₂) →
(∀ n₁ n₂ → n₁ ≡ cast n₂ → s₁ n₁ ≡ cast (s₂ n₂)) →
n₁ A₁ z₁ s₁ ≡ cast (n₂ A₂ z₂ s₂))) λ _ →
↑ (# 1) ⊤
Isomorphic-inductive-natural-numbers = refl