{-# OPTIONS --cubical-compatible --safe #-}
open import Equality
open import Prelude hiding (id; proj₁; proj₂)
module Records-with-with
{c⁺}
(eq : ∀ {a p} → Equality-with-J a p c⁺)
(open Derived-definitions-and-properties eq)
(Label : Type)
(_≟_ : Decidable-equality Label)
where
open import Bijection eq using (_↔_; ↑↔)
open import Function-universe eq hiding (_∘_)
open import List eq using (foldr)
infix 4 _,
record Manifest-Σ {a b} (A : Type a) {B : A → Type b}
(f : (x : A) → B x) : Type a where
constructor _,
field proj₁ : A
proj₂ : B proj₁
proj₂ = f proj₁
mutual
infixl 5 _,_∶_ _,_≔_
data Signature s : Type (lsuc s) where
∅ : Signature s
_,_∶_ : (Sig : Signature s)
(ℓ : Label)
(A : Record Sig → Type s) →
Signature s
_,_≔_ : (Sig : Signature s)
(ℓ : Label)
{A : Record Sig → Type s}
(a : (r : Record Sig) → A r) →
Signature s
record Record {s} (Sig : Signature s) : Type s where
eta-equality
inductive
constructor rec
field fun : Record-fun Sig
Record-fun : ∀ {s} → Signature s → Type s
Record-fun ∅ = ↑ _ ⊤
Record-fun (Sig , ℓ ∶ A) = Σ (Record Sig) A
Record-fun (Sig , ℓ ≔ a) = Manifest-Σ (Record Sig) a
labels : ∀ {s} → Signature s → List Label
labels ∅ = []
labels (Sig , ℓ ∶ A) = ℓ ∷ labels Sig
labels (Sig , ℓ ≔ a) = ℓ ∷ labels Sig
infix 4 _∈_
_∈_ : ∀ {s} → Label → Signature s → Type
ℓ ∈ Sig =
foldr (λ ℓ′ → if ℓ ≟ ℓ′ then (λ _ → ⊤) else id)
⊥
(labels Sig)
Restrict : ∀ {s} (Sig : Signature s) (ℓ : Label) → ℓ ∈ Sig →
Signature s
Restrict ∅ ℓ ()
Restrict (Sig , ℓ′ ∶ A) ℓ ℓ∈ with ℓ ≟ ℓ′
... | yes _ = Sig
... | no _ = Restrict Sig ℓ ℓ∈
Restrict (Sig , ℓ′ ≔ a) ℓ ℓ∈ with ℓ ≟ ℓ′
... | yes _ = Sig
... | no _ = Restrict Sig ℓ ℓ∈
Restricted : ∀ {s} (Sig : Signature s) (ℓ : Label) → ℓ ∈ Sig → Type s
Restricted Sig ℓ ℓ∈ = Record (Restrict Sig ℓ ℓ∈)
Proj : ∀ {s} (Sig : Signature s) (ℓ : Label) (ℓ∈ : ℓ ∈ Sig) →
Restricted Sig ℓ ℓ∈ → Type s
Proj ∅ ℓ ()
Proj (Sig , ℓ′ ∶ A) ℓ ℓ∈ with ℓ ≟ ℓ′
... | yes _ = A
... | no _ = Proj Sig ℓ ℓ∈
Proj (_,_≔_ Sig ℓ′ {A} a) ℓ ℓ∈ with ℓ ≟ ℓ′
... | yes _ = A
... | no _ = Proj Sig ℓ ℓ∈
infixl 5 _∣_
_∣_ : ∀ {s} {Sig : Signature s} → Record Sig →
(ℓ : Label) {ℓ∈ : ℓ ∈ Sig} → Restricted Sig ℓ ℓ∈
_∣_ {Sig = ∅} r ℓ {}
_∣_ {Sig = Sig , ℓ′ ∶ A} (rec r) ℓ {ℓ∈} with ℓ ≟ ℓ′
... | yes _ = Σ.proj₁ r
... | no _ = _∣_ (Σ.proj₁ r) ℓ {ℓ∈}
_∣_ {Sig = Sig , ℓ′ ≔ a} (rec r) ℓ {ℓ∈} with ℓ ≟ ℓ′
... | yes _ = Manifest-Σ.proj₁ r
... | no _ = _∣_ (Manifest-Σ.proj₁ r) ℓ {ℓ∈}
infixl 5 _·_
_·_ : ∀ {s} {Sig : Signature s} (r : Record Sig)
(ℓ : Label) {ℓ∈ : ℓ ∈ Sig} →
Proj Sig ℓ ℓ∈ (r ∣ ℓ)
_·_ {Sig = ∅} r ℓ {}
_·_ {Sig = Sig , ℓ′ ∶ A} (rec r) ℓ {ℓ∈} with ℓ ≟ ℓ′
... | yes _ = Σ.proj₂ r
... | no _ = _·_ (Σ.proj₁ r) ℓ {ℓ∈}
_·_ {Sig = Sig , ℓ′ ≔ a} (rec r) ℓ {ℓ∈} with ℓ ≟ ℓ′
... | yes _ = Manifest-Σ.proj₂ r
... | no _ = _·_ (Manifest-Σ.proj₁ r) ℓ {ℓ∈}
mutual
infixl 5 _With_≔_
_With_≔_ : ∀ {s} (Sig : Signature s) (ℓ : Label) {ℓ∈ : ℓ ∈ Sig} →
((r : Restricted Sig ℓ ℓ∈) → Proj Sig ℓ ℓ∈ r) → Signature s
_With_≔_ ∅ ℓ {} a
_With_≔_ (Sig , ℓ′ ∶ A) ℓ {ℓ∈} a with ℓ ≟ ℓ′
... | yes _ = Sig , ℓ′ ≔ a
... | no _ = _With_≔_ Sig ℓ {ℓ∈} a , ℓ′ ∶ A ∘ drop-With
_With_≔_ (Sig , ℓ′ ≔ a′) ℓ {ℓ∈} a with ℓ ≟ ℓ′
... | yes _ = Sig , ℓ′ ≔ a
... | no _ = _With_≔_ Sig ℓ {ℓ∈} a , ℓ′ ≔ a′ ∘ drop-With
drop-With : ∀ {s} {Sig : Signature s} {ℓ : Label} {ℓ∈ : ℓ ∈ Sig}
{a : (r : Restricted Sig ℓ ℓ∈) → Proj Sig ℓ ℓ∈ r} →
Record (_With_≔_ Sig ℓ {ℓ∈} a) → Record Sig
drop-With {Sig = ∅} {ℓ∈ = ()} r
drop-With {Sig = Sig , ℓ′ ∶ A} {ℓ} (rec r) with ℓ ≟ ℓ′
... | yes _ = rec (Manifest-Σ.proj₁ r , Manifest-Σ.proj₂ r)
... | no _ = rec (drop-With (Σ.proj₁ r) , Σ.proj₂ r)
drop-With {Sig = Sig , ℓ′ ≔ a} {ℓ} (rec r) with ℓ ≟ ℓ′
... | yes _ = rec (Manifest-Σ.proj₁ r ,)
... | no _ = rec (drop-With (Manifest-Σ.proj₁ r) ,)
Recordʳ : ∀ {s} (Sig : Signature s) → (Record Sig → Type s) → Type s
Recordʳ ∅ κ = κ _
Recordʳ (Sig , ℓ ∶ A) κ = Recordʳ Sig (λ r → Σ (A r) (κ ∘ rec ∘ (r ,_)))
Recordʳ (Sig , ℓ ≔ a) κ = Recordʳ Sig (λ r → κ (rec (r ,)))
Manifest-Σ↔ :
∀ {a b} {A : Type a} {B : A → Type b} {f : (x : A) → B x} →
Manifest-Σ A f ↔ A
Manifest-Σ↔ = record
{ surjection = record
{ logical-equivalence = record
{ to = Manifest-Σ.proj₁
; from = _,
}
; right-inverse-of = λ _ → refl _
}
; left-inverse-of = λ _ → refl _
}
Record↔Record-fun :
∀ {s} {Sig : Signature s} → Record Sig ↔ Record-fun Sig
Record↔Record-fun = record
{ surjection = record
{ logical-equivalence = record { to = Record.fun ; from = rec }
; right-inverse-of = λ _ → refl _
}
; left-inverse-of = λ _ → refl _
}
mutual
Σ-Record↔Recordʳ :
∀ {s} (Sig : Signature s) (κ : Record Sig → Type s) →
Σ (Record Sig) κ ↔ Recordʳ Sig κ
Σ-Record↔Recordʳ Sig κ =
Σ (Record Sig) κ ↝⟨ Σ-cong Record↔Record-fun (λ _ → id) ⟩
Σ (Record-fun Sig) (κ ∘ rec) ↝⟨ Σ-Record-fun↔Recordʳ Sig κ ⟩□
Recordʳ Sig κ □
Σ-Record-fun↔Recordʳ :
∀ {s} (Sig : Signature s) (κ : Record Sig → Type s) →
Σ (Record-fun Sig) (κ ∘ rec) ↔ Recordʳ Sig κ
Σ-Record-fun↔Recordʳ ∅ κ =
Σ (↑ _ ⊤) (κ ∘ rec) ↝⟨ Σ-cong ↑↔ (λ _ → id) ⟩
Σ ⊤ (κ ∘ rec ∘ lift) ↝⟨ Σ-left-identity ⟩□
κ _ □
Σ-Record-fun↔Recordʳ (Sig , ℓ ∶ A) κ =
Σ (Σ (Record Sig) A) (κ ∘ rec) ↝⟨ inverse Σ-assoc ⟩
Σ (Record Sig) (λ r → Σ (A r) (κ ∘ rec ∘ (r ,_))) ↝⟨ Σ-Record↔Recordʳ Sig _ ⟩□
Recordʳ Sig (λ r → Σ (A r) (κ ∘ rec ∘ (r ,_))) □
Σ-Record-fun↔Recordʳ (Sig , ℓ ≔ a) κ =
Σ (Manifest-Σ (Record Sig) a) (κ ∘ rec) ↝⟨ Σ-cong Manifest-Σ↔ (λ _ → id) ⟩
Σ (Record Sig) (κ ∘ rec ∘ _,) ↝⟨ Σ-Record↔Recordʳ Sig _ ⟩□
Recordʳ Sig (κ ∘ rec ∘ _,) □
Record↔Recordʳ :
∀ {s} (Sig : Signature s) →
Record Sig ↔ Recordʳ Sig (λ _ → ↑ s ⊤)
Record↔Recordʳ Sig =
Record Sig ↝⟨ inverse ×-right-identity ⟩
Record Sig × ⊤ ↝⟨ id ×-cong inverse ↑↔ ⟩
Record Sig × ↑ _ ⊤ ↝⟨ Σ-Record↔Recordʳ Sig _ ⟩□
Recordʳ Sig (λ _ → ↑ _ ⊤) □
Recʳ : ∀ {s} → Signature s → Type s
Recʳ ∅ = ↑ _ ⊤
Recʳ (Sig , ℓ ∶ A) = Recordʳ Sig A
Recʳ (Sig , ℓ ≔ a) = Recʳ Sig
mutual
Record↔Recʳ :
∀ {s} {Sig : Signature s} →
Record Sig ↔ Recʳ Sig
Record↔Recʳ {Sig} =
Record Sig ↝⟨ Record↔Record-fun ⟩
Record-fun Sig ↝⟨ Record-fun↔Recʳ Sig ⟩□
Recʳ Sig □
Record-fun↔Recʳ :
∀ {s} (Sig : Signature s) →
Record-fun Sig ↔ Recʳ Sig
Record-fun↔Recʳ ∅ = ↑ _ ⊤ □
Record-fun↔Recʳ (Sig , ℓ ∶ A) =
Σ (Record Sig) A ↝⟨ Σ-Record↔Recordʳ Sig A ⟩□
Recordʳ Sig A □
Record-fun↔Recʳ (Sig , ℓ ≔ a) =
Manifest-Σ (Record Sig) a ↝⟨ Manifest-Σ↔ ⟩
Record Sig ↝⟨ Record↔Recʳ ⟩□
Recʳ Sig □