text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.Maybe.Properties where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Empty
open import Cubical.Data.Unit
open import Cubical.Data.Nat
open import Cubical.Relation.Nullary
open import Cubical.Data.Sum

open import Cubical.Data.Maybe.Base

-- Path space of Maybe type
module MaybePath {ℓ} {A : Type ℓ} where
  Cover : Maybe A → Maybe A → Type ℓ
  Cover nothing  nothing   = Lift Unit
  Cover nothing  (just _)  = Lift ⊥
  Cover (just _) nothing   = Lift ⊥
  Cover (just a) (just a') = a ≡ a'

  reflCode : (c : Maybe A) → Cover c c
  reflCode nothing  = lift tt
  reflCode (just b) = refl

  encode : ∀ c c' → c ≡ c' → Cover c c'
  encode c _ = J (λ c' _ → Cover c c') (reflCode c)

  encodeRefl : ∀ c → encode c c refl ≡ reflCode c
  encodeRefl c = JRefl (λ c' _ → Cover c c') (reflCode c)

  decode : ∀ c c' → Cover c c' → c ≡ c'
  decode nothing  nothing  _ = refl
  decode (just _) (just _) p = cong just p

  decodeRefl : ∀ c → decode c c (reflCode c) ≡ refl
  decodeRefl nothing  = refl
  decodeRefl (just _) = refl

  decodeEncode : ∀ c c' → (p : c ≡ c') → decode c c' (encode c c' p) ≡ p
  decodeEncode c _ =
    J (λ c' p → decode c c' (encode c c' p) ≡ p)
      (cong (decode c c) (encodeRefl c) ∙ decodeRefl c)

  isOfHLevelCover : (n : ℕ)
    → isOfHLevel (suc (suc n)) A
    → ∀ c c' → isOfHLevel (suc n) (Cover c c')
  isOfHLevelCover n p nothing  nothing   = isOfHLevelLift (suc n) (isOfHLevelUnit (suc n))
  isOfHLevelCover n p nothing  (just a') = isOfHLevelLift (suc n)
    (subst (λ m → isOfHLevel m ⊥) (+-comm n 1) (hLevelLift n isProp⊥))
  isOfHLevelCover n p (just a) nothing   = isOfHLevelLift (suc n)
    (subst (λ m → isOfHLevel m ⊥) (+-comm n 1) (hLevelLift n isProp⊥))
  isOfHLevelCover n p (just a) (just a') = p a a'

isOfHLevelMaybe : ∀ {ℓ} (n : ℕ) {A : Type ℓ}
  → isOfHLevel (suc (suc n)) A
  → isOfHLevel (suc (suc n)) (Maybe A)
isOfHLevelMaybe n lA c c' =
  retractIsOfHLevel (suc n)
    (MaybePath.encode c c')
    (MaybePath.decode c c')
    (MaybePath.decodeEncode c c')
    (MaybePath.isOfHLevelCover n lA c c')

private
 variable
   ℓ : Level
   A : Type ℓ

fromJust-def : A → Maybe A → A
fromJust-def a nothing = a
fromJust-def _ (just a) = a

just-inj : (x y : A) → just x ≡ just y → x ≡ y
just-inj x _ eq = cong (fromJust-def x) eq

¬nothing≡just : ∀ {x : A} → ¬ (nothing ≡ just x)
¬nothing≡just {A = A} {x = x} p = lower (subst (caseMaybe (Maybe A) (Lift ⊥)) p (just x))

¬just≡nothing : ∀ {x : A} → ¬ (just x ≡ nothing)
¬just≡nothing {A = A} {x = x} p = lower (subst (caseMaybe (Lift ⊥) (Maybe A)) p (just x))

discreteMaybe : Discrete A → Discrete (Maybe A)
discreteMaybe eqA nothing nothing    = yes refl
discreteMaybe eqA nothing (just a')  = no ¬nothing≡just
discreteMaybe eqA (just a) nothing   = no ¬just≡nothing
discreteMaybe eqA (just a) (just a') with eqA a a'
... | yes p = yes (cong just p)
... | no ¬p = no (λ p → ¬p (just-inj _ _ p))

module SumUnit where
  Maybe→SumUnit : Maybe A → Unit ⊎ A
  Maybe→SumUnit nothing  = inl tt
  Maybe→SumUnit (just a) = inr a

  SumUnit→Maybe : Unit ⊎ A → Maybe A
  SumUnit→Maybe (inl _) = nothing
  SumUnit→Maybe (inr a) = just a

  Maybe→SumUnit→Maybe : (x : Maybe A) → SumUnit→Maybe (Maybe→SumUnit x) ≡ x
  Maybe→SumUnit→Maybe nothing  = refl
  Maybe→SumUnit→Maybe (just _) = refl

  SumUnit→Maybe→SumUnit : (x : Unit ⊎ A) → Maybe→SumUnit (SumUnit→Maybe x) ≡ x
  SumUnit→Maybe→SumUnit (inl _) = refl
  SumUnit→Maybe→SumUnit (inr _) = refl

Maybe≡SumUnit : Maybe A ≡ Unit ⊎ A
Maybe≡SumUnit = isoToPath (iso SumUnit.Maybe→SumUnit SumUnit.SumUnit→Maybe SumUnit.SumUnit→Maybe→SumUnit SumUnit.Maybe→SumUnit→Maybe)

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
{-# OPTIONS --safe #-}

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Weakening {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped as U hiding (wk)
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Weakening as T hiding (wk; wkEq; wkTerm; wkEqTerm)
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Irrelevance

open import Tools.Product
import Tools.PropositionalEquality as PE

import Data.Nat as Nat

-- Weakening of neutrals in WHNF

wkTermNe : ∀ {ρ Γ Δ k A rA} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ)
         → Γ ⊩neNf k ∷ A ^ rA → Δ ⊩neNf U.wk ρ k ∷ U.wk ρ A ^ rA
wkTermNe {ρ} [ρ] ⊢Δ (neNfₜ neK ⊢k k≡k) =
  neNfₜ (wkNeutral ρ neK) (T.wkTerm [ρ] ⊢Δ ⊢k) (~-wk [ρ] ⊢Δ k≡k)

wkEqTermNe : ∀ {ρ Γ Δ k k′ A rA} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ)
           → Γ ⊩neNf k ≡ k′ ∷ A ^ rA → Δ ⊩neNf U.wk ρ k ≡ U.wk ρ k′ ∷ U.wk ρ A ^ rA
wkEqTermNe {ρ} [ρ] ⊢Δ (neNfₜ₌ neK neM k≡m) =
  neNfₜ₌ (wkNeutral ρ neK) (wkNeutral ρ neM) (~-wk [ρ] ⊢Δ k≡m)

-- Weakening of reducible natural numbers

mutual
  wkTermℕ : ∀ {ρ Γ Δ n} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ)
          → Γ ⊩ℕ n ∷ℕ → Δ ⊩ℕ U.wk ρ n ∷ℕ
  wkTermℕ {ρ} [ρ] ⊢Δ (ℕₜ n d n≡n prop) =
    ℕₜ (U.wk ρ n) (wkRed:*:Term [ρ] ⊢Δ d)
       (≅ₜ-wk [ρ] ⊢Δ n≡n)
       (wkNatural-prop [ρ] ⊢Δ prop)

  wkNatural-prop : ∀ {ρ Γ Δ n} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ)
                 → Natural-prop Γ n
                 → Natural-prop Δ (U.wk ρ n)
  wkNatural-prop ρ ⊢Δ (sucᵣ n) = sucᵣ (wkTermℕ ρ ⊢Δ n)
  wkNatural-prop ρ ⊢Δ zeroᵣ = zeroᵣ
  wkNatural-prop ρ ⊢Δ (ne nf) = ne (wkTermNe ρ ⊢Δ nf)

mutual
  wkEqTermℕ : ∀ {ρ Γ Δ t u} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ)
            → Γ ⊩ℕ t ≡ u ∷ℕ
            → Δ ⊩ℕ U.wk ρ t ≡ U.wk ρ u ∷ℕ
  wkEqTermℕ {ρ} [ρ] ⊢Δ (ℕₜ₌ k k′ d d′ t≡u prop) =
    ℕₜ₌ (U.wk ρ k) (U.wk ρ k′) (wkRed:*:Term [ρ] ⊢Δ d)
        (wkRed:*:Term [ρ] ⊢Δ d′) (≅ₜ-wk [ρ] ⊢Δ t≡u)
        (wk[Natural]-prop [ρ] ⊢Δ prop)

  wk[Natural]-prop : ∀ {ρ Γ Δ n n′} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ)
                   → [Natural]-prop Γ n n′
                   → [Natural]-prop Δ (U.wk ρ n) (U.wk ρ n′)
  wk[Natural]-prop ρ ⊢Δ (sucᵣ [n≡n′]) = sucᵣ (wkEqTermℕ ρ ⊢Δ [n≡n′])
  wk[Natural]-prop ρ ⊢Δ zeroᵣ = zeroᵣ
  wk[Natural]-prop ρ ⊢Δ (ne x) = ne (wkEqTermNe ρ ⊢Δ x)

-- Empty
wkTermEmpty : ∀ {ρ Γ Δ l n} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ)
  → Γ ⊩Empty n ∷Empty^ l → Δ ⊩Empty U.wk ρ n ∷Empty^ l
wkTermEmpty {ρ} [ρ] ⊢Δ (Emptyₜ (ne d)) = Emptyₜ (ne (T.wkTerm [ρ] ⊢Δ d))

wk[Empty]-prop : ∀ {ρ Γ Δ n l n′} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ)
  → [Empty]-prop Γ n n′ l
  → [Empty]-prop Δ (U.wk ρ n) (U.wk ρ n′) l
wk[Empty]-prop {ρ} [ρ] ⊢Δ (ne d d') = ne (T.wkTerm [ρ] ⊢Δ d) (T.wkTerm [ρ] ⊢Δ d')

wkEqTermEmpty : ∀ {ρ Γ Δ t u l } → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ)
  → Γ ⊩Empty t ≡ u ∷Empty^ l
  → Δ ⊩Empty U.wk ρ t ≡ U.wk ρ u ∷Empty^ l
wkEqTermEmpty {ρ} [ρ] ⊢Δ (Emptyₜ₌ (ne d d')) = Emptyₜ₌ (ne (T.wkTerm [ρ] ⊢Δ d) (T.wkTerm [ρ] ⊢Δ d'))

-- Weakening of the logical relation

wk : ∀ {ρ Γ Δ A rA l} → ρ ∷ Δ ⊆ Γ → ⊢ Δ → Γ ⊩⟨ l ⟩ A ^ rA → Δ ⊩⟨ l ⟩ U.wk ρ A ^ rA
wk ρ ⊢Δ (Uᵣ (Uᵣ r l′ l< eq d)) = Uᵣ (Uᵣ r l′ l< eq (wkRed:*: ρ ⊢Δ d))
wk ρ ⊢Δ (ℕᵣ D) = ℕᵣ (wkRed:*: ρ ⊢Δ D)
wk ρ ⊢Δ (Emptyᵣ D) = Emptyᵣ (wkRed:*: ρ ⊢Δ D)
wk {ρ} [ρ] ⊢Δ (ne′ K D neK K≡K) =
  ne′ (U.wk ρ K) (wkRed:*: [ρ] ⊢Δ D) (wkNeutral ρ neK) (~-wk [ρ] ⊢Δ K≡K)
wk {ρ} {Γ} {Δ} {A} {rA} {l} [ρ] ⊢Δ (Πᵣ′ rF lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext) =
  let ⊢ρF = T.wk [ρ] ⊢Δ ⊢F
      iF = [ rF , ι lF ]
      iG = [ TypeInfo.r rA , ι lG ]
      [F]′ : ∀ {ρ ρ′ E} ([ρ] : ρ ∷ E ⊆ Δ) ([ρ′] : ρ′ ∷ Δ ⊆ Γ) (⊢E : ⊢ E)
           → E ⊩⟨ l ⟩ U.wk ρ (U.wk ρ′ F) ^ iF
      [F]′ {ρ} {ρ′} [ρ] [ρ′] ⊢E = irrelevance′
                              (PE.sym (wk-comp ρ ρ′ F))
                              ([F] ([ρ] •ₜ [ρ′]) ⊢E)
      [a]′ : ∀ {ρ ρ′ E a} ([ρ] : ρ ∷ E ⊆ Δ) ([ρ′] : ρ′ ∷ Δ ⊆ Γ) (⊢E : ⊢ E)
             ([a] : E ⊩⟨ l ⟩ a ∷ U.wk ρ (U.wk ρ′ F) ^ iF / [F]′ [ρ] [ρ′] ⊢E)
           → E ⊩⟨ l ⟩ a ∷ U.wk (ρ • ρ′) F ^ iF / [F] ([ρ] •ₜ [ρ′]) ⊢E
      [a]′ {ρ} {ρ′} [ρ] [ρ′] ⊢E [a] = irrelevanceTerm′ (wk-comp ρ ρ′ F) PE.refl PE.refl
                                          ([F]′ [ρ] [ρ′] ⊢E) ([F] ([ρ] •ₜ [ρ′]) ⊢E) [a]
      [G]′ : ∀ {ρ ρ′ E a} ([ρ] : ρ ∷ E ⊆ Δ) ([ρ′] : ρ′ ∷ Δ ⊆ Γ) (⊢E : ⊢ E)
             ([a] : E ⊩⟨ l ⟩ a ∷ U.wk ρ (U.wk ρ′ F) ^ iF / [F]′ [ρ] [ρ′] ⊢E)
           → E ⊩⟨ l ⟩ U.wk (lift (ρ • ρ′)) G [ a ] ^ iG
      [G]′ η η′ ⊢E [a] = [G] (η •ₜ η′) ⊢E ([a]′ η η′ ⊢E [a])
  in  Πᵣ′ rF lF lG lF≤ lG≤ (U.wk ρ F) (U.wk (lift ρ) G) (T.wkRed:*: [ρ] ⊢Δ D) ⊢ρF
           (T.wk (lift [ρ]) (⊢Δ ∙ ⊢ρF) ⊢G)
           (≅-wk [ρ] ⊢Δ A≡A)
           (λ {ρ₁} [ρ₁] ⊢Δ₁ → irrelevance′ (PE.sym (wk-comp ρ₁ ρ F))
                                    ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁))
           (λ {ρ₁} [ρ₁] ⊢Δ₁ [a] → irrelevance′ (wk-comp-subst ρ₁ ρ G)
                                        ([G]′ [ρ₁] [ρ] ⊢Δ₁ [a]))
           (λ {ρ₁} [ρ₁] ⊢Δ₁ [a] [b] [a≡b] →
              let [a≡b]′ = irrelevanceEqTerm′ (wk-comp ρ₁ ρ F) PE.refl PE.refl
                                              ([F]′ [ρ₁] [ρ] ⊢Δ₁)
                                              ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁)
                                              [a≡b]
              in  irrelevanceEq″ (wk-comp-subst ρ₁ ρ G)
                                  (wk-comp-subst ρ₁ ρ G) PE.refl PE.refl
                                  ([G]′ [ρ₁] [ρ] ⊢Δ₁ [a])
                                  (irrelevance′
                                            (wk-comp-subst ρ₁ ρ G)
                                            ([G]′ [ρ₁] [ρ] ⊢Δ₁ [a]))
                                  (G-ext ([ρ₁] •ₜ [ρ]) ⊢Δ₁
                                         ([a]′ [ρ₁] [ρ] ⊢Δ₁ [a])
                                         ([a]′ [ρ₁] [ρ] ⊢Δ₁ [b])
                                         [a≡b]′))
wk {ρ} {Γ} {Δ} {A} {rA} {l} [ρ] ⊢Δ (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) =
  let ⊢ρF = T.wk [ρ] ⊢Δ ⊢F
      iF = [ % , TypeInfo.l rA ]
      [F]′ : ∀ {ρ ρ′ E} ([ρ] : ρ ∷ E ⊆ Δ) ([ρ′] : ρ′ ∷ Δ ⊆ Γ) (⊢E : ⊢ E)
           → E ⊩⟨ l ⟩ U.wk ρ (U.wk ρ′ F) ^ iF
      [F]′ {ρ} {ρ′} [ρ] [ρ′] ⊢E = irrelevance′
                              (PE.sym (wk-comp ρ ρ′ F))
                              ([F] ([ρ] •ₜ [ρ′]) ⊢E)
      [a]′ : ∀ {ρ ρ′ E a} ([ρ] : ρ ∷ E ⊆ Δ) ([ρ′] : ρ′ ∷ Δ ⊆ Γ) (⊢E : ⊢ E)
             ([a] : E ⊩⟨ l ⟩ a ∷ U.wk ρ (U.wk ρ′ F) ^ iF / [F]′ [ρ] [ρ′] ⊢E)
           → E ⊩⟨ l ⟩ a ∷ U.wk (ρ • ρ′) F ^ iF / [F] ([ρ] •ₜ [ρ′]) ⊢E
      [a]′ {ρ} {ρ′} [ρ] [ρ′] ⊢E [a] = irrelevanceTerm′ (wk-comp ρ ρ′ F) PE.refl PE.refl
                                          ([F]′ [ρ] [ρ′] ⊢E) ([F] ([ρ] •ₜ [ρ′]) ⊢E) [a]
      [G]′ : ∀ {ρ ρ′ E a} ([ρ] : ρ ∷ E ⊆ Δ) ([ρ′] : ρ′ ∷ Δ ⊆ Γ) (⊢E : ⊢ E)
             ([a] : E ⊩⟨ l ⟩ a ∷ U.wk ρ (U.wk ρ′ F) ^ iF / [F]′ [ρ] [ρ′] ⊢E)
           → E ⊩⟨ l ⟩ U.wk (lift (ρ • ρ′)) G [ a ] ^ rA
      [G]′ η η′ ⊢E [a] = [G] (η •ₜ η′) ⊢E ([a]′ η η′ ⊢E [a])
  in  ∃ᵣ′ (U.wk ρ F) (U.wk (lift ρ) G) (T.wkRed:*: [ρ] ⊢Δ D) ⊢ρF
           (T.wk (lift [ρ]) (⊢Δ ∙ ⊢ρF) ⊢G)
           (≅-wk [ρ] ⊢Δ A≡A)
           (λ {ρ₁} [ρ₁] ⊢Δ₁ → irrelevance′ (PE.sym (wk-comp ρ₁ ρ F))
                                    ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁))
           (λ {ρ₁} [ρ₁] ⊢Δ₁ [a] → irrelevance′ (wk-comp-subst ρ₁ ρ G)
                                        ([G]′ [ρ₁] [ρ] ⊢Δ₁ [a]))
           (λ {ρ₁} [ρ₁] ⊢Δ₁ [a] [b] [a≡b] →
              let [a≡b]′ = irrelevanceEqTerm′ (wk-comp ρ₁ ρ F) PE.refl PE.refl
                                              ([F]′ [ρ₁] [ρ] ⊢Δ₁)
                                              ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁)
                                              [a≡b]
              in  irrelevanceEq″ (wk-comp-subst ρ₁ ρ G)
                                  (wk-comp-subst ρ₁ ρ G) PE.refl PE.refl
                                  ([G]′ [ρ₁] [ρ] ⊢Δ₁ [a])
                                  (irrelevance′
                                            (wk-comp-subst ρ₁ ρ G)
                                            ([G]′ [ρ₁] [ρ] ⊢Δ₁ [a]))
                                  (G-ext ([ρ₁] •ₜ [ρ]) ⊢Δ₁
                                         ([a]′ [ρ₁] [ρ] ⊢Δ₁ [a])
                                         ([a]′ [ρ₁] [ρ] ⊢Δ₁ [b])
                                         [a≡b]′))
wk {l = ι ¹} ρ ⊢Δ (emb l< X) = emb l< (wk ρ ⊢Δ X)
wk {l = ∞} ρ ⊢Δ (emb l< X) = emb l< (wk ρ ⊢Δ X)

wkEq : ∀ {ρ Γ Δ A B r l} → ([ρ] : ρ ∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
       ([A] : Γ ⊩⟨ l ⟩ A ^ r)
     → Γ ⊩⟨ l ⟩ A ≡ B ^ r / [A]
     → Δ ⊩⟨ l ⟩ U.wk ρ A ≡ U.wk ρ B ^ r / wk [ρ] ⊢Δ [A]
wkEq ρ ⊢Δ (Uᵣ (Uᵣ r l′ l< eq d)) D = wkRed* ρ ⊢Δ D
wkEq ρ ⊢Δ (ℕᵣ D) A≡B = wkRed* ρ ⊢Δ A≡B
wkEq ρ ⊢Δ (Emptyᵣ D) A≡B = wkRed* ρ ⊢Δ A≡B
wkEq {ρ} [ρ] ⊢Δ (ne′ _ _ _ _) (ne₌ M D′ neM K≡M) =
  ne₌ (U.wk ρ M) (wkRed:*: [ρ] ⊢Δ D′)
      (wkNeutral ρ neM) (~-wk [ρ] ⊢Δ K≡M)
wkEq {ρ} [ρ] ⊢Δ (Πᵣ′ rF lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  Π₌ (U.wk ρ F′) (U.wk (lift ρ) G′) (T.wkRed* [ρ] ⊢Δ D′) (≅-wk [ρ] ⊢Δ A≡B)
     (λ {ρ₁} [ρ₁] ⊢Δ₁ → irrelevanceEq″ (PE.sym (wk-comp ρ₁ ρ F))
                                 (PE.sym (wk-comp ρ₁ ρ F′)) PE.refl PE.refl
                                 ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁)
                                 (irrelevance′ (PE.sym (wk-comp ρ₁ ρ F))
                                               ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁))
                                 ([F≡F′] ([ρ₁] •ₜ [ρ]) ⊢Δ₁))
     (λ {ρ₁} [ρ₁] ⊢Δ₁ [a] →
        let [a]′ = irrelevanceTerm′ (wk-comp ρ₁ ρ F) PE.refl PE.refl
                                    (irrelevance′ (PE.sym (wk-comp ρ₁ ρ F))
                                                  ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁))
                                    ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁) [a]
        in  irrelevanceEq″ (wk-comp-subst ρ₁ ρ G)
                            (wk-comp-subst ρ₁ ρ G′) PE.refl PE.refl
                            ([G] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′)
                            (irrelevance′ (wk-comp-subst ρ₁ ρ G)
                                          ([G] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′))
                            ([G≡G′] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′))
wkEq {ρ} [ρ] ⊢Δ (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                (∃₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  ∃₌ (U.wk ρ F′) (U.wk (lift ρ) G′) (T.wkRed* [ρ] ⊢Δ D′) (≅-wk [ρ] ⊢Δ A≡B)
     (λ {ρ₁} [ρ₁] ⊢Δ₁ → irrelevanceEq″ (PE.sym (wk-comp ρ₁ ρ F))
                                 (PE.sym (wk-comp ρ₁ ρ F′)) PE.refl PE.refl
                                 ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁)
                                 (irrelevance′ (PE.sym (wk-comp ρ₁ ρ F))
                                               ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁))
                                 ([F≡F′] ([ρ₁] •ₜ [ρ]) ⊢Δ₁))
     (λ {ρ₁} [ρ₁] ⊢Δ₁ [a] →
        let [a]′ = irrelevanceTerm′ (wk-comp ρ₁ ρ F) PE.refl PE.refl
                                    (irrelevance′ (PE.sym (wk-comp ρ₁ ρ F))
                                                  ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁))
                                    ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁) [a]
        in  irrelevanceEq″ (wk-comp-subst ρ₁ ρ G)
                            (wk-comp-subst ρ₁ ρ G′) PE.refl PE.refl
                            ([G] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′)
                            (irrelevance′ (wk-comp-subst ρ₁ ρ G)
                                          ([G] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′))
                            ([G≡G′] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′))
wkEq {l = ι ¹} ρ ⊢Δ (emb l< X) A≡B = wkEq ρ ⊢Δ X A≡B
wkEq {l = ∞} ρ ⊢Δ (emb l< X) A≡B = wkEq ρ ⊢Δ X A≡B

wkTerm : ∀ {ρ Γ Δ A t r l} ([ρ] : ρ ∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
         ([A] : Γ ⊩⟨ l ⟩ A ^ r)
       → Γ ⊩⟨ l ⟩ t ∷ A ^ r / [A]
       → Δ ⊩⟨ l ⟩ U.wk ρ t ∷ U.wk ρ A ^ r / wk [ρ] ⊢Δ [A]
wkTerm {ρ} {Δ = Δ} {t = t} {l = ι ¹} [ρ] ⊢Δ (Uᵣ (Uᵣ r ⁰ l< eq d)) (Uₜ K d₁ typeK K≡K [t]) =
  let
    -- this code is a bit of a mess tbh
    -- it is mostly about using irrelevance back and forth between proofs of
    -- reducibility using U.wk ρ′ (U.wk ρ t) and proofs using U.wk (ρ′ • ρ) t
    [t]′ = λ {ρ′} {Δ′} [ρ′] (⊢Δ′ : ⊢ Δ′) →
      irrelevance′ (PE.sym (wk-comp ρ′ ρ t)) ([t] ([ρ′] •ₜ [ρ]) ⊢Δ′)
    [t]′_to_[t] = λ {ρ′} {Δ′} {a} [ρ′] (⊢Δ′ : ⊢ Δ′)
      ([a] : Δ′ ⊩⟨ ι ⁰ ⟩ a ∷ U.wk ρ′ (U.wk ρ t) ^ [ r , ι ⁰ ] / [t]′ [ρ′] ⊢Δ′) →
      irrelevanceTerm′ (wk-comp ρ′ ρ t) PE.refl PE.refl ([t]′ [ρ′] ⊢Δ′) ([t] ([ρ′] •ₜ [ρ]) ⊢Δ′) [a]
    [t]′_to_[t]_eq = λ {ρ′} {Δ′} {a} {a′} [ρ′] (⊢Δ′ : ⊢ Δ′)
      (a≡a′ : Δ′ ⊩⟨ ι ⁰ ⟩ a ≡ a′ ∷ U.wk ρ′ (U.wk ρ t) ^ [ r , ι ⁰ ] / [t]′ [ρ′] ⊢Δ′) →
      irrelevanceEqTerm′ (wk-comp ρ′ ρ t) PE.refl PE.refl ([t]′ [ρ′] ⊢Δ′) ([t] ([ρ′] •ₜ [ρ]) ⊢Δ′) a≡a′
    [t]′_to_[t]_id = λ {ρ′} {Δ′} {e} {B} [e] →
      (PE.subst (λ X → Δ′ ⊢ e ∷ Id (U ⁰) X B ^ [ % , ι ¹ ]) (wk-comp ρ′ ρ t) [e])
  in
  Uₜ (U.wk ρ K) (wkRed:*:Term [ρ] ⊢Δ d₁) (wkType ρ typeK) (≅ₜ-wk [ρ] ⊢Δ K≡K) [t]′
-- this is a duplicate of the above code (because we need logRelRec to compute)
-- surely there is a way to avoid this redundancy
wkTerm {ρ} {Δ = Δ} {t = t} {l = ∞} [ρ] ⊢Δ (Uᵣ (Uᵣ r ¹ l< eq d)) (Uₜ K d₁ typeK K≡K [t]) =
  let
    [t]′ = λ {ρ′} {Δ′} [ρ′] (⊢Δ′ : ⊢ Δ′) →
      irrelevance′ (PE.sym (wk-comp ρ′ ρ t)) ([t] ([ρ′] •ₜ [ρ]) ⊢Δ′)
    [t]′_to_[t] = λ {ρ′} {Δ′} {a} [ρ′] (⊢Δ′ : ⊢ Δ′)
      ([a] : Δ′ ⊩⟨ ι ¹ ⟩ a ∷ U.wk ρ′ (U.wk ρ t) ^ [ r , ι ¹ ] / [t]′ [ρ′] ⊢Δ′) →
      irrelevanceTerm′ (wk-comp ρ′ ρ t) PE.refl PE.refl ([t]′ [ρ′] ⊢Δ′) ([t] ([ρ′] •ₜ [ρ]) ⊢Δ′) [a]
    [t]′_to_[t]_eq = λ {ρ′} {Δ′} {a} {a′} [ρ′] (⊢Δ′ : ⊢ Δ′)
      (a≡a′ : Δ′ ⊩⟨ ι ¹ ⟩ a ≡ a′ ∷ U.wk ρ′ (U.wk ρ t) ^ [ r , ι ¹ ] / [t]′ [ρ′] ⊢Δ′) →
      irrelevanceEqTerm′ (wk-comp ρ′ ρ t) PE.refl PE.refl ([t]′ [ρ′] ⊢Δ′) ([t] ([ρ′] •ₜ [ρ]) ⊢Δ′) a≡a′
    [t]′_to_[t]_id = λ {ρ′} {Δ′} {e} {B} [e] →
      (PE.subst (λ X → Δ′ ⊢ e ∷ Id (U ⁰) X B ^ [ % , ι ¹ ]) (wk-comp ρ′ ρ t) [e])
  in
  Uₜ (U.wk ρ K) (wkRed:*:Term [ρ] ⊢Δ d₁) (wkType ρ typeK) (≅ₜ-wk [ρ] ⊢Δ K≡K) [t]′
wkTerm ρ ⊢Δ (ℕᵣ D) [t] = wkTermℕ ρ ⊢Δ [t]
wkTerm ρ ⊢Δ (Emptyᵣ D) [t] = wkTermEmpty ρ ⊢Δ [t]
wkTerm {ρ} {r = [ ! , l′ ]} [ρ] ⊢Δ (ne′ K D neK K≡K) (neₜ k d nf) =
  neₜ (U.wk ρ k) (wkRed:*:Term [ρ] ⊢Δ d) (wkTermNe [ρ] ⊢Δ nf)
wkTerm {ρ} {r = [ % , l′ ]} [ρ] ⊢Δ (ne′ K D neK K≡K) (neₜ d) = neₜ ( T.wkTerm [ρ] ⊢Δ d)
wkTerm {ρ} {r = [ ! , l′ ]} [ρ] ⊢Δ (Πᵣ′ rF lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (Πₜ f d funcF f≡f [f] [f]₁) =
  Πₜ (U.wk ρ f) (wkRed:*:Term [ρ] ⊢Δ d) (wkFunction ρ funcF)
     (≅ₜ-wk [ρ] ⊢Δ f≡f)
     (λ {ρ₁} [ρ₁] ⊢Δ₁ [a] [b] [a≡b] →
        let F-compEq = wk-comp ρ₁ ρ F
            G-compEq = wk-comp-subst ρ₁ ρ G
            [F]₁ = [F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁
            [F]₂ = irrelevance′ (PE.sym (wk-comp ρ₁ ρ F)) [F]₁
            [a]′ = irrelevanceTerm′ F-compEq PE.refl PE.refl [F]₂ [F]₁ [a]
            [b]′ = irrelevanceTerm′ F-compEq PE.refl PE.refl [F]₂ [F]₁ [b]
            [G]₁ = [G] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′
            [G]₂ = irrelevance′ G-compEq [G]₁
            [a≡b]′ = irrelevanceEqTerm′ F-compEq PE.refl PE.refl [F]₂ [F]₁ [a≡b]
        in  irrelevanceEqTerm″ PE.refl PE.refl (PE.cong (λ x → x ∘ _ ^ _ ) (PE.sym (wk-comp ρ₁ ρ _)))
                                (PE.cong (λ x → x ∘ _ ^ _) (PE.sym (wk-comp ρ₁ ρ _)))
                                G-compEq
                                [G]₁ [G]₂
                                ([f] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′ [b]′ [a≡b]′))
     (λ {ρ₁} [ρ₁] ⊢Δ₁ [a] →
        let [F]₁ = [F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁
            [F]₂ = irrelevance′ (PE.sym (wk-comp ρ₁ ρ F)) [F]₁
            [a]′ = irrelevanceTerm′ (wk-comp ρ₁ ρ F) PE.refl PE.refl [F]₂ [F]₁ [a]
            [G]₁ = [G] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′
            [G]₂ = irrelevance′ (wk-comp-subst ρ₁ ρ G) [G]₁
        in  irrelevanceTerm″ (wk-comp-subst ρ₁ ρ G) PE.refl PE.refl
                              (PE.cong (λ x → x ∘ _ ^ _ ) (PE.sym (wk-comp ρ₁ ρ _)))
                              [G]₁ [G]₂ ([f]₁ ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′))
wkTerm {ρ} {r = [ % , l′ ]} [ρ] ⊢Δ (Πᵣ′ rF lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext) d = T.wkTerm [ρ] ⊢Δ d
wkTerm {ρ} [ρ] ⊢Δ (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) d = T.wkTerm [ρ] ⊢Δ d
wkTerm {l = ι ¹} ρ ⊢Δ (emb l< X) t = wkTerm ρ ⊢Δ X t
wkTerm {l = ∞} ρ ⊢Δ (emb l< X) t = wkTerm ρ ⊢Δ X t

wkEqTerm : ∀ {ρ Γ Δ A t u r l} ([ρ] : ρ ∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
           ([A] : Γ ⊩⟨ l ⟩ A ^ r)
         → Γ ⊩⟨ l ⟩ t ≡ u ∷ A ^ r / [A]
         → Δ ⊩⟨ l ⟩ U.wk ρ t ≡ U.wk ρ u ∷ U.wk ρ A ^ r / wk [ρ] ⊢Δ [A]
wkEqTerm {ρ} {Γ} {Δ} {A} {t} {u} {r} {l = ι ¹} [ρ] ⊢Δ (Uᵣ (Uᵣ ti ⁰ l< eq d)) (Uₜ₌ [t] [u] A≡B [t≡u]) =
  let
    [t]′ = λ {ρ′} {Δ′} ([ρ′] : ρ′ ∷ Δ′ ⊆ Δ) (⊢Δ′ : ⊢ Δ′) →
      irrelevance′ (PE.sym (wk-comp ρ′ ρ t)) (LogRel._⊩¹U_∷_^_/_.[t] [t] ([ρ′] •ₜ [ρ]) ⊢Δ′)
    [t]″ = λ {ρ′} {Δ′} ([ρ′] : ρ′ ∷ Δ′ ⊆ Δ) (⊢Δ′ : ⊢ Δ′) →
      LogRel._⊩¹U_∷_^_/_.[t] [t] ([ρ′] •ₜ [ρ]) ⊢Δ′
    [t]′_to_[t]″ = λ {ρ′} {Δ′} {a} [ρ′] (⊢Δ′ : ⊢ Δ′)
      ([a] : Δ′ ⊩⟨ ι ⁰ ⟩ a ∷ U.wk ρ′ (U.wk ρ t) ^ [ ti , ι ⁰ ] / [t]′ [ρ′] ⊢Δ′) →
      (irrelevanceTerm′ (wk-comp ρ′ ρ t) PE.refl PE.refl ([t]′ [ρ′] ⊢Δ′) ([t]″ [ρ′] ⊢Δ′) [a])
    [t≡u]′ = λ {ρ′} {Δ′} [ρ′] (⊢Δ′ : ⊢ Δ′) →
      irrelevanceEq″ (PE.sym (wk-comp ρ′ ρ t)) (PE.sym (wk-comp ρ′ ρ u)) PE.refl PE.refl ([t]″ [ρ′] ⊢Δ′)
        ((LogRel._⊩¹U_∷_^_/_.[t] (wkTerm [ρ] ⊢Δ (Uᵣ (Uᵣ ti ⁰ l< eq d)) [t]) [ρ′] ⊢Δ′))
        ([t≡u] ([ρ′] •ₜ [ρ]) ⊢Δ′)
  in
  Uₜ₌ (wkTerm [ρ] ⊢Δ (Uᵣ (Uᵣ ti ⁰ l< eq d)) [t]) (wkTerm [ρ] ⊢Δ (Uᵣ (Uᵣ ti ⁰ l< eq d)) [u])
    (≅ₜ-wk [ρ] ⊢Δ A≡B) [t≡u]′
-- this is a duplicate of the above code (because we need logRelRec to compute)
-- surely there is a way to avoid this redundancy
wkEqTerm {ρ} {Γ} {Δ} {A} {t} {u} {r} {l = ∞} [ρ] ⊢Δ (Uᵣ (Uᵣ ti ¹ l< eq d)) (Uₜ₌ [t] [u] A≡B [t≡u]) =
  let
    [t]′ = λ {ρ′} {Δ′} ([ρ′] : ρ′ ∷ Δ′ ⊆ Δ) (⊢Δ′ : ⊢ Δ′) →
      irrelevance′ (PE.sym (wk-comp ρ′ ρ t)) (LogRel._⊩¹U_∷_^_/_.[t] [t] ([ρ′] •ₜ [ρ]) ⊢Δ′)
    [t]″ = λ {ρ′} {Δ′} ([ρ′] : ρ′ ∷ Δ′ ⊆ Δ) (⊢Δ′ : ⊢ Δ′) →
      LogRel._⊩¹U_∷_^_/_.[t] [t] ([ρ′] •ₜ [ρ]) ⊢Δ′
    [t]′_to_[t]″ = λ {ρ′} {Δ′} {a} [ρ′] (⊢Δ′ : ⊢ Δ′)
      ([a] : Δ′ ⊩⟨ ι ¹ ⟩ a ∷ U.wk ρ′ (U.wk ρ t) ^ [ ti , ι ¹ ] / [t]′ [ρ′] ⊢Δ′) →
      (irrelevanceTerm′ (wk-comp ρ′ ρ t) PE.refl PE.refl ([t]′ [ρ′] ⊢Δ′) ([t]″ [ρ′] ⊢Δ′) [a])
    [t≡u]′ = λ {ρ′} {Δ′} [ρ′] (⊢Δ′ : ⊢ Δ′) →
      irrelevanceEq″ (PE.sym (wk-comp ρ′ ρ t)) (PE.sym (wk-comp ρ′ ρ u)) PE.refl PE.refl ([t]″ [ρ′] ⊢Δ′)
        ((LogRel._⊩¹U_∷_^_/_.[t] (wkTerm [ρ] ⊢Δ (Uᵣ (Uᵣ ti ¹ l< eq d)) [t]) [ρ′] ⊢Δ′))
        ([t≡u] ([ρ′] •ₜ [ρ]) ⊢Δ′)
  in
  Uₜ₌ (wkTerm [ρ] ⊢Δ (Uᵣ (Uᵣ ti ¹ l< eq d)) [t]) (wkTerm [ρ] ⊢Δ (Uᵣ (Uᵣ ti ¹ l< eq d)) [u])
    (≅ₜ-wk [ρ] ⊢Δ A≡B) [t≡u]′
wkEqTerm ρ ⊢Δ (ℕᵣ D) [t≡u] = wkEqTermℕ ρ ⊢Δ [t≡u]
wkEqTerm ρ ⊢Δ (Emptyᵣ D) [t≡u] = wkEqTermEmpty ρ ⊢Δ [t≡u]
wkEqTerm {ρ} {r = [ ! , l′ ]} [ρ] ⊢Δ (ne′ K D neK K≡K) (neₜ₌ k m d d′ nf) =
  neₜ₌ (U.wk ρ k) (U.wk ρ m)
       (wkRed:*:Term [ρ] ⊢Δ d) (wkRed:*:Term [ρ] ⊢Δ d′)
       (wkEqTermNe [ρ] ⊢Δ nf)
wkEqTerm {ρ} {r = [ % , l′ ]}[ρ] ⊢Δ (ne′ K D neK K≡K) (neₜ₌ d d′) = neₜ₌ (T.wkTerm [ρ] ⊢Δ d) (T.wkTerm [ρ] ⊢Δ d′)
wkEqTerm {ρ} {r = [ ! , l′ ]} [ρ] ⊢Δ (Πᵣ′ rF lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                    (Πₜ₌ f g d d′ funcF funcG f≡g [t] [u] [f≡g]) =
  let [A] = Πᵣ′ rF lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext
  in  Πₜ₌ (U.wk ρ f) (U.wk ρ g) (wkRed:*:Term [ρ] ⊢Δ d) (wkRed:*:Term [ρ] ⊢Δ d′)
          (wkFunction ρ funcF) (wkFunction ρ funcG)
          (≅ₜ-wk [ρ] ⊢Δ f≡g) (wkTerm [ρ] ⊢Δ [A] [t]) (wkTerm [ρ] ⊢Δ [A] [u])
          (λ {ρ₁} [ρ₁] ⊢Δ₁ [a] →
             let [F]₁ = [F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁
                 [F]₂ = irrelevance′ (PE.sym (wk-comp ρ₁ ρ F)) [F]₁
                 [a]′ = irrelevanceTerm′ (wk-comp ρ₁ ρ F) PE.refl PE.refl [F]₂ [F]₁ [a]
                 [G]₁ = [G] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′
                 [G]₂ = irrelevance′ (wk-comp-subst ρ₁ ρ G) [G]₁
             in  irrelevanceEqTerm″ PE.refl PE.refl (PE.cong (λ y → y ∘ _ ^ _) (PE.sym (wk-comp ρ₁ ρ _)))
                                     (PE.cong (λ y → y ∘ _ ^ _) (PE.sym (wk-comp ρ₁ ρ _)))
                                     (wk-comp-subst ρ₁ ρ G)
                                     [G]₁ [G]₂
                                     ([f≡g] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′))
wkEqTerm {ρ} {r = [ % , l′ ]} [ρ] ⊢Δ (Πᵣ′ rF lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                    (d , d′) = T.wkTerm [ρ] ⊢Δ d , T.wkTerm [ρ] ⊢Δ d′
wkEqTerm {ρ} {r = [ % , l′ ]} [ρ] ⊢Δ (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                    (d , d′) = T.wkTerm [ρ] ⊢Δ d , T.wkTerm [ρ] ⊢Δ d′
wkEqTerm {l = ι ¹} ρ ⊢Δ (emb l< X) t≡u = wkEqTerm ρ ⊢Δ X t≡u
wkEqTerm {l = ∞} ρ ⊢Δ (emb l< X) t≡u = wkEqTerm ρ ⊢Δ X t≡u

ext: agda

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
{-# OPTIONS --without-K #-}
module function.extensionality.strong where

open import level
open import sum
open import function.core
open import equality.core
open import function.isomorphism
open import function.extensionality.core
open import function.extensionality.proof
open import hott.level.core
open import hott.level.closure.core
open import hott.equivalence.core

private
  module Dummy {i j}{X : Set i}{Y : X → Set j} where
    _~_ : (f g : (x : X) → Y x) → Set (i ⊔ j)
    f ~ g = ∀ x → f x ≡ g x
    infix 5 _~_

    R : (f : (x : X) → Y x) → f ~ f
    R f x = refl

    iso₁ : {f g : (x : X) → Y x} (p : f ≡ g)
         → funext (funext-inv p) ≡ p
    iso₁ {f} refl = funext-id f

    iso₂ : (f g : (x : X) → Y x) (h : f ~ g)
         → funext-inv (funext h) ≡ h
    iso₂ f g h = subst (λ {(g , h) → funext-inv (funext h) ≡ h})
                       (e-contr' (g , h))
                       strong-id
      where
        E : Set (i ⊔ j)
        E = Σ ((x : X) → Y x) λ g → f ~ g

        e-contr : contr E
        e-contr = retract-level
          (λ u → proj₁ ∘' u , proj₂ ∘' u)
          (λ {(g , h) x → g x , h x})
          (λ {(g , h) → refl})
          (Π-contr (λ x → singl-contr (f x)))

        e-contr' : (u : E) → (f , R f) ≡ u
        e-contr' u = contr⇒prop e-contr (f , R f) u

        strong-id : funext-inv (funext (R f)) ≡ R f
        strong-id = ap funext-inv (funext-id f)

    strong-funext-iso : {f g : (x : X) → Y x}
                   → (f ~ g) ≅ (f ≡ g)
    strong-funext-iso {f}{g} = iso funext funext-inv (iso₂ f g) iso₁

    strong-funext : {f g : (x : X) → Y x} → (f ~ g) ≡ (f ≡ g)
    strong-funext = ≅⇒≡ strong-funext-iso

open Dummy public using (strong-funext; strong-funext-iso)

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
module ConstructorsInstance where

record UnitRC : Set where
  instance
    constructor tt

data UnitD : Set where
  instance
    tt : UnitD

postulate
  fRC : {{_ : UnitRC}} → Set
  fD  : {{_ : UnitD}}  → Set

tryRC : Set
tryRC = fRC

tryD : Set
tryD = fD

data D : Set where
  a : D
  instance
    b : D
  c : D

postulate
  g : {{_ : D}} → Set

-- This should work because instance search will choose [b]
try2 : Set
try2 = g

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Everything where

open import Cubical.HITs.Cylinder public
open import Cubical.HITs.Hopf public
open import Cubical.HITs.Interval public
open import Cubical.HITs.Ints.BiInvInt public hiding ( pred ; suc-pred ; pred-suc )
open import Cubical.HITs.Ints.DeltaInt public hiding ( pred ; succ ; zero )
open import Cubical.HITs.Ints.HAEquivInt public hiding ( suc-haequiv )
open import Cubical.HITs.Ints.IsoInt public
open import Cubical.HITs.Ints.QuoInt public
open import Cubical.HITs.Join public
open import Cubical.HITs.ListedFiniteSet public
open import Cubical.HITs.Pushout public
open import Cubical.HITs.Modulo public
open import Cubical.HITs.S1 public
open import Cubical.HITs.S2 public
open import Cubical.HITs.S3 public
open import Cubical.HITs.Rational public
open import Cubical.HITs.Susp public
open import Cubical.HITs.SmashProduct public renaming (comm to Smash-comm)
open import Cubical.HITs.Torus public
open import Cubical.HITs.PropositionalTruncation public
open import Cubical.HITs.SetTruncation public
open import Cubical.HITs.GroupoidTruncation public
open import Cubical.HITs.2GroupoidTruncation public
open import Cubical.HITs.SetQuotients public
open import Cubical.HITs.FiniteMultiset public hiding ( _++_ ; [_] ; assoc-++ )
open import Cubical.HITs.Colimit


text:
{-# OPTIONS -WShadowingInTelescope #-}

bad : Set → Set → Set
bad = λ x x → x


text:
{-# OPTIONS --safe #-}

module Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Function hiding (const)
open import Cubical.Foundations.Isomorphism

open import Cubical.Data.Sigma.Properties using (Σ≡Prop)
open import Cubical.HITs.SetTruncation

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base
open import Cubical.Algebra.Ring        using ()
open import Cubical.Algebra.CommAlgebra
open import Cubical.Algebra.CommAlgebra.Instances.Initial
open import Cubical.Algebra.Algebra

open import Cubical.Data.Empty
open import Cubical.Data.Sigma

private
  variable
    ℓ ℓ' ℓ'' : Level

module Theory {R : CommRing ℓ} {I : Type ℓ'} where
  open CommRingStr (snd R)
         using (0r; 1r)
         renaming (_·_ to _·r_; _+_ to _+r_; ·Comm to ·r-comm; ·Rid to ·r-rid)

  module _ (A : CommAlgebra R ℓ'') (φ : I → ⟨ A ⟩) where
    open CommAlgebraStr (A .snd)
    open AlgebraTheory (CommRing→Ring R) (CommAlgebra→Algebra A)
    open Construction using (var; const) renaming (_+_ to _+c_; -_ to -c_; _·_ to _·c_)

    imageOf0Works : 0r ⋆ 1a ≡ 0a
    imageOf0Works = 0-actsNullifying 1a

    imageOf1Works : 1r ⋆ 1a ≡ 1a
    imageOf1Works = ⋆-lid 1a

    inducedMap : ⟨ R [ I ] ⟩ → ⟨ A ⟩
    inducedMap (var x) = φ x
    inducedMap (const r) = r ⋆ 1a
    inducedMap (P +c Q) = (inducedMap P) + (inducedMap Q)
    inducedMap (-c P) = - inducedMap P
    inducedMap (Construction.+-assoc P Q S i) = +-assoc (inducedMap P) (inducedMap Q) (inducedMap S) i
    inducedMap (Construction.+-rid P i) =
      let
        eq : (inducedMap P) + (inducedMap (const 0r)) ≡ (inducedMap P)
        eq = (inducedMap P) + (inducedMap (const 0r)) ≡⟨ refl ⟩
             (inducedMap P) + (0r ⋆ 1a)               ≡⟨ cong
                                                         (λ u → (inducedMap P) + u)
                                                         (imageOf0Works) ⟩
             (inducedMap P) + 0a                      ≡⟨ +-rid _ ⟩
             (inducedMap P) ∎
      in eq i
    inducedMap (Construction.+-rinv P i) =
      let eq : (inducedMap P - inducedMap P) ≡ (inducedMap (const 0r))
          eq = (inducedMap P - inducedMap P) ≡⟨ +-rinv _ ⟩
               0a                            ≡⟨ sym imageOf0Works ⟩
               (inducedMap (const 0r))∎
      in eq i
    inducedMap (Construction.+-comm P Q i) = +-comm (inducedMap P) (inducedMap Q) i
    inducedMap (P ·c Q) = inducedMap P · inducedMap Q
    inducedMap (Construction.·-assoc P Q S i) = ·Assoc (inducedMap P) (inducedMap Q) (inducedMap S) i
    inducedMap (Construction.·-lid P i) =
      let eq = inducedMap (const 1r) · inducedMap P ≡⟨ cong (λ u → u · inducedMap P) imageOf1Works ⟩
               1a · inducedMap P                    ≡⟨ ·Lid (inducedMap P) ⟩
               inducedMap P ∎
      in eq i
    inducedMap (Construction.·-comm P Q i) = ·-comm (inducedMap P) (inducedMap Q) i
    inducedMap (Construction.ldist P Q S i) = ·Ldist+ (inducedMap P) (inducedMap Q) (inducedMap S) i
    inducedMap (Construction.+HomConst s t i) = ⋆-ldist s t 1a i
    inducedMap (Construction.·HomConst s t i) =
      let eq = (s ·r t) ⋆ 1a       ≡⟨ cong (λ u → u ⋆ 1a) (·r-comm _ _) ⟩
               (t ·r s) ⋆ 1a       ≡⟨ ⋆-assoc t s 1a ⟩
               t ⋆ (s ⋆ 1a)        ≡⟨ cong (λ u → t ⋆ u) (sym (·Rid _)) ⟩
               t ⋆ ((s ⋆ 1a) · 1a) ≡⟨ ⋆-rassoc t (s ⋆ 1a) 1a ⟩
               (s ⋆ 1a) · (t ⋆ 1a) ∎
      in eq i
    inducedMap (Construction.0-trunc P Q p q i j) =
      isSetAlgebra (CommAlgebra→Algebra A) (inducedMap P) (inducedMap Q) (cong _ p) (cong _ q) i j

    module _ where
      open IsAlgebraHom

      inducedHom : AlgebraHom (CommAlgebra→Algebra (R [ I ])) (CommAlgebra→Algebra A)
      inducedHom .fst = inducedMap
      inducedHom .snd .pres0 = 0-actsNullifying _
      inducedHom .snd .pres1 = imageOf1Works
      inducedHom .snd .pres+ x y = refl
      inducedHom .snd .pres· x y = refl
      inducedHom .snd .pres- x = refl
      inducedHom .snd .pres⋆ r x =
        (r ⋆ 1a) · inducedMap x ≡⟨ ⋆-lassoc r 1a (inducedMap x) ⟩
        r ⋆ (1a · inducedMap x) ≡⟨ cong (λ u → r ⋆ u) (·Lid (inducedMap x)) ⟩
        r ⋆ inducedMap x ∎

  module _ (A : CommAlgebra R ℓ'') where
    open CommAlgebraStr (A .snd)
    open AlgebraTheory (CommRing→Ring R) (CommAlgebra→Algebra A)
    open Construction using (var; const) renaming (_+_ to _+c_; -_ to -c_; _·_ to _·c_)

    Hom = CommAlgebraHom  (R [ I ]) A
    open IsAlgebraHom

    evaluateAt : Hom → I → ⟨ A ⟩
    evaluateAt φ x = φ .fst (var x)

    mapRetrievable : ∀ (φ : I → ⟨ A ⟩)
                     → evaluateAt (inducedHom A φ) ≡ φ
    mapRetrievable φ = refl

    proveEq : ∀ {X : Type ℓ''} (isSetX : isSet X) (f g : ⟨ R [ I ] ⟩ → X)
              → (var-eq : (x : I) → f (var x) ≡ g (var x))
              → (const-eq : (r : ⟨ R ⟩) → f (const r) ≡ g (const r))
              → (+-eq : (x y : ⟨ R [ I ] ⟩) → (eq-x : f x ≡ g x) → (eq-y : f y ≡ g y)
                        → f (x +c y) ≡ g (x +c y))
              → (·-eq : (x y : ⟨ R [ I ] ⟩) → (eq-x : f x ≡ g x) → (eq-y : f y ≡ g y)
                        → f (x ·c y) ≡ g (x ·c y))
              → (-eq : (x : ⟨ R [ I ] ⟩) → (eq-x : f x ≡ g x)
                        → f (-c x) ≡ g (-c x))
              → f ≡ g
    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (var x) = var-eq x i
    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (const x) = const-eq x i
    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (x +c y) =
      +-eq x y
           (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
           (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i y)
           i
    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (-c x) =
      -eq x ((λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)) i
    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (x ·c y) =
      ·-eq x y
           (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
           (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i y)
           i
    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.+-assoc x y z j) =
       let
        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
        a₀₋ : f (x +c (y +c z)) ≡ g (x +c (y +c z))
        a₀₋ = +-eq _ _ (rec x) (+-eq _ _ (rec y) (rec z))
        a₁₋ : f ((x +c y) +c z) ≡ g ((x +c y) +c z)
        a₁₋ = +-eq _ _ (+-eq _ _ (rec x) (rec y)) (rec z)
        a₋₀ : f (x +c (y +c z)) ≡ f ((x +c y) +c z)
        a₋₀ = cong f (Construction.+-assoc x y z)
        a₋₁ : g (x +c (y +c z)) ≡ g ((x +c y) +c z)
        a₋₁ = cong g (Construction.+-assoc x y z)
      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i

    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.+-rid x j) =
       let
        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
        a₀₋ : f (x +c (const 0r)) ≡ g (x +c (const 0r))
        a₀₋ = +-eq _ _ (rec x) (const-eq 0r)
        a₁₋ : f x ≡ g x
        a₁₋ = rec x
        a₋₀ : f (x +c (const 0r)) ≡ f x
        a₋₀ = cong f (Construction.+-rid x)
        a₋₁ : g (x +c (const 0r)) ≡ g x
        a₋₁ = cong g (Construction.+-rid x)
      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i

    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.+-rinv x j) =
       let
        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
        a₀₋ : f (x +c (-c x)) ≡ g (x +c (-c x))
        a₀₋ = +-eq x (-c x) (rec x) (-eq x (rec x))
        a₁₋ : f (const 0r) ≡ g (const 0r)
        a₁₋ = const-eq 0r
        a₋₀ : f (x +c (-c x)) ≡ f (const 0r)
        a₋₀ = cong f (Construction.+-rinv x)
        a₋₁ : g (x +c (-c x)) ≡ g (const 0r)
        a₋₁ = cong g (Construction.+-rinv x)
      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i

    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.+-comm x y j) =
      let
        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
        a₀₋ : f (x +c y) ≡ g (x +c y)
        a₀₋ = +-eq x y (rec x) (rec y)
        a₁₋ : f (y +c x) ≡ g (y +c x)
        a₁₋ = +-eq y x (rec y) (rec x)
        a₋₀ : f (x +c y) ≡ f (y +c x)
        a₋₀ = cong f (Construction.+-comm x y)
        a₋₁ : g (x +c y) ≡ g (y +c x)
        a₋₁ = cong g (Construction.+-comm x y)
      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i

    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.·-assoc x y z j) =
       let
        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
        a₀₋ : f (x ·c (y ·c z)) ≡ g (x ·c (y ·c z))
        a₀₋ = ·-eq _ _ (rec x) (·-eq _ _ (rec y) (rec z))
        a₁₋ : f ((x ·c y) ·c z) ≡ g ((x ·c y) ·c z)
        a₁₋ = ·-eq _ _ (·-eq _ _ (rec x) (rec y)) (rec z)
        a₋₀ : f (x ·c (y ·c z)) ≡ f ((x ·c y) ·c z)
        a₋₀ = cong f (Construction.·-assoc x y z)
        a₋₁ : g (x ·c (y ·c z)) ≡ g ((x ·c y) ·c z)
        a₋₁ = cong g (Construction.·-assoc x y z)
      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i

    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.·-lid x j) =
       let
        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
        a₀₋ : f ((const 1r) ·c x) ≡ g ((const 1r) ·c x)
        a₀₋ = ·-eq _ _ (const-eq 1r) (rec x)
        a₁₋ : f x ≡ g x
        a₁₋ = rec x
        a₋₀ : f ((const 1r) ·c x) ≡ f x
        a₋₀ = cong f (Construction.·-lid x)
        a₋₁ : g ((const 1r) ·c x) ≡ g x
        a₋₁ = cong g (Construction.·-lid x)
      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i

    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.·-comm x y j) =
       let
        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
        a₀₋ : f (x ·c y) ≡ g (x ·c y)
        a₀₋ = ·-eq _ _ (rec x) (rec y)
        a₁₋ : f (y ·c x) ≡ g (y ·c x)
        a₁₋ = ·-eq _ _ (rec y) (rec x)
        a₋₀ : f (x ·c y) ≡ f (y ·c x)
        a₋₀ = cong f (Construction.·-comm x y)
        a₋₁ : g (x ·c y) ≡ g (y ·c x)
        a₋₁ = cong g (Construction.·-comm x y)
      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i

    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.ldist x y z j) =
       let
        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
        a₀₋ : f ((x +c y) ·c z) ≡ g ((x +c y) ·c z)
        a₀₋ = ·-eq (x +c y) z
           (+-eq _ _ (rec x) (rec y))
           (rec z)
        a₁₋ : f ((x ·c z) +c (y ·c z)) ≡ g ((x ·c z) +c (y ·c z))
        a₁₋ = +-eq _ _ (·-eq _ _ (rec x) (rec z)) (·-eq _ _ (rec y) (rec z))
        a₋₀ : f ((x +c y) ·c z) ≡ f ((x ·c z) +c (y ·c z))
        a₋₀ = cong f (Construction.ldist x y z)
        a₋₁ : g ((x +c y) ·c z) ≡ g ((x ·c z) +c (y ·c z))
        a₋₁ = cong g (Construction.ldist x y z)
      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i

    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.+HomConst s t j) =
       let
        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
        a₀₋ : f (const (s +r t)) ≡ g (const (s +r t))
        a₀₋ = const-eq (s +r t)
        a₁₋ : f (const s +c const t) ≡ g (const s +c const t)
        a₁₋ = +-eq _ _ (const-eq s) (const-eq t)
        a₋₀ : f (const (s +r t)) ≡ f (const s +c const t)
        a₋₀ = cong f (Construction.+HomConst s t)
        a₋₁ : g (const (s +r t)) ≡ g (const s +c const t)
        a₋₁ = cong g (Construction.+HomConst s t)
      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i

    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.·HomConst s t j) =
       let
        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
        a₀₋ : f (const (s ·r t)) ≡ g (const (s ·r t))
        a₀₋ = const-eq (s ·r t)
        a₁₋ : f (const s ·c const t) ≡ g (const s ·c const t)
        a₁₋ = ·-eq _ _ (const-eq s) (const-eq t)
        a₋₀ : f (const (s ·r t)) ≡ f (const s ·c const t)
        a₋₀ = cong f (Construction.·HomConst s t)
        a₋₁ : g (const (s ·r t)) ≡ g (const s ·c const t)
        a₋₁ = cong g (Construction.·HomConst s t)
      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i

    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.0-trunc x y p q j k) =
      let
        P : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
        P x i = proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x
        Q : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
        Q x i = proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x
      in isOfHLevel→isOfHLevelDep 2
           (λ z → isProp→isSet (isSetX (f z) (g z))) _ _
           (cong P p)
           (cong Q q)
           (Construction.0-trunc x y p q) j k i

    homRetrievable : ∀ (f : Hom)
                     → inducedMap A (evaluateAt f) ≡ fst f
    homRetrievable f =
       proveEq
        (isSetAlgebra (CommAlgebra→Algebra A))
        (inducedMap A (evaluateAt f))
        (λ x → f $a x)
        (λ x → refl)
        (λ r → r ⋆ 1a                     ≡⟨ cong (λ u → r ⋆ u) (sym f.pres1) ⟩
               r ⋆ (f $a (const 1r))      ≡⟨ sym (f.pres⋆ r _) ⟩
               f $a (const r ·c const 1r) ≡⟨ cong (λ u → f $a u) (sym (Construction.·HomConst r 1r)) ⟩
               f $a (const (r ·r 1r))     ≡⟨ cong (λ u → f $a (const u)) (·r-rid r) ⟩
               f $a (const r) ∎)

        (λ x y eq-x eq-y →
              ι (x +c y)            ≡⟨ refl ⟩
              (ι x + ι y)           ≡⟨ cong (λ u → u + ι y) eq-x ⟩
              ((f $a x) + ι y)      ≡⟨
                                     cong (λ u → (f $a x) + u) eq-y ⟩
              ((f $a x) + (f $a y)) ≡⟨ sym (f.pres+ _ _) ⟩ (f $a (x +c y)) ∎)

        (λ x y eq-x eq-y →
           ι (x ·c y)          ≡⟨ refl ⟩
           ι x     · ι y       ≡⟨ cong (λ u → u · ι y) eq-x ⟩
           (f $a x) · (ι y)    ≡⟨ cong (λ u → (f $a x) · u) eq-y ⟩
           (f $a x) · (f $a y) ≡⟨ sym (f.pres· _ _) ⟩
           f $a (x ·c y) ∎)
       (λ x eq-x →
           ι (-c x)    ≡⟨ refl ⟩
           - ι x       ≡⟨ cong (λ u → - u) eq-x ⟩
           - (f $a x)  ≡⟨ sym (f.pres- x) ⟩
           f $a (-c x) ∎)
      where
      ι = inducedMap A (evaluateAt f)
      module f = IsAlgebraHom (f .snd)

evaluateAt : {R : CommRing ℓ} {I : Type ℓ'} (A : CommAlgebra R ℓ'')
             (f : CommAlgebraHom (R [ I ]) A)
             → (I → fst A)
evaluateAt A f x = f $a (Construction.var x)

inducedHom : {R : CommRing ℓ} {I : Type ℓ'} (A : CommAlgebra R ℓ'')
             (φ : I → fst A )
             → CommAlgebraHom (R [ I ]) A
inducedHom A φ = Theory.inducedHom A φ

homMapIso : {R : CommRing ℓ} {I : Type ℓ} (A : CommAlgebra R ℓ')
             → Iso (CommAlgebraHom (R [ I ]) A) (I → (fst A))
Iso.fun (homMapIso A) = evaluateAt A
Iso.inv (homMapIso A) = inducedHom A
Iso.rightInv (homMapIso A) = λ ϕ → Theory.mapRetrievable A ϕ
Iso.leftInv (homMapIso {R = R} {I = I} A) =
  λ f → Σ≡Prop (λ f → isPropIsCommAlgebraHom {M = R [ I ]} {N = A} f)
               (Theory.homRetrievable A f)

homMapPath : {R : CommRing ℓ} {I : Type ℓ} (A : CommAlgebra R ℓ')
             → CommAlgebraHom (R [ I ]) A ≡ (I → fst A)
homMapPath A = isoToPath (homMapIso A)

module _ {R : CommRing ℓ} {A B : CommAlgebra R ℓ''} where
  open AlgebraHoms
  A′ = CommAlgebra→Algebra A
  B′ = CommAlgebra→Algebra B
  R′ = (CommRing→Ring R)
  ν : AlgebraHom A′ B′ → (⟨ A ⟩ → ⟨ B ⟩)
  ν φ = φ .fst

  {-
    Hom(R[I],A) → (I → A)
         ↓          ↓
    Hom(R[I],B) → (I → B)
  -}
  naturalR : {I : Type ℓ'} (ψ : CommAlgebraHom A B)
             (f : CommAlgebraHom (R [ I ]) A)
             → (fst ψ) ∘ evaluateAt A f ≡ evaluateAt B (ψ ∘a f)
  naturalR ψ f = refl

  {-
    Hom(R[I],A) → (I → A)
         ↓          ↓
    Hom(R[J],A) → (J → A)
  -}
  naturalL : {I J : Type ℓ'} (φ : J → I)
             (f : CommAlgebraHom (R [ I ]) A)
             → (evaluateAt A f) ∘ φ
               ≡ evaluateAt A (f ∘a (inducedHom (R [ I ]) (λ x → Construction.var (φ x))))
  naturalL φ f = refl

module _ {R : CommRing ℓ} where
  {-
    Prove that the FreeCommAlgebra over R on zero generators is
    isomorphic to the initial R-Algebra - R itsself.
  -}
  freeOn⊥ : CommAlgebraEquiv (R [ ⊥ ]) (initialCAlg R)
  freeOn⊥ =
     equivByInitiality
        R (R [ ⊥ ])
          {- Show that R[⊥] has the universal property of the
             initial R-Algbera and conclude that those are isomorphic -}
        λ B →  let to : CommAlgebraHom (R [ ⊥ ]) B → (⊥ → fst B)
                   to = evaluateAt B

                   from :  (⊥ → fst B) → CommAlgebraHom (R [ ⊥ ]) B
                   from = inducedHom B

                   from-to : (x : _) → from (to x) ≡ x
                   from-to x =
                     Σ≡Prop (λ f → isPropIsCommAlgebraHom {M = R [ ⊥ ]} {N = B} f)
                            (Theory.homRetrievable B x)

                   equiv : CommAlgebraHom (R [ ⊥ ]) B ≃ (⊥ → fst B)
                   equiv =
                     isoToEquiv
                       (iso to from (λ x → isContr→isOfHLevel 1 isContr⊥→A _ _) from-to)
               in isOfHLevelRespectEquiv 0 (invEquiv equiv) isContr⊥→A

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
------------------------------------------------------------------------
-- Encoders and decoders
------------------------------------------------------------------------

open import Atom

module Coding (atoms : χ-atoms) where

open import Equality.Propositional
open import Prelude hiding (const)
open import Tactic.By.Propositional

open import Bijection equality-with-J as Bijection using (_↔_)
open import Equality.Decision-procedures equality-with-J
open import Function-universe equality-with-J hiding (id; _∘_)
open import Injection equality-with-J using (Injective)
open import List equality-with-J using (foldr)
open import Maybe equality-with-J
open import Monad equality-with-J

open import Chi            atoms
open import Constants      atoms
open import Free-variables atoms
open import Values         atoms

open χ-atoms atoms

------------------------------------------------------------------------
-- General definitions

-- Representation functions.

record Rep {a b} (A : Type a) (B : Type b) : Type (a ⊔ b) where
  field
    -- Representation function.
    ⌜_⌝ : A → B

    -- ⌜_⌝ is injective.
    rep-injective : Injective ⌜_⌝

open Rep ⦃ … ⦄ public

-- An identity encoder.

id-rep : ∀ {a} {A : Type a} → Rep A A
id-rep = record
  { ⌜_⌝           = id
  ; rep-injective = id
  }

-- Composition of representation functions.

infixr 9 _∘-rep_

_∘-rep_ : ∀ {a b c} {A : Type a} {B : Type b} {C : Type c} →
          Rep B C → Rep A B → Rep A C
r₁ ∘-rep r₂ = record
  { ⌜_⌝           = R₁.⌜_⌝ ∘ R₂.⌜_⌝
  ; rep-injective = λ {x y} →
      R₁.⌜ R₂.⌜ x ⌝ ⌝ ≡ R₁.⌜ R₂.⌜ y ⌝ ⌝  ↝⟨ R₁.rep-injective ⟩
      R₂.⌜ x ⌝ ≡ R₂.⌜ y ⌝                ↝⟨ R₂.rep-injective ⟩□
      x ≡ y                              □
  }
  where
  module R₁ = Rep r₁
  module R₂ = Rep r₂

-- Encoder/decoder pairs.

record Code {a b} (A : Type a) (B : Type b) : Type (a ⊔ b) where
  field
    -- Encoder.
    code : A → B

    -- Partial decoder.
    decode : B → Maybe A

    -- The decoder must decode encoded values successfully.
    decode∘code : ∀ x → decode (code x) ≡ just x

  -- The encoder is injective.

  code-injective : Injective code
  code-injective {x} {y} eq = ⊎.cancel-inj₂ (
    just x           ≡⟨ by decode∘code ⟩
    decode (code x)  ≡⟨ by eq ⟩
    decode (code y)  ≡⟨ by decode∘code ⟩∎
    just y           ∎)

  -- Encoder/decoder pairs can be turned into representation
  -- functions.

  rep : Rep A B
  rep = record
    { ⌜_⌝           = code
    ; rep-injective = code-injective
    }

open Code ⦃ … ⦄ public

-- Converts bijections to encoders.

↔→Code : ∀ {a b} {A : Type a} {B : Type b} → A ↔ B → Code A B
↔→Code A↔B = record
  { code        = to
  ; decode      = λ b → just (from b)
  ; decode∘code = λ a →
      just (from (to a))  ≡⟨ cong just (left-inverse-of a) ⟩
      just a              ∎
  }
  where
  open _↔_ A↔B

-- An identity encoder.

id-code : ∀ {a} {A : Type a} → Code A A
id-code = ↔→Code Bijection.id

-- Composition of encoders.

infixr 9 _∘-code_

_∘-code_ : ∀ {a b c} {A : Type a} {B : Type b} {C : Type c} →
           Code B C → Code A B → Code A C
c₁ ∘-code c₂ = record
  { code        = C₁.code ∘ C₂.code
  ; decode      = λ c → C₁.decode c >>=′ C₂.decode
  ; decode∘code = λ a →
      C₁.decode (C₁.code (C₂.code a)) >>=′ C₂.decode  ≡⟨ cong (_>>=′ _) (C₁.decode∘code (C₂.code a)) ⟩
      return (C₂.code a) >>=′ C₂.decode               ≡⟨⟩
      C₂.decode (C₂.code a)                           ≡⟨ by C₂.decode∘code ⟩∎
      return a                                        ∎
  }
  where
  module C₁ = Code c₁
  module C₂ = Code c₂

------------------------------------------------------------------------
-- Some general definitions related to χ

-- Constructor applications can be encoded as expressions (that are
-- also constructor applications).

code-Consts : ∃ λ (cd : Code Consts Exp) →
                ∀ c → Constructor-application (Code.code cd c)
code-Consts = record
  { code        = cd
  ; decode      = dc
  ; decode∘code = dc∘cd
  } , cd-cs
  where
  mutual

    cd : Consts → Exp
    cd (const c cs) = const c (cd⋆ cs)

    cd⋆ : List Consts → List Exp
    cd⋆ []       = []
    cd⋆ (c ∷ cs) = cd c ∷ cd⋆ cs

  mutual

    cd-cs : ∀ c → Constructor-application (cd c)
    cd-cs (const c cs) = const c (cd⋆-cs cs)

    cd⋆-cs : ∀ cs → Constructor-applications (cd⋆ cs)
    cd⋆-cs []       = []
    cd⋆-cs (c ∷ cs) = cd-cs c ∷ cd⋆-cs cs

  mutual

    dc : Exp → Maybe Consts
    dc (const c es) = const c ⟨$⟩ dc⋆ es
    dc _            = nothing

    dc⋆ : List Exp → Maybe (List Consts)
    dc⋆ []       = return []
    dc⋆ (e ∷ es) = _∷_ ⟨$⟩ dc e ⊛ dc⋆ es

  mutual

    dc∘cd : ∀ c → dc (cd c) ≡ just c
    dc∘cd (const c cs) =
      const c ⟨$⟩ ⟨ dc⋆ (cd⋆ cs) ⟩  ≡⟨ ⟨by⟩ (dc∘cd⋆ cs) ⟩
      const c ⟨$⟩ return cs         ≡⟨ refl ⟩∎
      return (const c cs)           ∎

    dc∘cd⋆ : ∀ cs → dc⋆ (cd⋆ cs) ≡ just cs
    dc∘cd⋆ [] = refl
    dc∘cd⋆ (c ∷ cs) =
      _∷_ ⟨$⟩ ⟨ dc (cd c) ⟩ ⊛ dc⋆ (cd⋆ cs)  ≡⟨ ⟨by⟩ (dc∘cd c) ⟩
      _∷_ ⟨$⟩ return c ⊛ ⟨ dc⋆ (cd⋆ cs) ⟩   ≡⟨ ⟨by⟩ (dc∘cd⋆ cs) ⟩
      _∷_ ⟨$⟩ return c ⊛ return cs          ≡⟨⟩
      return (c ∷ cs)                       ∎

-- Converts instances of the form Rep A Consts to Rep A Exp.

rep-Consts-Exp : ∀ {a} {A : Type a} ⦃ r : Rep A Consts ⦄ →
                 Rep A Exp
rep-Consts-Exp ⦃ r ⦄ = rep ⦃ proj₁ code-Consts ⦄ ∘-rep r

-- Represents something as an expression.

rep-as-Exp : ∀ {a} {A : Type a} ⦃ r : Rep A Consts ⦄ → A → Exp
rep-as-Exp = ⌜_⌝ ⦃ rep-Consts-Exp ⦄

-- rep-as-Exp returns constructor applications.

rep-const :
  ∀ {a} {A : Type a} ⦃ r : Rep A Consts ⦄
  (x : A) → Constructor-application (rep-as-Exp x)
rep-const = proj₂ code-Consts ∘ ⌜_⌝

-- rep-as-Exp returns closed expressions.

rep-closed :
  ∀ {a} {A : Type a} ⦃ r : Rep A Consts ⦄
  (x : A) → Closed (rep-as-Exp x)
rep-closed = const→closed ∘ rep-const

-- Constructor applications can be encoded as closed expressions.

code-Consts-Closed : Code Consts Closed-exp
Code.code code-Consts-Closed c =
  code ⦃ r = proj₁ code-Consts ⦄ c , const→closed (proj₂ code-Consts c)

Code.decode code-Consts-Closed (e , _) =
  decode ⦃ r = proj₁ code-Consts ⦄ e

Code.decode∘code code-Consts-Closed c =
  decode ⦃ r = proj₁ code-Consts ⦄ (code ⦃ r = proj₁ code-Consts ⦄ c)  ≡⟨ decode∘code ⦃ r = proj₁ code-Consts ⦄ c ⟩∎
  just c                                                              ∎

-- Converts instances of the form Rep A Consts to Rep A Closed-exp.

rep-Consts-Closed-exp :
  ∀ {a} {A : Type a} ⦃ r : Rep A Consts ⦄ → Rep A Closed-exp
rep-Consts-Closed-exp ⦃ r ⦄ = rep ⦃ r = code-Consts-Closed ⦄ ∘-rep r

-- rep-as-Exp returns values.

rep-value :
  ∀ {a} {A : Type a} ⦃ r : Rep A Consts ⦄
  (x : A) → Value (rep-as-Exp x)
rep-value = const→value ∘ rep-const

-- Some derived lemmas.

subst-rep :
  ∀ {a} {A : Type a} ⦃ r : Rep A Consts ⦄ (x : A) {y e} →
  rep-as-Exp x [ y ← e ] ≡ rep-as-Exp x
subst-rep x = subst-closed _ _ (rep-closed x)

substs-rep :
  ∀ {a} {A : Type a} ⦃ r : Rep A Consts ⦄ (x : A) ps →
  foldr (λ ye → _[ proj₁ ye ← proj₂ ye ]) (rep-as-Exp x) ps ≡
  rep-as-Exp x
substs-rep x = substs-closed (rep-as-Exp x) (rep-closed x)

rep⇓rep :
  ∀ {a} {A : Type a} ⦃ r : Rep A Consts ⦄
  (x : A) → rep-as-Exp x ⇓ rep-as-Exp x
rep⇓rep x = values-compute-to-themselves (rep-value x)

rep⇓≡rep :
  ∀ {a} {A : Type a} ⦃ r : Rep A Consts ⦄ {v}
  (x : A) → rep-as-Exp x ⇓ v → rep-as-Exp x ≡ v
rep⇓≡rep x = values-only-compute-to-themselves (rep-value x)

------------------------------------------------------------------------
-- Specifications of how a number of types are encoded as χ
-- constructor applications

-- Encoder for booleans.

code-Bool : Code Bool Consts
code-Bool = record
  { code        = cd
  ; decode      = dc
  ; decode∘code = dc∘cd
  }
  where
  cd : Bool → Consts
  cd true  = const c-true  []
  cd false = const c-false []

  dc : Consts → Maybe Bool
  dc (const c args) with c-true C.≟ c | c-false C.≟ c
  dc (const c [])   | yes _ | _     = return true
  dc (const c [])   | _     | yes _ = return false
  dc (const c _)    | _     | _     = nothing

  dc∘cd : ∀ b → dc (cd b) ≡ just b
  dc∘cd true with c-true C.≟ c-true
  ... | yes _   = refl
  ... | no  t≢t = ⊥-elim (t≢t refl)
  dc∘cd false with c-true C.≟ c-false | c-false C.≟ c-false
  ... | no  _   | no f≢f = ⊥-elim (f≢f refl)
  ... | yes t≡f | _      = ⊥-elim (C.distinct-codes→distinct-names
                                     (λ ()) t≡f)
  ... | no _    | yes _  = refl

-- Encoder for natural numbers.

code-ℕ : Code ℕ Consts
code-ℕ = record
  { code        = cd
  ; decode      = dc
  ; decode∘code = dc∘cd
  }
  where
  cd : ℕ → Consts
  cd zero    = const c-zero []
  cd (suc n) = const c-suc (cd n ∷ [])

  dc : Consts → Maybe ℕ
  dc (const c args)     with c-zero C.≟ c | c-suc C.≟ c
  dc (const c [])       | yes eq | _      = return zero
  dc (const c (n ∷ [])) | _      | yes eq = map suc (dc n)
  dc (const c _)        | _      | _      = nothing

  dc∘cd : ∀ n → dc (cd n) ≡ just n
  dc∘cd zero with c-zero C.≟ c-zero
  ... | yes _   = refl
  ... | no  z≢z = ⊥-elim (z≢z refl)
  dc∘cd (suc n) with c-zero C.≟ c-suc | c-suc C.≟ c-suc
  ... | no  _   | no s≢s = ⊥-elim (s≢s refl)
  ... | yes z≡s | _      = ⊥-elim (C.distinct-codes→distinct-names
                                     (λ ()) z≡s)
  ... | no _    | yes _  =
    map suc ⟨ dc (cd n) ⟩  ≡⟨ ⟨by⟩ (dc∘cd n) ⟩
    map suc (return n)     ≡⟨ refl ⟩∎
    return (suc n)         ∎

-- Encoder for variables.

code-Var : Code Var Consts
code-Var = code-ℕ ∘-code ↔→Code V.countably-infinite

-- Encoder for constants.

code-Const : Code Const Consts
code-Const = code-ℕ ∘-code ↔→Code C.countably-infinite

-- Encoders for products.

module _ {a b} {A : Type a} {B : Type b} where

  private

    encode : (A → Consts) → (B → Consts) → A × B → Consts
    encode encA encB (x , y) = const c-pair (encA x ∷ encB y ∷ [])

  rep-× : ⦃ r : Rep A Consts ⦄ ⦃ s : Rep B Consts ⦄ →
          Rep (A × B) Consts
  rep-× ⦃ r ⦄ ⦃ s ⦄ = record
    { ⌜_⌝           = encode ⌜_⌝ ⌜_⌝
    ; rep-injective = λ { {x₁ , x₂} {y₁ , y₂} →
        const c-pair (⌜ x₁ ⌝ ∷ ⌜ x₂ ⌝ ∷ []) ≡
        const c-pair (⌜ y₁ ⌝ ∷ ⌜ y₂ ⌝ ∷ [])    ↝⟨ lemma ⟩

        ⌜ x₁ ⌝ ≡ ⌜ y₁ ⌝ × ⌜ x₂ ⌝ ≡ ⌜ y₂ ⌝      ↝⟨ Σ-map rep-injective rep-injective ⟩

        x₁ ≡ y₁ × x₂ ≡ y₂                      ↝⟨ uncurry (cong₂ _,_) ⟩□

        (x₁ , x₂) ≡ (y₁ , y₂)                  □ }
    }
    where
    lemma :
      ∀ {c₁ c₂ x₁ x₂ y₁ y₂} →
      Consts.const c₁ (x₁ ∷ x₂ ∷ []) ≡ const c₂ (y₁ ∷ y₂ ∷ []) →
      x₁ ≡ y₁ × x₂ ≡ y₂
    lemma refl = refl , refl

  code-× : ⦃ c : Code A Consts ⦄ ⦃ d : Code B Consts ⦄ →
           Code (A × B) Consts
  code-× = record
    { code        = cd
    ; decode      = dc
    ; decode∘code = dc∘cd
    }
    where
    cd : A × B → Consts
    cd = encode code code

    dc : Consts → Maybe (A × B)
    dc (const c args)         with c-pair C.≟ c
    dc (const c (x ∷ y ∷ [])) | yes _ = decode x >>=′ λ x →
                                        decode y >>=′ λ y →
                                        just (x , y)
    dc (const c args)         | _     = nothing

    dc∘cd : ∀ x → dc (cd x) ≡ just x
    dc∘cd (x , y) with c-pair C.≟ c-pair
    ... | no p≢p = ⊥-elim (p≢p refl)
    ... | yes _  =
      (⟨ decode (code x) ⟩ >>=′ λ x →
       decode (code y) >>=′ λ y →
       just (x , y))                      ≡⟨ ⟨by⟩ decode∘code ⟩

      (return x >>=′ λ x →
       decode (code y) >>=′ λ y →
       just (x , y))                      ≡⟨⟩

      (⟨ decode (code y) ⟩ >>=′ λ y →
       just (x , y))                      ≡⟨ ⟨by⟩ decode∘code ⟩

      (return y >>=′ λ y → just (x , y))  ≡⟨ refl ⟩∎

      return (x , y)                      ∎

-- Encoders for lists.

module _ {a} {A : Type a} where

  private

    encode : (A → Consts) → List A → Consts
    encode enc []       = const c-nil []
    encode enc (x ∷ xs) = const c-cons (enc x ∷ encode enc xs ∷ [])

  rep-List : ⦃ r : Rep A Consts ⦄ → Rep (List A) Consts
  rep-List = record
    { ⌜_⌝           = encode ⌜_⌝
    ; rep-injective = injective
    }
    where
    injective : ∀ {xs ys} → encode ⌜_⌝ xs ≡ encode ⌜_⌝ ys → xs ≡ ys
    injective {[]}     {[]}     = λ _ → refl
    injective {[]}     {_ ∷ _}  = λ ()
    injective {_ ∷ _}  {[]}     = λ ()
    injective {x ∷ xs} {y ∷ ys} =
      const c-cons (⌜ x ⌝ ∷ encode ⌜_⌝ xs ∷ []) ≡
      const c-cons (⌜ y ⌝ ∷ encode ⌜_⌝ ys ∷ [])      ↝⟨ lemma ⟩

      ⌜ x ⌝ ≡ ⌜ y ⌝ × encode ⌜_⌝ xs ≡ encode ⌜_⌝ ys  ↝⟨ Σ-map rep-injective injective ⟩

      x ≡ y × xs ≡ ys                                ↝⟨ uncurry (cong₂ _∷_) ⟩□

      x ∷ xs ≡ y ∷ ys                                □
      where
      lemma :
        ∀ {c₁ x₁ y₁ c₂ x₂ y₂} →
        Consts.const c₁ (x₁ ∷ y₁ ∷ []) ≡ const c₂ (x₂ ∷ y₂ ∷ []) →
        x₁ ≡ x₂ × y₁ ≡ y₂
      lemma refl = refl , refl

  code-List : ⦃ c : Code A Consts ⦄ → Code (List A) Consts
  code-List = record
    { code        = cd
    ; decode      = dc
    ; decode∘code = dc∘cd
    }
    where
    cd : List A → Consts
    cd = encode code

    dc : Consts → Maybe (List A)
    dc (const c args)           with c-nil C.≟ c | c-cons C.≟ c
    dc (const c [])             | yes eq | _      = return []
    dc (const c′ (x ∷ xs ∷ [])) | _      | yes eq =
      _∷_ ⟨$⟩ decode x ⊛ dc xs
    dc (const c args) | _ | _ = nothing

    dc∘cd : ∀ x → dc (cd x) ≡ just x
    dc∘cd [] with c-nil C.≟ c-nil
    ... | yes _   = refl
    ... | no  n≢n = ⊥-elim (n≢n refl)
    dc∘cd (x ∷ xs) with c-nil C.≟ c-cons | c-cons C.≟ c-cons
    ... | no _    | no c≢c = ⊥-elim (c≢c refl)
    ... | yes n≡c | _      = ⊥-elim (C.distinct-codes→distinct-names
                                       (λ ()) n≡c)
    ... | no _    | yes _  =
      _∷_ ⟨$⟩ ⟨ decode (code x) ⟩ ⊛ dc (cd xs)  ≡⟨ ⟨by⟩ decode∘code ⟩
      _∷_ ⟨$⟩ return x ⊛ ⟨ dc (cd xs) ⟩         ≡⟨ ⟨by⟩ (dc∘cd xs) ⟩
      _∷_ ⟨$⟩ return x ⊛ return xs              ≡⟨⟩
      return (x ∷ xs)                           ∎

-- Encoder for lists of variables.

code-Var⋆ : Code (List Var) Consts
code-Var⋆ = code-List ⦃ code-Var ⦄

private

  module Var   = Code code-Var
  module Var⋆  = Code code-Var⋆
  module Const = Code code-Const

  -- Encoder for the abstract syntax.

  mutual

    code-E : Exp → Consts
    code-E (apply e₁ e₂) = const c-apply (code-E e₁ ∷ code-E e₂ ∷ [])
    code-E (lambda x e)  = const c-lambda (code ⦃ code-Var ⦄ x ∷ code-E e ∷ [])
    code-E (case e bs)   = const c-case (code-E e ∷ code-B⋆ bs ∷ [])
    code-E (rec x e)     = const c-rec (code ⦃ code-Var ⦄ x ∷ code-E e ∷ [])
    code-E (var x)       = const c-var (code ⦃ code-Var ⦄ x ∷ [])
    code-E (const c es)  = const c-const (code ⦃ code-Const ⦄ c ∷ code-⋆ es ∷ [])

    code-B : Br → Consts
    code-B (branch c xs e) =
      const c-branch
        (code ⦃ code-Const ⦄ c ∷ code ⦃ code-Var⋆ ⦄ xs ∷ code-E e ∷ [])

    -- TODO: One could presumably use sized types to avoid repetitive
    -- code. However, I did not want to use sized types in the
    -- specification of χ.

    code-⋆ : List Exp → Consts
    code-⋆ []       = const c-nil []
    code-⋆ (e ∷ es) = const c-cons (code-E e ∷ code-⋆ es ∷ [])

    code-B⋆ : List Br → Consts
    code-B⋆ []       = const c-nil []
    code-B⋆ (b ∷ bs) = const c-cons (code-B b ∷ code-B⋆ bs ∷ [])

  mutual

    decode-E : Consts → Maybe Exp
    decode-E (const c args) with c-apply  C.≟ c
                               | c-lambda C.≟ c
                               | c-case   C.≟ c
                               | c-rec    C.≟ c
                               | c-var    C.≟ c
                               | c-const  C.≟ c

    decode-E (const c (e₁ ∷ e₂ ∷ [])) | yes eq | _ | _ | _ | _ | _ =
      apply ⟨$⟩ decode-E e₁ ⊛ decode-E e₂

    decode-E (const c (x ∷ e ∷ [])) | _ | yes eq | _ | _ | _ | _ =
      lambda ⟨$⟩ decode ⦃ code-Var ⦄ x ⊛ decode-E e

    decode-E (const c (e ∷ bs ∷ [])) | _ | _ | yes eq | _ | _ | _ =
      case ⟨$⟩ decode-E e ⊛ decode-B⋆ bs

    decode-E (const c (x ∷ e ∷ [])) | _ | _ | _ | yes eq | _ | _ =
      rec ⟨$⟩ decode ⦃ code-Var ⦄ x ⊛ decode-E e

    decode-E (const c (x ∷ [])) | _ | _ | _ | _ | yes eq | _ =
      var ⟨$⟩ decode ⦃ code-Var ⦄ x

    decode-E (const c (c′ ∷ es ∷ [])) | _ | _ | _ | _ | _ | yes eq =
      const ⟨$⟩ decode ⦃ code-Const ⦄ c′ ⊛ decode-⋆ es

    decode-E (const c args) | _ | _ | _ | _ | _ | _ = nothing

    decode-B : Consts → Maybe Br
    decode-B (const c args)               with c-branch C.≟ c
    decode-B (const c (c′ ∷ xs ∷ e ∷ [])) | yes eq =
      branch ⟨$⟩ decode ⦃ code-Const ⦄ c′
               ⊛ decode ⦃ code-Var⋆ ⦄ xs
               ⊛ decode-E e
    decode-B (const c args) | _ = nothing

    decode-⋆ : Consts → Maybe (List Exp)
    decode-⋆ (const c args)           with c-nil C.≟ c | c-cons C.≟ c
    decode-⋆ (const c [])             | yes eq | _      = return []
    decode-⋆ (const c′ (e ∷ es ∷ [])) | _      | yes eq =
      _∷_ ⟨$⟩ decode-E e ⊛ decode-⋆ es
    decode-⋆ (const c args) | _ | _ = nothing

    decode-B⋆ : Consts → Maybe (List Br)
    decode-B⋆ (const c args)           with c-nil C.≟ c | c-cons C.≟ c
    decode-B⋆ (const c [])             | yes eq | _      = return []
    decode-B⋆ (const c′ (b ∷ bs ∷ [])) | _      | yes eq =
      _∷_ ⟨$⟩ decode-B b ⊛ decode-B⋆ bs
    decode-B⋆ (const c args) | _ | _ = nothing

  mutual

    decode∘code-E : ∀ e → decode-E (code-E e) ≡ just e

    decode∘code-E (apply e₁ e₂) with c-apply C.≟ c-apply
    ... | no c≢c = ⊥-elim (c≢c refl)
    ... | yes _  =
      apply ⟨$⟩ ⟨ decode-E (code-E e₁) ⟩ ⊛ decode-E (code-E e₂)  ≡⟨ ⟨by⟩ (decode∘code-E e₁) ⟩
      apply ⟨$⟩ return e₁ ⊛ ⟨ decode-E (code-E e₂) ⟩             ≡⟨ ⟨by⟩ (decode∘code-E e₂) ⟩
      apply ⟨$⟩ return e₁ ⊛ return e₂                            ≡⟨⟩
      return (apply e₁ e₂)                                       ∎

    decode∘code-E (lambda x e) with c-apply  C.≟ c-lambda
                                  | c-lambda C.≟ c-lambda
    ... | _       | no l≢l = ⊥-elim (l≢l refl)
    ... | yes a≡l | _      = ⊥-elim (C.distinct-codes→distinct-names
                                       (λ ()) a≡l)
    ... | no _    | yes _  =
      lambda ⟨$⟩ ⟨ Var.decode (code ⦃ code-Var ⦄ x) ⟩ ⊛ decode-E (code-E e)  ≡⟨ ⟨by⟩ Var.decode∘code ⟩
      lambda ⟨$⟩ return x ⊛ ⟨ decode-E (code-E e) ⟩                          ≡⟨ ⟨by⟩ (decode∘code-E e) ⟩
      lambda ⟨$⟩ return x ⊛ return e                                         ≡⟨⟩
      return (lambda x e)                                                    ∎

    decode∘code-E (case e bs) with c-apply  C.≟ c-case
                                 | c-lambda C.≟ c-case
                                 | c-case   C.≟ c-case
    ... | _       | _       | no c≢c = ⊥-elim (c≢c refl)
    ... | _       | yes l≡c | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                 (λ ()) l≡c)
    ... | yes a≡c | _       | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                 (λ ()) a≡c)
    ... | no _    | no _    | yes _  =
      case ⟨$⟩ ⟨ decode-E (code-E e) ⟩ ⊛ decode-B⋆ (code-B⋆ bs)  ≡⟨ ⟨by⟩ (decode∘code-E e) ⟩
      case ⟨$⟩ return e ⊛ ⟨ decode-B⋆ (code-B⋆ bs) ⟩             ≡⟨ ⟨by⟩ (decode∘code-B⋆ bs) ⟩
      case ⟨$⟩ return e ⊛ return bs                              ≡⟨⟩
      return (case e bs)                                         ∎

    decode∘code-E (rec x e) with c-apply  C.≟ c-rec
                               | c-lambda C.≟ c-rec
                               | c-case   C.≟ c-rec
                               | c-rec    C.≟ c-rec
    ... | _       | _       | _       | no r≢r = ⊥-elim (r≢r refl)
    ... | _       | _       | yes c≡r | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                           (λ ()) c≡r)
    ... | _       | yes l≡r | _       | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                           (λ ()) l≡r)
    ... | yes a≡r | _       | _       | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                           (λ ()) a≡r)
    ... | no _    | no _    | no _    | yes _  =
      rec ⟨$⟩ ⟨ Var.decode (code ⦃ code-Var ⦄ x) ⟩ ⊛ decode-E (code-E e)  ≡⟨ ⟨by⟩ Var.decode∘code ⟩
      rec ⟨$⟩ return x ⊛ ⟨ decode-E (code-E e) ⟩                          ≡⟨ ⟨by⟩ (decode∘code-E e) ⟩
      rec ⟨$⟩ return x ⊛ return e                                         ≡⟨⟩
      return (rec x e)                                                    ∎

    decode∘code-E (var x) with c-apply  C.≟ c-var
                             | c-lambda C.≟ c-var
                             | c-case   C.≟ c-var
                             | c-rec    C.≟ c-var
                             | c-var    C.≟ c-var
    ... | _       | _       | _       | _       | no v≢v = ⊥-elim (v≢v refl)
    ... | _       | _       | _       | yes r≡v | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                                     (λ ()) r≡v)
    ... | _       | _       | yes c≡v | _       | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                                     (λ ()) c≡v)
    ... | _       | yes l≡v | _       | _       | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                                     (λ ()) l≡v)
    ... | yes a≡v | _       | _       | _       | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                                     (λ ()) a≡v)
    ... | no _    | no _    | no _    | no _    | yes _  =
      var ⟨$⟩ ⟨ Var.decode (code ⦃ code-Var ⦄ x) ⟩  ≡⟨ ⟨by⟩ Var.decode∘code ⟩
      var ⟨$⟩ return x                              ≡⟨ refl ⟩∎
      return (var x)                                ∎

    decode∘code-E (const c es) with c-apply  C.≟ c-const
                                  | c-lambda C.≟ c-const
                                  | c-case   C.≟ c-const
                                  | c-rec    C.≟ c-const
                                  | c-var    C.≟ c-const
                                  | c-const  C.≟ c-const
    ... | _       | _       | _       | _       | _       | no c≢c = ⊥-elim (c≢c refl)
    ... | _       | _       | _       | _       | yes v≡c | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                                               (λ ()) v≡c)
    ... | _       | _       | _       | yes r≡c | _       | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                                               (λ ()) r≡c)
    ... | _       | _       | yes c≡c | _       | _       | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                                               (λ ()) c≡c)
    ... | _       | yes l≡c | _       | _       | _       | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                                               (λ ()) l≡c)
    ... | yes a≡c | _       | _       | _       | _       | _      = ⊥-elim (C.distinct-codes→distinct-names
                                                                               (λ ()) a≡c)
    ... | no _    | no _    | no _    | no _    | no _    | yes _  =
      const ⟨$⟩ ⟨ Const.decode (code ⦃ code-Const ⦄ c) ⟩ ⊛
                decode-⋆ (code-⋆ es)                       ≡⟨ ⟨by⟩ Const.decode∘code ⟩

      const ⟨$⟩ return c ⊛ ⟨ decode-⋆ (code-⋆ es) ⟩        ≡⟨ ⟨by⟩ (decode∘code-⋆ es) ⟩

      const ⟨$⟩ return c ⊛ return es                       ≡⟨⟩

      return (const c es)                                  ∎

    decode∘code-B : ∀ b → decode-B (code-B b) ≡ just b
    decode∘code-B (branch c xs e) with c-branch C.≟ c-branch
    ... | no b≢b = ⊥-elim (b≢b refl)
    ... | yes _  =
      branch ⟨$⟩ ⟨ Const.decode (code ⦃ code-Const ⦄ c) ⟩ ⊛
                 Var⋆.decode (code ⦃ code-Var⋆ ⦄ xs) ⊛
                 decode-E (code-E e)                             ≡⟨ ⟨by⟩ Const.decode∘code ⟩

      branch ⟨$⟩ return c ⊛
                 ⟨ Var⋆.decode (code ⦃ code-Var⋆ ⦄ xs) ⟩ ⊛
                 decode-E (code-E e)                             ≡⟨ ⟨by⟩ Var⋆.decode∘code ⟩

      branch ⟨$⟩ return c ⊛ return xs ⊛ ⟨ decode-E (code-E e) ⟩  ≡⟨ ⟨by⟩ (decode∘code-E e) ⟩

      branch ⟨$⟩ return c ⊛ return xs ⊛ return e                 ≡⟨⟩

      return (branch c xs e)                                     ∎

    decode∘code-⋆ : ∀ es → decode-⋆ (code-⋆ es) ≡ just es
    decode∘code-⋆ [] with c-nil C.≟ c-nil
    ... | no  n≢n = ⊥-elim (n≢n refl)
    ... | yes _   = refl
    decode∘code-⋆ (e ∷ es) with c-nil C.≟ c-cons | c-cons C.≟ c-cons
    ... | no _    | no c≢c = ⊥-elim (c≢c refl)
    ... | yes n≡c | _      = ⊥-elim (C.distinct-codes→distinct-names
                                       (λ ()) n≡c)
    ... | no _    | yes _  =
      _∷_ ⟨$⟩ ⟨ decode-E (code-E e) ⟩ ⊛ decode-⋆ (code-⋆ es)  ≡⟨ ⟨by⟩ (decode∘code-E e) ⟩
      _∷_ ⟨$⟩ return e ⊛ ⟨ decode-⋆ (code-⋆ es) ⟩             ≡⟨ ⟨by⟩ (decode∘code-⋆ es) ⟩
      _∷_ ⟨$⟩ return e ⊛ return es                            ≡⟨⟩
      return (e ∷ es)                                         ∎

    decode∘code-B⋆ : ∀ bs → decode-B⋆ (code-B⋆ bs) ≡ just bs
    decode∘code-B⋆ [] with c-nil C.≟ c-nil
    ... | no  n≢n = ⊥-elim (n≢n refl)
    ... | yes _   = refl
    decode∘code-B⋆ (b ∷ bs) with c-nil C.≟ c-cons | c-cons C.≟ c-cons
    ... | no _    | no c≢c = ⊥-elim (c≢c refl)
    ... | yes n≡c | _      = ⊥-elim (C.distinct-codes→distinct-names
                                       (λ ()) n≡c)
    ... | no _    | yes _  =
      _∷_ ⟨$⟩ ⟨ decode-B (code-B b) ⟩ ⊛ decode-B⋆ (code-B⋆ bs)  ≡⟨ ⟨by⟩ (decode∘code-B b) ⟩
      _∷_ ⟨$⟩ return b ⊛ ⟨ decode-B⋆ (code-B⋆ bs) ⟩             ≡⟨ ⟨by⟩ (decode∘code-B⋆ bs) ⟩
      _∷_ ⟨$⟩ return b ⊛ return bs                              ≡⟨⟩
      return (b ∷ bs)                                           ∎

code-Exp : Code Exp Consts
Code.code        code-Exp = code-E
Code.decode      code-Exp = decode-E
Code.decode∘code code-Exp = decode∘code-E

code-Br : Code Br Consts
Code.code        code-Br = code-B
Code.decode      code-Br = decode-B
Code.decode∘code code-Br = decode∘code-B

code-Exps : Code (List Exp) Consts
Code.code        code-Exps = code-⋆
Code.decode      code-Exps = decode-⋆
Code.decode∘code code-Exps = decode∘code-⋆

code-Brs : Code (List Br) Consts
Code.code        code-Brs = code-B⋆
Code.decode      code-Brs = decode-B⋆
Code.decode∘code code-Brs = decode∘code-B⋆

-- Encoder for closed expressions.

code-Closed : Code Closed-exp Consts
Code.code   code-Closed = code ⦃ code-Exp ⦄ ∘ proj₁
Code.decode code-Closed c with decode ⦃ code-Exp ⦄ c
... | nothing = nothing
... | just e  with closed? e
...   | yes cl = just (e , cl)
...   | no _   = nothing
Code.decode∘code code-Closed (c , cl)
  with decode ⦃ r = code-Exp ⦄ (code ⦃ code-Exp ⦄ c)
     | decode∘code ⦃ r = code-Exp ⦄ c
... | .(just c) | refl with closed? c
...   | no  ¬cl = ⊥-elim (¬cl cl)
...   | yes cl′ =
  cong just (closed-equal-if-expressions-equal refl)

max_stars_repo_name: nad/chi

max_issues_repo_name: nad/chi

max_forks_repo_name: nad/chi


text:
-- Hilbert-style formalisation of closed syntax.
-- Sequences of terms.

module OldBasicILP.Syntax.ClosedHilbertSequential where

open import OldBasicILP.Syntax.Common public

-- Mutually-recursive declarations.

data Ty : Set

record Proof (Ξ : Cx Ty) (A : Ty) : Set

data ⊢ᴰ_ : Cx Ty → Set

_⧺ᴰ_ : ∀ {Ξ₁ Ξ₂} → ⊢ᴰ Ξ₁ → ⊢ᴰ Ξ₂ → ⊢ᴰ Ξ₁ ⧺ Ξ₂

-- Types parametrised by closed derivations.

infixr 10 _⦂_
infixl 9 _∧_
infixr 7 _▻_
data Ty where
  α_  : Atom → Ty
  _▻_ : Ty → Ty → Ty
  _⦂_ : ∀ {Ξ A} → Proof Ξ A → Ty → Ty
  _∧_ : Ty → Ty → Ty
  ⊤  : Ty

-- Anti-bug wrappers.

record Proof (Ξ : Cx Ty) (A : Ty) where
  inductive
  constructor [_]
  field
    der : ⊢ᴰ Ξ , A

-- More mutually-recursive declarations.

appᴰ : ∀ {Ξ₁ Ξ₂ A B} → ⊢ᴰ Ξ₁ , A ▻ B → ⊢ᴰ Ξ₂ , A → ⊢ᴰ (Ξ₂ , A) ⧺ (Ξ₁ , A ▻ B) , B

boxᴰ : ∀ {Ξ A} → (d : ⊢ᴰ Ξ , A) → ⊢ᴰ ∅ , [ d ] ⦂ A

-- Derivations.

infix 3 ⊢ᴰ_
data ⊢ᴰ_ where
  nil   : ⊢ᴰ ∅
  mp    : ∀ {Ξ A B}   → A ▻ B ∈ Ξ → A ∈ Ξ → ⊢ᴰ Ξ → ⊢ᴰ Ξ , B
  ci    : ∀ {Ξ A}     → ⊢ᴰ Ξ → ⊢ᴰ Ξ , A ▻ A
  ck    : ∀ {Ξ A B}   → ⊢ᴰ Ξ → ⊢ᴰ Ξ , A ▻ B ▻ A
  cs    : ∀ {Ξ A B C} → ⊢ᴰ Ξ → ⊢ᴰ Ξ , (A ▻ B ▻ C) ▻ (A ▻ B) ▻ A ▻ C

  nec   : ∀ {Ξ A}     → ∀ {`Ξ} → (`d : ⊢ᴰ `Ξ , A)
                      → ⊢ᴰ Ξ → ⊢ᴰ Ξ , [ `d ] ⦂ A

  cdist : ∀ {Ξ A B}   → ∀ {`Ξ₁ `Ξ₂} → {`d₁ : ⊢ᴰ `Ξ₁ , A ▻ B} → {`d₂ : ⊢ᴰ `Ξ₂ , A}
                      → ⊢ᴰ Ξ → ⊢ᴰ Ξ , [ `d₁ ] ⦂ (A ▻ B) ▻ [ `d₂ ] ⦂ A ▻ [ appᴰ `d₁ `d₂ ] ⦂ B

  cup   : ∀ {Ξ A}     → ∀ {`Ξ} → {`d : ⊢ᴰ `Ξ , A}
                      → ⊢ᴰ Ξ → ⊢ᴰ Ξ , [ `d ] ⦂ A ▻ [ boxᴰ `d ] ⦂ [ `d ] ⦂ A

  cdown : ∀ {Ξ A}     → ∀ {`Ξ} → {`d : ⊢ᴰ `Ξ , A}
                      → ⊢ᴰ Ξ → ⊢ᴰ Ξ , [ `d ] ⦂ A ▻ A

  cpair : ∀ {Ξ A B}   → ⊢ᴰ Ξ → ⊢ᴰ Ξ , A ▻ B ▻ A ∧ B
  cfst  : ∀ {Ξ A B}   → ⊢ᴰ Ξ → ⊢ᴰ Ξ , A ∧ B ▻ A
  csnd  : ∀ {Ξ A B}   → ⊢ᴰ Ξ → ⊢ᴰ Ξ , A ∧ B ▻ B
  unit  : ∀ {Ξ}       → ⊢ᴰ Ξ → ⊢ᴰ Ξ , ⊤

-- Anti-bug wrappers.

infix 3 ⊢_
⊢_ : Ty → Set
⊢ A = ∃ (λ Ξ → ⊢ᴰ Ξ , A)

-- Concatenation of derivations.

d₁ ⧺ᴰ nil       = d₁
d₁ ⧺ᴰ mp i j d₂ = mp (mono∈ weak⊆⧺₂ i) (mono∈ weak⊆⧺₂ j) (d₁ ⧺ᴰ d₂)
d₁ ⧺ᴰ ci d₂     = ci (d₁ ⧺ᴰ d₂)
d₁ ⧺ᴰ ck d₂     = ck (d₁ ⧺ᴰ d₂)
d₁ ⧺ᴰ cs d₂     = cs (d₁ ⧺ᴰ d₂)
d₁ ⧺ᴰ nec `d d₂ = nec `d (d₁ ⧺ᴰ d₂)
d₁ ⧺ᴰ cdist d₂  = cdist (d₁ ⧺ᴰ d₂)
d₁ ⧺ᴰ cup d₂    = cup (d₁ ⧺ᴰ d₂)
d₁ ⧺ᴰ cdown d₂  = cdown (d₁ ⧺ᴰ d₂)
d₁ ⧺ᴰ cpair d₂  = cpair (d₁ ⧺ᴰ d₂)
d₁ ⧺ᴰ cfst d₂   = cfst (d₁ ⧺ᴰ d₂)
d₁ ⧺ᴰ csnd d₂   = csnd (d₁ ⧺ᴰ d₂)
d₁ ⧺ᴰ unit d₂   = unit (d₁ ⧺ᴰ d₂)

-- Modus ponens and necessitation in nested form.

appᴰ {Ξ₁} {Ξ₂} {A} {B} d₁ d₂ = mp top (mono∈ (weak⊆⧺₁ (Ξ₁ , A ▻ B)) top) (d₂ ⧺ᴰ d₁)

boxᴰ {Ξ} {A} d = nec d nil

app : ∀ {A B} → ⊢ A ▻ B → ⊢ A → ⊢ B
app {A} {B} (Ξ₁ , d₁) (Ξ₂ , d₂) = Ξ₃ , d₃
  where Ξ₃ = (Ξ₂ , A) ⧺ (Ξ₁ , A ▻ B)
        d₃ = appᴰ d₁ d₂

box : ∀ {A} → (t : ⊢ A) → ⊢ [ π₂ t ] ⦂ A
box (Ξ , d) = ∅ , boxᴰ d

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
------------------------------------------------------------------------
-- Some types and functions used by several parser variants
------------------------------------------------------------------------

module Utilities where

open import Data.Product
open import Data.List
open import Data.Function using (flip)

------------------------------------------------------------------------
-- Associativity

-- Used to specify how chain₁, chain and chain≥ should apply the
-- parsed operators: left or right associatively.

data Assoc : Set where
  left  : Assoc
  right : Assoc

------------------------------------------------------------------------
-- Post-processing for the chain parsers

-- Application.

appʳ : forall {r} -> r × (r -> r -> r) -> r -> r
appʳ (x , _•_) y = x • y

appˡ : forall {r} -> r -> (r -> r -> r) × r -> r
appˡ x (_•_ , y) = x • y

-- Shifting. See Examples below for an illuminating example.

shiftˡ : forall {a b} -> List (a × b) -> a -> a × List (b × a)
shiftˡ []                x  = (x , [])
shiftˡ ((x₁ , x₂) ∷ xs₃) x₄ = (x₁ , (x₂ , proj₁ x₃xs₄) ∷ proj₂ x₃xs₄)
  where x₃xs₄ = shiftˡ xs₃ x₄

-- The post-processing function. See Examples below for some
-- illuminating examples.

chain₁-combine : forall {r} ->
                 Assoc -> List (r × (r -> r -> r)) -> r -> r
chain₁-combine right xs y = foldr appʳ y xs
chain₁-combine left  xs y with shiftˡ xs y
... | (x , ys) = foldl appˡ x ys

-- Variants.

shiftʳ : forall {a b} -> a -> List (b × a) -> List (a × b) × a
shiftʳ x  []                = ([] , x)
shiftʳ x₁ ((x₂ , x₃) ∷ xs₄) = ((x₁ , x₂) ∷ proj₁ xs₃x₄ , proj₂ xs₃x₄)
  where xs₃x₄ = shiftʳ x₃ xs₄

chain≥-combine : forall {r} ->
                 Assoc -> r -> List ((r -> r -> r) × r) -> r
chain≥-combine left  x ys = foldl appˡ x ys
chain≥-combine right x ys with shiftʳ x ys
... | (xs , y) = foldr appʳ y xs

private
 module Examples {r s : Set}
                 (x y z : r)
                 (A B : s)
                 (_+_ _*_ : r -> r -> r)
                 where

  open import Relation.Binary.PropositionalEquality

  ex₁ : shiftˡ ((x , A) ∷ (y , B) ∷ []) z ≡ (x , ((A , y) ∷ (B , z) ∷ []))
  ex₁ = refl

  ex₁ʳ : chain₁-combine right ((x , _+_) ∷ (y , _*_) ∷ []) z ≡ x + (y * z)
  ex₁ʳ = refl

  ex₁ˡ : chain₁-combine left  ((x , _+_) ∷ (y , _*_) ∷ []) z ≡ (x + y) * z
  ex₁ˡ = refl

  ex≥ : shiftʳ x ((A , y) ∷ (B , z) ∷ []) ≡ ((x , A) ∷ (y , B) ∷ [] , z)
  ex≥ = refl

  ex≥ʳ : chain≥-combine right x ((_+_ , y) ∷ (_*_ , z) ∷ []) ≡ x + (y * z)
  ex≥ʳ = refl

  ex≥ˡ : chain≥-combine left  x ((_+_ , y) ∷ (_*_ , z) ∷ []) ≡ (x + y) * z
  ex≥ˡ = refl

------------------------------------------------------------------------
-- Some suitably typed composition operators

infixr 9 _∘′_ _∘₂_

_∘′_ : {a c : Set} {b : a -> Set1} ->
       (forall {x} -> b x -> c) -> ((x : a) -> b x) -> (a -> c)
f ∘′ g = \x -> f (g x)

_∘₂_ : {a b c : Set2} -> (b -> c) -> (a -> b) -> (a -> c)
f ∘₂ g = \x -> f (g x)

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Foundations.Pointed.Base where

open import Cubical.Foundations.Prelude

Pointed : (ℓ : Level) → Type (ℓ-suc ℓ)
Pointed ℓ = Σ[ A ∈ Type ℓ ] A

typ : ∀ {ℓ} (A∙ : Pointed ℓ) → Type ℓ
typ = fst

pt : ∀ {ℓ} (A∙ : Pointed ℓ) → typ A∙
pt = snd

max_stars_repo_name: oisdk/cubical

max_issues_repo_name: oisdk/cubical

max_forks_repo_name: oisdk/cubical


text:
module Oscar.Class.Substitution where

open import Oscar.Data.Equality
open import Oscar.Function
open import Oscar.Relation
open import Oscar.Level

record Substitution {a} {A : Set a} {b} (B : A → Set b) {c} (C : A → Set c) : Set (a ⊔ b ⊔ c) where
  field
    ε : ∀ {m} → B m → C m
    _◇_ : ∀ {l m n} → (g : B m → C n) (f : B l → C m) → B l → C n
    ◇-left-identity : ∀ {m n} → (f : B m → C n) → ε ◇ f ≡̇ f
    ◇-right-identity : ∀ {m n} → (f : B m → C n) → f ◇ ε ≡̇ f
    ◇-associativity : ∀ {k l m n} (f : B k → C l) (g : B l → C m) (h : B m → C n) → h ◇ (g ◇ f) ≡̇ (h ◇ g) ◇ f

open Substitution ⦃ … ⦄ public

{-# DISPLAY Substitution._◇_ _ = _◇_ #-}

instance Substitution-id : ∀ {a} {A : Set a} {bc} {BC : A → Set bc} → Substitution BC BC
Substitution.ε Substitution-id = id
Substitution._◇_ Substitution-id g f = g ∘ f
Substitution.◇-left-identity Substitution-id _ _ = refl
Substitution.◇-right-identity Substitution-id _ _ = refl
Substitution.◇-associativity Substitution-id _ _ _ _ = refl


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Numbers.Naturals.Naturals
open import Numbers.Naturals.Multiplication
open import Numbers.Integers.Order
open import Numbers.Integers.RingStructure.Ring
open import Numbers.Integers.RingStructure.IntegralDomain
open import Semirings.Definition
open import Rings.EuclideanDomains.Definition
open import Orders.Total.Definition
open import Numbers.Naturals.EuclideanAlgorithm

module Numbers.Integers.RingStructure.EuclideanDomain where

private
  norm : ℤ → ℕ
  norm (nonneg x) = x
  norm (negSucc x) = succ x

  norm' : {a : ℤ} → (a!=0 : (a ≡ nonneg 0) → False) → ℕ
  norm' {a} _ = norm a

  multiplyIncreasesSuccLemma : (a b : ℕ) → succ (succ a) <N (succ (succ a)) *N (succ (succ b))
  multiplyIncreasesSuccLemma a b with multiplyIncreases (succ (succ b)) (succ (succ a)) (le b (applyEquality succ (Semiring.commutative ℕSemiring b 1))) (le (succ a) (applyEquality (λ i → succ (succ i)) (Semiring.sumZeroRight ℕSemiring a)))
  ... | bl rewrite multiplicationNIsCommutative (succ (succ b)) (succ (succ a)) = bl

  multiplyIncreasesSucc : (a b : ℕ) → succ a ≤N (succ a) *N (succ b)
  multiplyIncreasesSucc zero zero = inr refl
  multiplyIncreasesSucc zero (succ b) = inl (le (b +N 0) (Semiring.commutative ℕSemiring (succ (b +N 0)) 1))
  multiplyIncreasesSucc (succ a) zero = inr (applyEquality (λ i → succ (succ i)) (equalityCommutative (productWithOneRight a)))
  multiplyIncreasesSucc (succ a) (succ b) = inl (multiplyIncreasesSuccLemma a b)

  multiplyIncreasesSuccLemma' : (a b : ℕ) → succ (succ a) <N succ ((succ (succ a)) *N succ b) +N succ a
  multiplyIncreasesSuccLemma' a b = succPreservesInequality (le (b +N succ (b +N a *N succ b)) refl)

  multiplyIncreasesSucc' : (a b : ℕ) → succ a ≤N succ ((b +N a *N b) +N a)
  multiplyIncreasesSucc' zero zero = inr refl
  multiplyIncreasesSucc' zero (succ b) = inl (le b (applyEquality succ (transitivity (Semiring.commutative ℕSemiring b 1) (transitivity (equalityCommutative (Semiring.sumZeroRight ℕSemiring (succ b))) (equalityCommutative (Semiring.sumZeroRight ℕSemiring _))))))
  multiplyIncreasesSucc' (succ a) zero rewrite multiplicationNIsCommutative a zero = inr refl
  multiplyIncreasesSucc' (succ a) (succ b) = inl (multiplyIncreasesSuccLemma' a b)

  normSize : {a b : ℤ} → (a!=0 : (a ≡ nonneg 0) → False) → (b!=0 : (b ≡ nonneg 0) → False) → (c : ℤ) → b ≡ (a *Z c) → (norm a) ≤N (norm b)
  normSize {nonneg a} {nonneg b} a!=0 b!=0 (nonneg zero) b=ac rewrite nonnegInjective b=ac | multiplicationNIsCommutative a 0 = exFalso (b!=0 refl)
  normSize {nonneg a} {nonneg b} a!=0 b!=0 (nonneg (succ 0)) b=ac rewrite nonnegInjective b=ac | multiplicationNIsCommutative a 1 = inr (equalityCommutative (Semiring.sumZeroRight ℕSemiring a))
  normSize {nonneg 0} {nonneg b} a!=0 b!=0 (nonneg (succ (succ c))) b=ac = exFalso (a!=0 refl)
  normSize {nonneg (succ a)} {nonneg (succ b)} a!=0 b!=0 (nonneg (succ (succ c))) b=ac rewrite nonnegInjective b=ac = multiplyIncreasesSucc a (succ c)
  normSize {nonneg 0} {nonneg b} a!=0 b!=0 (negSucc c) bad = exFalso (a!=0 refl)
  normSize {nonneg (succ a)} {nonneg b} a!=0 b!=0 (negSucc c) ()
  normSize {nonneg a} {negSucc b} a!=0 b!=0 (nonneg c) ()
  normSize {nonneg (succ a)} {negSucc b} a!=0 b!=0 (negSucc c) pr rewrite negSuccInjective pr = multiplyIncreasesSucc' a c
  normSize {negSucc a} {nonneg zero} _ b!=0 c pr = exFalso (b!=0 refl)
  normSize {negSucc a} {nonneg (succ b)} _ _ (nonneg zero) ()
  normSize {negSucc a} {nonneg (succ b)} _ _ (nonneg (succ x)) ()
  normSize {negSucc a} {nonneg (succ b)} _ _ (negSucc c) pr rewrite nonnegInjective pr = multiplyIncreasesSucc a c
  normSize {negSucc a} {negSucc b} _ _ (nonneg (succ c)) pr rewrite negSuccInjective pr | multiplicationNIsCommutative c a | Semiring.commutative ℕSemiring (a +N a *N c) c | Semiring.+Associative ℕSemiring c a (a *N c) | Semiring.commutative ℕSemiring c a | equalityCommutative (Semiring.+Associative ℕSemiring a c (a *N c)) | Semiring.commutative ℕSemiring a (c +N a *N c) = multiplyIncreasesSucc' a c

  divAlg : {a b : ℤ} → (a!=0 : (a ≡ nonneg 0) → False) → (b!=0 : (b ≡ nonneg 0) → False) → DivisionAlgorithmResult ℤRing norm' a!=0 b!=0
  divAlg {nonneg zero} {b} a!=0 b!=0 = exFalso (a!=0 refl)
  divAlg {nonneg (succ a)} {nonneg zero} a!=0 b!=0 = exFalso (b!=0 refl)
  divAlg {nonneg (succ a)} {nonneg (succ b)} a!=0 b!=0 with divisionAlg (succ b) (succ a)
  divAlg {nonneg (succ a)} {nonneg (succ b)} a!=0 b!=0 | record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inl remIsSmall ; quotSmall = quotSmall } = record { quotient = nonneg quot ; rem = nonneg rem ; remSmall = u ; divAlg = transitivity (applyEquality nonneg (equalityCommutative pr)) t }
    where
      t : nonneg ((quot +N b *N quot) +N rem) ≡ nonneg (quot *N succ b) +Z nonneg rem
      t rewrite multiplicationNIsCommutative (succ b) quot = +Zinherits (quot *N succ b) rem
      u : (nonneg rem ≡ nonneg 0) || Sg ((nonneg rem ≡ nonneg 0) → False) (λ pr → rem <N succ b)
      u with TotalOrder.totality ℤOrder (nonneg 0) (nonneg rem)
      u | inl (inl 0<rem) = inr ((λ p → TotalOrder.irreflexive ℤOrder (TotalOrder.<WellDefined ℤOrder refl p 0<rem)) , remIsSmall)
      u | inr 0=rem rewrite 0=rem = inl refl
  divAlg {nonneg (succ a)} {negSucc b} _ _ with divisionAlg (succ b) (succ a)
  divAlg {nonneg (succ a)} {negSucc b} _ _ | record { quot = zero ; rem = rem ; pr = pr ; remIsSmall = inl remIsSmall ; quotSmall = inl quotSmall } rewrite multiplicationNIsCommutative b 0 = record { quotient = nonneg 0 ; rem = nonneg rem ; remSmall = inr (p , remIsSmall) ; divAlg = applyEquality nonneg (equalityCommutative pr) }
    where
      p : (nonneg rem ≡ nonneg 0) → False
      p pr2 rewrite pr = naughtE (equalityCommutative (nonnegInjective pr2))
  divAlg {nonneg (succ a)} {negSucc b} _ _ | record { quot = succ quot ; rem = zero ; pr = pr ; remIsSmall = inl remIsSmall ; quotSmall = inl quotSmall } = record { quotient = negSucc quot ; rem = nonneg zero ; remSmall = inl refl ; divAlg = applyEquality nonneg (transitivity (equalityCommutative pr) (applyEquality (λ i → i +N 0) (multiplicationNIsCommutative (succ b) (succ quot)))) }
  divAlg {nonneg (succ a)} {negSucc b} _ _ | record { quot = succ quot ; rem = succ rem ; pr = pr ; remIsSmall = inl remIsSmall ; quotSmall = inl quotSmall } = record { quotient = negSucc quot ; rem = nonneg (succ rem) ; remSmall = inr ((λ ()) , remIsSmall) ; divAlg = applyEquality nonneg (transitivity (equalityCommutative pr) (applyEquality (λ i → i +N succ rem) (multiplicationNIsCommutative (succ b) (succ quot)))) }
  divAlg {negSucc a} {nonneg zero} _ b!=0 = exFalso (b!=0 refl)
  divAlg {negSucc a} {nonneg (succ b)} _ _ with divisionAlg (succ b) (succ a)
  divAlg {negSucc a} {nonneg (succ b)} _ _ | record { quot = zero ; rem = zero ; pr = pr ; remIsSmall = inl remIsSmall ; quotSmall = quotSmall } = exFalso (naughtE (transitivity (equalityCommutative (transitivity (Semiring.sumZeroRight ℕSemiring _) (multiplicationNIsCommutative b 0))) pr))
  divAlg {negSucc a} {nonneg (succ b)} _ _ | record { quot = succ quot ; rem = zero ; pr = pr ; remIsSmall = inl remIsSmall ; quotSmall = quotSmall } = record { quotient = negSucc quot ; rem = nonneg 0 ; remSmall = inl refl ; divAlg = applyEquality negSucc (succInjective (transitivity (equalityCommutative pr) t)) }
    where
      t : succ (quot +N b *N succ quot) +N 0 ≡ succ ((quot +N b *N quot) +N b)
      t rewrite Semiring.sumZeroRight ℕSemiring (succ (quot +N b *N succ quot)) | Semiring.commutative ℕSemiring (quot +N b *N quot) b | Semiring.+Associative ℕSemiring b quot (b *N quot) | Semiring.commutative ℕSemiring b quot | equalityCommutative (Semiring.+Associative ℕSemiring quot b (b *N quot)) | multiplicationNIsCommutative b (succ quot) | multiplicationNIsCommutative quot b = refl
  divAlg {negSucc a} {nonneg (succ b)} _ _ | record { quot = zero ; rem = succ rem ; pr = pr ; remIsSmall = inl remIsSmall ; quotSmall = quotSmall } rewrite multiplicationNIsCommutative b 0 | equalityCommutative (succInjective pr) = record { quotient = nonneg zero ; rem = negSucc rem ; remSmall = inr (((λ ()) , remIsSmall)) ; divAlg = refl }
  divAlg {negSucc a} {nonneg (succ b)} _ _ | record { quot = succ quot ; rem = succ rem ; pr = pr ; remIsSmall = inl remIsSmall ; quotSmall = quotSmall } = record { quotient = negSucc quot ; rem = negSucc rem ; remSmall = inr ((λ ()) , remIsSmall) ; divAlg = applyEquality negSucc (succInjective (transitivity (equalityCommutative pr) t)) }
    where
      t : succ b *N succ quot +N succ rem ≡ succ (succ (succ b *N quot +N b) +N rem)
      t rewrite Semiring.commutative ℕSemiring ((quot +N b *N quot) +N b) rem | Semiring.commutative ℕSemiring (succ rem) ((quot +N b *N quot) +N b) | multiplicationNIsCommutative b (succ quot) | equalityCommutative (Semiring.+Associative ℕSemiring quot (b *N quot) b) | Semiring.commutative ℕSemiring b (quot *N b) | multiplicationNIsCommutative b quot = refl
  divAlg {negSucc a} {negSucc b} _ _ with divisionAlg (succ b) (succ a)
  divAlg {negSucc a} {negSucc b} _ _ | record { quot = zero ; rem = zero ; pr = pr ; remIsSmall = inl remIsSmall ; quotSmall = quotSmall } = exFalso (naughtE (transitivity (equalityCommutative (transitivity (Semiring.sumZeroRight ℕSemiring (b *N 0)) (multiplicationNIsCommutative b 0))) pr))
  divAlg {negSucc a} {negSucc b} _ _ | record { quot = zero ; rem = succ rem ; pr = pr ; remIsSmall = inl remIsSmall ; quotSmall = quotSmall } rewrite multiplicationNIsCommutative b 0 | equalityCommutative (succInjective pr) = record { quotient = nonneg 0 ; rem = negSucc rem ; remSmall = inr ((λ ()) , remIsSmall) ; divAlg = refl }
  divAlg {negSucc a} {negSucc b} _ _ | record { quot = succ quot ; rem = zero ; pr = pr ; remIsSmall = inl remIsSmall ; quotSmall = quotSmall } rewrite Semiring.sumZeroRight ℕSemiring (quot +N b *N succ quot) | Semiring.commutative ℕSemiring b (succ quot) = record { quotient = nonneg (succ quot) ; rem = nonneg 0 ; remSmall = inl refl ; divAlg = applyEquality negSucc (succInjective (transitivity (equalityCommutative pr) t)) }
    where
      t : succ (quot +N b *N succ quot) ≡ succ ((b +N quot *N b) +N quot)
      t rewrite Semiring.commutative ℕSemiring quot (b *N succ quot) | multiplicationNIsCommutative b (succ quot) = refl
  divAlg {negSucc a} {negSucc b} _ _ | record { quot = succ quot ; rem = succ rem ; pr = pr ; remIsSmall = inl remIsSmall ; quotSmall = quotSmall } rewrite multiplicationNIsCommutative b (succ quot) | Semiring.commutative ℕSemiring quot (b +N quot *N b) | Semiring.commutative ℕSemiring ((b +N quot *N b) +N quot) (succ rem) | Semiring.commutative ℕSemiring rem ((b +N quot *N b) +N quot) = record { quotient = nonneg (succ quot) ; rem = negSucc rem ; remSmall = inr (((λ ()) , remIsSmall)) ; divAlg = applyEquality negSucc (equalityCommutative (succInjective pr)) }

ℤEuclideanDomain : EuclideanDomain ℤRing
EuclideanDomain.isIntegralDomain ℤEuclideanDomain = ℤIntDom
EuclideanDomain.norm ℤEuclideanDomain = norm'
EuclideanDomain.normSize ℤEuclideanDomain = normSize
EuclideanDomain.divisionAlg ℤEuclideanDomain {a} {b} a!=0 b!=0 = divAlg {a} {b} a!=0 b!=0


text:
{-# OPTIONS --without-K --safe #-}

data D : Set where
  c : D → D

variable
  x y : D

data P : D → D → Set where
  c : P (c x) (c y)

record Q (y : D) : Set where

G : .(Q y) → P x y → Set₁
G _ c = Set


text:
{-# OPTIONS --without-K #-}
module hott.loop.sum where

open import sum
open import equality
open import function.core
open import function.extensionality
open import function.isomorphism
open import function.overloading
open import sets.nat
open import pointed
open import hott.equivalence
open import hott.level.core
open import hott.loop.core
open import hott.loop.properties

private
  abstract
    loop-sum' : ∀ {i}{j}{A : Set i}{B : A → Set j}(n : ℕ)
              → (hB : (a : A) → h n (B a))
              → {a₀ : A}{b₀ : B a₀}
              → Ω n {Σ A B} (a₀ , b₀) ≅ Ω n a₀
    loop-sum' 0 hB {a₀}{b₀} = Σ-ap-iso refl≅ (λ a → contr-⊤-iso (hB a)) ·≅ ×-right-unit
    loop-sum' {A = A}{B = B} (suc n) hB {a₀}{b₀} = Ω-iso n (sym≅ Σ-split-iso) refl
                                                ·≅ loop-sum' n λ p → hB _ _ _

    loop-sum-β : ∀ {i}{j}{A : Set i}{B : A → Set j}(n : ℕ)
               → (hB : (a : A) → h n (B a))
               → {a₀ : A}{b₀ : B a₀}
               → (p : Ω n {Σ A B} (a₀ , b₀))
               → apply≅ (loop-sum' n hB) p ≡ mapΩ n proj₁ p
    loop-sum-β zero hB p = refl
    loop-sum-β (suc n) hB p
      = loop-sum-β n _ (mapΩ n apΣ p)
      · mapΩ-hom n apΣ proj₁ p
      · funext-inv (ap proj₁ (ap (mapΩP n) lem)) p
      where
        lem : ∀ {i}{j}{A : Set i}{B : A → Set j}{a₀ : A}{b₀ : B a₀}
            → _≡_ {A = PMap (_≡_ {A = Σ A B} (a₀ , b₀) (a₀ , b₀) , refl) ((a₀ ≡ a₀) , refl)}
              (proj₁ ∘ apΣ , refl)
              (ap proj₁ , refl)
        lem = apply≅ pmap-eq ((λ _ → refl) , refl)

loop-sum : ∀ {i}{j}{A : Set i}{B : A → Set j}(n : ℕ)
         → (hB : (a : A) → h n (B a))
         → {a₀ : A}{b₀ : B a₀}
         → Ω n {Σ A B} (a₀ , b₀) ≅ Ω n a₀
loop-sum n hB {a₀}{b₀} = ≈⇒≅ (mapΩ n proj₁ , subst weak-equiv eq we)
  where
    abstract
      we : weak-equiv (apply (loop-sum' n hB {a₀}{b₀}))
      we = proj₂ (≅⇒≈ (loop-sum' n hB))

      eq : apply (loop-sum' n hB {a₀}{b₀}) ≡ mapΩ n proj₁
      eq = funext (loop-sum-β n hB)

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
module Oscar.Property.Associativity where

open import Oscar.Level

record Associativity
  {𝔬} {⋆ : Set 𝔬}
  {𝔪} {_⇒_ : ⋆ → ⋆ → Set 𝔪}
  (_∙_ : ∀ {y z} → y ⇒ z → ∀ {x} → x ⇒ y → x ⇒ z)
  {𝔮} (_≤_ : ∀ {x y} → x ⇒ y → x ⇒ y → Set 𝔮)
  : Set (𝔬 ⊔ 𝔪 ⊔ 𝔮) where
  field
    associativity : ∀ {w x} (f : w ⇒ x) {y} (g : x ⇒ y) {z} (h : y ⇒ z) → ((h ∙ g) ∙ f) ≤ (h ∙ (g ∙ f))

open Associativity ⦃ … ⦄ public

association : ∀
  {𝔬} {⋆ : Set 𝔬}
  {𝔪} {_⇒_ : ⋆ → ⋆ → Set 𝔪}
  (_∙_ : ∀ {y z} → y ⇒ z → ∀ {x} → x ⇒ y → x ⇒ z)
  {𝔮} (_≤_ : ∀ {x y} → x ⇒ y → x ⇒ y → Set 𝔮)
  ⦃ _ : Associativity _∙_ _≤_ ⦄
  → ∀ {w x} (f : w ⇒ x) {y} (g : x ⇒ y) {z} (h : y ⇒ z) → ((h ∙ g) ∙ f) ≤ (h ∙ (g ∙ f))
association _∙_ _≤_ = associativity {_∙_ = _∙_} {_≤_ = _≤_}


text:
------------------------------------------------------------------------
-- Universe levels
------------------------------------------------------------------------

module Imports.Level where

postulate
  Level : Set
  zero : Level
  suc  : (i : Level) → Level
  _⊔_ : Level -> Level -> Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO zero  #-}
{-# BUILTIN LEVELSUC  suc   #-}
{-# BUILTIN LEVELMAX  _⊔_   #-}

infixl 6 _⊔_

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module Mockingbird.Forest where

open import Mockingbird.Forest.Base public

max_stars_repo_name: splintah/combinatory-logic

max_issues_repo_name: splintah/combinatory-logic

max_forks_repo_name: splintah/combinatory-logic


text:
-- {-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.lhs.unify:65 -v tc.irr:50 #-}

open import Agda.Builtin.Nat

data B {A : Set} : A → Set where
  b : (a : A) → B a

data C {A : Set} : ∀ a → B {A} a → Set where
  c : (a : A) → C a (b a)

id : ∀ x → C _ x → B 0
id x (c y) = {!!}

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
{-# OPTIONS --without-K #-}
module hw2 where

open import Level using (_⊔_)
open import Function using (id)
open import Data.Nat using (ℕ; suc; _+_; _*_)
open import Data.Empty using (⊥)
open import Data.Sum using (_⊎_; inj₁; inj₂)

import Level

infix 4 _≡_

recℕ : ∀ {ℓ} → (C : Set ℓ) → C → (ℕ → C → C) → ℕ → C
recℕ C z f 0 = z
recℕ C z f (suc n) = f n (recℕ C z f n)

indℕ : ∀ {ℓ}
         → (C : ℕ → Set ℓ)
         → C 0
         → ((n : ℕ) → C n → C (suc n))
         → (n : ℕ)
         → C n
indℕ C z f 0 = z
indℕ C z f (suc n) = f n (indℕ C z f n)

------------------------------------------------------------------------------
-- ≡
data _≡_ {ℓ} {A : Set ℓ} : (x y : A) → Set ℓ where
  refl : (x : A) → x ≡ x

rec≡ : {A : Set} →
       (R : A → A → Set) {reflexiveR : {a : A} → R a a} →
       ({x y : A} (p : x ≡ y) → R x y)
rec≡ R {reflR} (refl y) = reflR {y}

------------------------------------------------------------------------------
-- subst
subst : ∀ {ℓ} {A : Set ℓ} {C : A → Set ℓ} →
        ({x y : A} (p : x ≡ y) → C x → C y)
subst (refl x) = id

------------------------------------------------------------------------------
-- ∘
_∘_ : {A B C : Set} → (f : B → C) → (g : A → B) → A → C
f ∘ g = (λ a → f (g a))

module Circle1 where
  private
    data S¹* : Set where
      base* : S¹*

  S¹ : Set
  S¹ = S¹*

  base : S¹
  base = base*

  postulate
    loop : base ≡ base

  recS¹ : {C : Set} → (cbase : C) → (cloop : cbase ≡ cbase) → S¹ → C
  recS¹ cbase cloop base* = cbase

--  postulate
--    βrecS¹ : {C : Set} → (cbase : C) → (cloop : cbase ≡ cbase)
--      → ap (recS¹ cbase cloop) loop ≡ cloop

-- indS¹ : {C : S¹ → Set}
--  → (cbase : C base) → (cloop : transport C look cbase ≡ cbase)
--  → apd (indS¹ {C} cbase cloop) loop ≡ cloop

max_stars_repo_name: andmkent/misc-HoTT

max_issues_repo_name: andmkent/misc-HoTT

max_forks_repo_name: andmkent/misc-HoTT