text:
open import Data.Empty
open import Data.List hiding ([_]) renaming (_∷_ to _∷ₗ_)
open import Data.Maybe
open import Data.Product
open import Data.Sum
open import Data.Unit

open import AEff
open import EffectAnnotations
open import Preservation
open import Progress
open import Renamings
open import Substitutions renaming (⟨_,_⟩ to ⟨_,,_⟩)
open import Types

open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Nullary
open import Relation.Nullary.Negation

module Finality where

-- SMALL-STEP OPERATIONAL SEMANTICS FOR WELL-TYPED COMPUTATIONS
-- WITH INLINED EVALUATION CONTEXT RULES

mutual

  infix 10 _↝↝_

  data _↝↝_ {Γ : Ctx} : {C : CType} → Γ ⊢C⦂ C → Γ ⊢C⦂ C → Set where

    -- COMPUTATIONAL RULES

    apply           : {X : VType}
                      {C : CType} →
                      (M : Γ ∷ X ⊢C⦂ C) →
                      (V : Γ ⊢V⦂ X) →
                      ----------------------
                      (ƛ M) · V
                      ↝↝
                      M [ sub-id [ V ]s ]c

    let-return      : {X Y : VType}
                      {o : O}
                      {i : I} →
                      (V : Γ ⊢V⦂ X) →
                      (N : Γ ∷ X ⊢C⦂ Y ! (o , i)) →
                      -----------------------------
                      let= (return V) `in N
                      ↝↝
                      N [ sub-id [ V ]s ]c

    let-↑           : {X Y : VType}
                      {o : O}
                      {i : I}
                      {op : Σₛ} →
                      (p : op ∈ₒ o) →
                      (V : Γ ⊢V⦂ proj₁ (payload op)) →
                      (M : Γ ⊢C⦂ X ! (o , i)) →
                      (N : Γ ∷ X ⊢C⦂ Y ! (o , i)) →
                      --------------------------------
                      let= (↑ op p V M) `in N
                      ↝↝
                      ↑ op p V (let= M `in N)

    let-promise     : {X Y Z : VType}
                      {o o' : O}
                      {i i' : I}
                      {op : Σₛ} →
                      (p : (o' , i') ⊑ lkpᵢ op i) →
                      (M₁ : Γ ∷ proj₁ (payload op) ∷ (𝟙 ⇒ (⟨ X ⟩ ! (∅ₒ , ∅ᵢ [ op ↦ just (o' , i') ]ᵢ))) ⊢C⦂ ⟨ X ⟩ ! (o' , i')) →
                      (M₂ : Γ ∷ ⟨ X ⟩ ⊢C⦂ Y ! (o , i)) →
                      (N : Γ ∷ Y ⊢C⦂ Z ! (o , i)) →
                      ---------------------------------------------------------------------------------------------------------
                      let= (promise op ∣ p ↦ M₁ `in M₂) `in N
                      ↝↝
                      (promise op ∣ p ↦ M₁ `in (let= M₂ `in (C-rename (ren-cong ren-wk) N)))

    let-await       : {X Y Z : VType}
                      {o : O}
                      {i : I} →
                      (V : Γ ⊢V⦂ ⟨ X ⟩) →
                      (M : Γ ∷ X ⊢C⦂ Y ! (o , i)) →
                      (N : Γ ∷ Y ⊢C⦂ Z ! (o , i)) →
                      -------------------------------------------------------
                      let= (await V until M) `in N
                      ↝↝
                      await V until (let= M `in C-rename (ren-cong ren-wk) N)

    let-spawn       : {X Y : VType}
                      {C : CType}
                      {o : O}
                      {i : I} →
                      (M : Γ ■ ⊢C⦂ C) →
                      (N : Γ ⊢C⦂ X ! (o , i)) →
                      (K : Γ ∷ X ⊢C⦂ Y ! (o , i)) →
                      ---------------------------------------
                      let= (spawn M N) `in K
                      ↝↝
                      spawn M (let= N `in K)

    promise-↑       : {X Y : VType}
                      {o o' : O}
                      {i i' : I}
                      {op op' : Σₛ} →
                      (p : (o' , i') ⊑ lkpᵢ op i) →
                      (q : op' ∈ₒ o) →
                      (V : Γ ∷ ⟨ X ⟩ ⊢V⦂ proj₁ (payload op')) →
                      (M : Γ ∷ proj₁ (payload op) ∷ (𝟙 ⇒ (⟨ X ⟩ ! (∅ₒ , ∅ᵢ [ op ↦ just (o' , i') ]ᵢ))) ⊢C⦂ ⟨ X ⟩ ! (o' , i')) →
                      (N : Γ ∷ ⟨ X ⟩ ⊢C⦂ Y ! (o , i)) →
                      --------------------------------------------------------------------------------------------------------
                      (promise op ∣ p ↦ M `in (↑ op' q V N))
                      ↝↝
                      ↑ op' q (strengthen-val {Δ = X ∷ₗ []} (proj₂ (payload op')) V) (promise op ∣ p ↦ M `in N)

    promise-spawn   : {X Y : VType}
                      {C : CType}
                      {o o' : O}
                      {i i' : I}
                      {op : Σₛ} →
                      (p : (o' , i') ⊑ lkpᵢ op i) →
                      (M : Γ ∷ proj₁ (payload op) ∷ (𝟙 ⇒ (⟨ X ⟩ ! (∅ₒ , ∅ᵢ [ op ↦ just (o' , i') ]ᵢ))) ⊢C⦂ ⟨ X ⟩ ! (o' , i')) →
                      (N : Γ ∷ ⟨ X ⟩ ■ ⊢C⦂ C) →
                      (K : Γ ∷ ⟨ X ⟩ ⊢C⦂ Y ! (o , i)) →
                      ---------------------------------------------------------------------------------------------------------
                      (promise op ∣ p ↦ M `in (spawn N K))
                      ↝↝
                      spawn (strengthen-■-c {Γ' = []} {Δ = X ∷ₗ []} N) (promise op ∣ p ↦ M `in K)

    ↓-return        : {X : VType}
                      {o : O}
                      {i : I}
                      {op : Σₛ} →
                      (V : Γ ⊢V⦂ proj₁ (payload op)) →
                      (W : Γ ⊢V⦂ X) →
                      ----------------------------------------------------------------
                      ↓ {o = o} {i = i} op V (return W)
                      ↝↝
                      return {o = proj₁ (op ↓ₑ (o , i))} {i = proj₂ (op ↓ₑ (o , i))} W

    ↓-↑             : {X : VType}
                      {o : O}
                      {i : I}
                      {op : Σₛ}
                      {op' : Σₛ} →
                      (p : op' ∈ₒ o) →
                      (V : Γ ⊢V⦂ proj₁ (payload op)) →
                      (W : Γ ⊢V⦂ proj₁ (payload op')) →
                      (M : Γ ⊢C⦂ X ! (o , i)) →
                      ---------------------------------
                      ↓ op V (↑ op' p W M)
                      ↝↝
                      ↑ op' (↓ₑ-⊑ₒ op' p) W (↓ op V M)

    ↓-promise-op    : {X Y : VType}
                      {o o' : O}
                      {i i' : I}
                      {op : Σₛ} →
                      (p : (o' , i') ⊑ lkpᵢ op i) →
                      (V : Γ ⊢V⦂ proj₁ (payload op)) →
                      (M : Γ ∷ proj₁ (payload op) ∷ (𝟙 ⇒ (⟨ X ⟩ ! (∅ₒ , ∅ᵢ [ op ↦ just (o' , i') ]ᵢ))) ⊢C⦂ ⟨ X ⟩ ! (o' , i')) →
                      (N : Γ ∷ ⟨ X ⟩ ⊢C⦂ Y ! (o , i)) →
                      --------------------------------------------------------------------------------------------------------------------------------------------------------
                      ↓ op V (promise op ∣ p ↦ M `in N )
                      ↝↝
                      (let= (coerce (⊑ₒ-trans (proj₁ (⊑-proj p (proj₂ (proj₂ (⊑-just p))))) (↓ₑ-⊑ₒ-o' {o = o} (proj₂ (proj₂ (⊑-just p)))))
                                    (⊑ᵢ-trans (proj₂ (⊑-proj p (proj₂ (proj₂ (⊑-just p))))) (↓ₑ-⊑ₒ-i' {o = o} (proj₂ (proj₂ (⊑-just p)))))
                                    (M [ (sub-id [ V ]s)
                                       [ ƛ (promise op ∣ subst (λ oi → (o' , i') ⊑ oi) (sym ite-≡) ⊑-refl ↦ C-rename (ren-cong (ren-cong ren-wk)) M `in return (` Hd)) ]s ]c))
                       `in (↓ op (V-rename ren-wk V) N))

    ↓-promise-op'   : {X Y : VType}
                      {o o' : O}
                      {i i' : I}
                      {op op' : Σₛ} →
                      (p : ¬ op ≡ op') →
                      (q : (o' , i') ⊑ lkpᵢ op' i) →
                      (V : Γ ⊢V⦂ proj₁ (payload op)) →
                      (M : Γ ∷ proj₁ (payload op') ∷ (𝟙 ⇒ (⟨ X ⟩ ! (∅ₒ , ∅ᵢ [ op' ↦ just (o' , i') ]ᵢ))) ⊢C⦂ ⟨ X ⟩ ! (o' , i')) →
                      (N : Γ ∷ ⟨ X ⟩ ⊢C⦂ Y ! (o , i)) →
                      -----------------------------------------------------------------------------------------------------------
                      ↓ op V (promise op' ∣ q ↦ M `in N )
                      ↝↝
                      promise op' ∣ (lkpᵢ-↓ₑ-neq-⊑ {o = o} {i = i} p q) ↦ M `in ↓ op (V-rename ren-wk V) N

    ↓-await        : {X Y : VType}
                     {o : O}
                     {i : I}
                     {op : Σₛ} →
                     (V : Γ ⊢V⦂ proj₁ (payload op)) →
                     (W : Γ ⊢V⦂ ⟨ X ⟩) →
                     (M : Γ ∷ X ⊢C⦂ Y ! (o , i)) →
                     ------------------------------------------
                     ↓ op V (await W until M)
                     ↝↝
                     await W until (↓ op (V-rename ren-wk V) M)

    ↓-spawn         : {X : VType}
                      {C : CType}
                      {o : O}
                      {i : I}
                      {op : Σₛ} →
                      (V : Γ ⊢V⦂ proj₁ (payload op)) →
                      (M : Γ ■ ⊢C⦂ C) →
                      (N : Γ ⊢C⦂ X ! (o , i)) →
                      --------------------------------
                      ↓ op V (spawn M N)
                      ↝↝
                      spawn M (↓ op V N)

    await-promise   : {X : VType}
                      {C : CType} →
                      (V : Γ ⊢V⦂ X) →
                      (M : Γ ∷ X ⊢C⦂ C) →
                      --------------------
                      await ⟨ V ⟩ until M
                      ↝↝
                      M [ sub-id [ V ]s ]c

    box-unbox       : {X : VType}
                      {C : CType} →
                      (V : Γ ■ ⊢V⦂ X) →
                      (M : Γ ∷ X ⊢C⦂ C) →
                      ----------------------------------------
                      unbox (□ V) `in M
                      ↝↝
                      M [ ⟨ sub-id ,, ■-str-v {Γ' = []} V ⟩ ]c

    -- INLINED EVALUATION CONTEXT RULES

    context-let      : {X Y : VType}
                       {o : O}
                       {i : I} →
                       {M M' : Γ ⊢C⦂ X ! (o , i)} →
                       {N : Γ ∷ X ⊢C⦂ Y ! (o , i)} →
                       M ↝↝ M' →
                       -----------------------------
                       let= M `in N
                       ↝↝
                       let= M' `in N

    context-↑        : {X : VType}
                       {o : O}
                       {i : I}
                       {op : Σₛ}
                       {p : op ∈ₒ o}
                       {V : Γ ⊢V⦂ proj₁ (payload op)}
                       {M N : Γ ⊢C⦂ X ! (o , i)} →
                       M ↝↝ N →
                       ---------------------------
                       ↑ op p V M
                       ↝↝
                       ↑ op p V N

    context-↓        : {X : VType}
                       {o : O}
                       {i : I}
                       {op : Σₛ}
                       {V : Γ ⊢V⦂ proj₁ (payload op)}
                       {M N : Γ ⊢C⦂ X ! (o , i)} →
                       M ↝↝ N →
                       ------------------------------
                       ↓ op V M
                       ↝↝
                       ↓ op V N

    context-promise : {X Y : VType}
                      {o o' : O}
                      {i i' : I}
                      {op : Σₛ} →
                      {r : (o' , i') ⊑ lkpᵢ op i}
                      {M : Γ ∷ proj₁ (payload op) ∷ (𝟙 ⇒ (⟨ X ⟩ ! (∅ₒ , ∅ᵢ [ op ↦ just (o' , i') ]ᵢ))) ⊢C⦂ ⟨ X ⟩ ! (o' , i')} →
                      {N N' : Γ ∷ ⟨ X ⟩ ⊢C⦂ Y ! (o , i)} →
                      N ↝↝ N' →
                      --------------------------------------------------------------------------------------------------------
                      promise op ∣ r ↦ M `in N
                      ↝↝
                      promise op ∣ r ↦ M `in N'

    context-spawn   : {C D : CType}
                      {M : Γ ■ ⊢C⦂ C}
                      {N N' : Γ ⊢C⦂ D} →
                      N ↝↝ N' →
                      ------------------
                      spawn M N
                      ↝↝
                      spawn M N'

    context-coerce  : {X : VType}
                      {o o' : O}
                      {i i' : I}
                      {p : o ⊑ₒ o'}
                      {q : i ⊑ᵢ i'} →
                      {M N : Γ ⊢C⦂ X ! (o , i)} →
                      M ↝↝ N →
                      ---------------------------
                      coerce p q M
                      ↝↝
                      coerce p q N

    -- COERCION RULES

    coerce-return   : {X : VType}
                      {o o' : O}
                      {i i' : I}
                      {p : o ⊑ₒ o'}
                      {q : i ⊑ᵢ i'} →
                      (V : Γ ⊢V⦂ X) →
                      --------------------------------
                      coerce p q (return V) ↝↝ return V

    coerce-↑        : {X : VType}
                      {o o' : O}
                      {i i' : I}
                      {p : o ⊑ₒ o'}
                      {q : i ⊑ᵢ i'}
                      {op : Σₛ} →
                      (r : op ∈ₒ o) →
                      (V : Γ ⊢V⦂ proj₁ (payload op)) →
                      (M : Γ ⊢C⦂ X ! (o , i)) →
                      -------------------------------
                      coerce p q (↑ op r V M)
                      ↝↝
                      ↑ op (p op r) V (coerce p q M)

    coerce-promise  : {X Y : VType}
                      {o o' o'' : O}
                      {i i' i'' : I}
                      {p : o ⊑ₒ o'}
                      {q : i ⊑ᵢ i'}
                      {op : Σₛ} →
                      (r : (o'' , i'') ⊑ lkpᵢ op i )
                      (M : Γ ∷ proj₁ (payload op) ∷ (𝟙 ⇒ (⟨ X ⟩ ! (∅ₒ , ∅ᵢ [ op ↦ just (o'' , i'') ]ᵢ))) ⊢C⦂ ⟨ X ⟩ ! (o'' , i'')) →
                      (N : Γ ∷ ⟨ X ⟩ ⊢C⦂ Y ! (o , i)) →
                      -------------------------------------------------------------------------------------------------------------
                      coerce p q (promise op ∣ r ↦ M `in N)
                      ↝↝
                      promise_∣_↦_`in_ op (subst (λ oi → (o'' , i'') ⊑ oi) (sym (lkpᵢ-next-eq q (proj₂ (proj₂ (⊑-just r)))))
                                            (⊑-trans r (proj₂ (proj₂ (⊑-just r))) (
                                              (lkpᵢ-next-⊑ₒ q (proj₂ (proj₂ (⊑-just r)))) ,
                                              (lkpᵢ-next-⊑ᵢ q (proj₂ (proj₂ (⊑-just r)))))))
                                          M
                                          (coerce p q N)

    coerce-await   : {X Y : VType}
                     {o o' : O}
                     {i i' : I}
                     {p : o ⊑ₒ o'}
                     {q : i ⊑ᵢ i'} →
                     (V : Γ ⊢V⦂ ⟨ X ⟩) →
                     (M : Γ ∷ X ⊢C⦂ Y ! (o , i)) →
                     -----------------------------
                     coerce p q (await V until M)
                     ↝↝
                     await V until (coerce p q M)

    coerce-spawn   : {X : VType}
                     {C : CType}
                     {o o' : O}
                     {i i' : I}
                     {p : o ⊑ₒ o'}
                     {q : i ⊑ᵢ i'} →
                     (M : Γ ■ ⊢C⦂ C) →
                     (N : Γ ⊢C⦂ X ! (o , i)) →
                     -------------------------
                     coerce p q (spawn M N)
                     ↝↝
                     spawn M (coerce p q N)

-- ONE-TO-ONE CORRESPONDENCE BETWEEN THE TWO SETS OF REDUCTION RULES

↝↝-to-↝ : {Γ : Ctx}
          {C : CType}
          {M N : Γ ⊢C⦂ C} →
          M ↝↝ N →
          -----------------
          M ↝ N

↝↝-to-↝ (apply M V) =
  apply M V
↝↝-to-↝ (let-return V N) =
  let-return V N
↝↝-to-↝ (let-↑ p V M N) =
  let-↑ p V M N
↝↝-to-↝ (let-promise p M₁ M₂ N) =
  let-promise p M₁ M₂ N
↝↝-to-↝ (let-await V M N) =
  let-await V M N
↝↝-to-↝ (let-spawn M N K) =
  let-spawn M N K
↝↝-to-↝ (promise-↑ p q V M N) =
  promise-↑ p q V M N
↝↝-to-↝ (promise-spawn p M N K) =
  promise-spawn p M N K
↝↝-to-↝ (↓-return V W) =
  ↓-return V W
↝↝-to-↝ (↓-↑ p V W M) =
  ↓-↑ p V W M
↝↝-to-↝ (↓-promise-op p V M N) =
  ↓-promise-op p V M N
↝↝-to-↝ (↓-promise-op' p q V M N) =
  ↓-promise-op' p q V M N
↝↝-to-↝ (↓-await V W M) =
  ↓-await V W M
↝↝-to-↝ (↓-spawn V M N) =
  ↓-spawn V M N
↝↝-to-↝ (await-promise V M) =
  await-promise V M
↝↝-to-↝ (box-unbox V M) =
  box-unbox V M
↝↝-to-↝ (context-let r) =
  context _ (↝↝-to-↝ r)
↝↝-to-↝ (context-↑ r) =
  context _ (↝↝-to-↝ r)
↝↝-to-↝ (context-↓ r) =
  context _ (↝↝-to-↝ r)
↝↝-to-↝ (context-promise r) =
  context _ (↝↝-to-↝ r)
↝↝-to-↝ (context-spawn r) =
  context _ (↝↝-to-↝ r)
↝↝-to-↝ (context-coerce r) =
  context _ (↝↝-to-↝ r)
↝↝-to-↝ (coerce-return V) =
  coerce-return V
↝↝-to-↝ (coerce-↑ p V M) =
  coerce-↑ p V M
↝↝-to-↝ (coerce-promise p M N) =
  coerce-promise p M N
↝↝-to-↝ (coerce-await V M) =
  coerce-await V M
↝↝-to-↝ (coerce-spawn M N) =
  coerce-spawn M N

mutual
  ↝-context-to-↝↝ : {Γ : Ctx}
                    {Δ : BCtx}
                    {C : CType} →
                    (E : Γ ⊢E[ Δ ]⦂ C) →
                    {M N : (Γ ⋈ Δ) ⊢C⦂ hole-ty-e E} →
                    M ↝ N →
                    ---------------------------------
                    E [ M ] ↝↝ E [ N ]

  ↝-context-to-↝↝ [-] r =
    ↝-to-↝↝ r
  ↝-context-to-↝↝ (let= E `in x) r =
    context-let (↝-context-to-↝↝ E r)
  ↝-context-to-↝↝ (↑ op p V E) r =
    context-↑ (↝-context-to-↝↝ E r)
  ↝-context-to-↝↝ (↓ op V E) r =
    context-↓ (↝-context-to-↝↝ E r)
  ↝-context-to-↝↝ (promise op ∣ p ↦ M `in E) r =
    context-promise (↝-context-to-↝↝ E r)
  ↝-context-to-↝↝ (spawn M E) r =
    context-spawn (↝-context-to-↝↝ E r)
  ↝-context-to-↝↝ (coerce p q E) r =
    context-coerce (↝-context-to-↝↝ E r)

  ↝-to-↝↝ : {Γ : Ctx}
            {C : CType}
            {M N : Γ ⊢C⦂ C} →
            M ↝ N →
            -----------------
            M ↝↝ N

  ↝-to-↝↝ (apply M V) =
    apply M V
  ↝-to-↝↝ (let-return V N) =
    let-return V N
  ↝-to-↝↝ (let-↑ p V M N) =
    let-↑ p V M N
  ↝-to-↝↝ (let-promise p M₁ M₂ N) =
    let-promise p M₁ M₂ N
  ↝-to-↝↝ (let-await V M N) =
    let-await V M N
  ↝-to-↝↝ (let-spawn M N K) =
    let-spawn M N K
  ↝-to-↝↝ (promise-↑ p q V M N) =
    promise-↑ p q V M N
  ↝-to-↝↝ (promise-spawn p M N K) =
    promise-spawn p M N K
  ↝-to-↝↝ (↓-return V W) =
    ↓-return V W
  ↝-to-↝↝ (↓-↑ p V W M) =
    ↓-↑ p V W M
  ↝-to-↝↝ (↓-promise-op p V M N) =
    ↓-promise-op p V M N
  ↝-to-↝↝ (↓-promise-op' p q V M N) =
    ↓-promise-op' p q V M N
  ↝-to-↝↝ (↓-await V W M) =
    ↓-await V W M
  ↝-to-↝↝ (↓-spawn V M N) =
    ↓-spawn V M N
  ↝-to-↝↝ (await-promise V M) =
    await-promise V M
  ↝-to-↝↝ (box-unbox V M) =
    box-unbox V M
  ↝-to-↝↝ (context E r) =
    ↝-context-to-↝↝ E r
  ↝-to-↝↝ (coerce-return V) =
    coerce-return V
  ↝-to-↝↝ (coerce-↑ p V M) =
    coerce-↑ p V M
  ↝-to-↝↝ (coerce-promise p M N) =
    coerce-promise p M N
  ↝-to-↝↝ (coerce-await V M) =
    coerce-await V M
  ↝-to-↝↝ (coerce-spawn M N) =
    coerce-spawn M N

-- FINALITY OF RESULT FORMS

run-finality-↝↝ : {Γ : MCtx}
                  {C : CType}
                  {M N : ⟨⟨ Γ ⟩⟩ ⊢C⦂ C} →
                  RunResult⟨ Γ ∣ M ⟩ →
                  M ↝↝ N →
                  -----------------------
                  ⊥

run-finality-↝↝ (promise ()) (promise-↑ p q V M N)
run-finality-↝↝ (promise ()) (promise-spawn p M N K)
run-finality-↝↝ (promise R) (context-promise r) =
  run-finality-↝↝ R r

comp-finality-↝↝ : {Γ : MCtx}
                   {C : CType}
                   {M N : ⟨⟨ Γ ⟩⟩ ⊢C⦂ C} →
                   CompResult⟨ Γ ∣ M ⟩ →
                   M ↝↝ N →
                   -----------------------
                   ⊥

comp-finality-↝↝ (comp R) r =
  run-finality-↝↝ R r
comp-finality-↝↝ (signal R) (context-↑ r) =
  comp-finality-↝↝ R r
comp-finality-↝↝ (spawn R) (context-spawn r) =
  comp-finality-↝↝ R r

comp-finality : {Γ : MCtx}
                {C : CType}
                {M N : ⟨⟨ Γ ⟩⟩ ⊢C⦂ C} →
                CompResult⟨ Γ ∣ M ⟩ →
                M ↝ N →
                -----------------------
                ⊥

comp-finality R r =
  comp-finality-↝↝ R (↝-to-↝↝ r)

max_stars_repo_name: danelahman/higher-order-aeff-agda

max_issues_repo_name: danelahman/modal-aeff-agda

max_forks_repo_name: danelahman/modal-aeff-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Substitutions
------------------------------------------------------------------------

-- Uses a variant of Conor McBride's technique from "Type-Preserving
-- Renaming and Substitution".

-- See Data.Fin.Substitution.Example for an example of how this module
-- can be used: a definition of substitution for the untyped
-- λ-calculus.

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

module Data.Fin.Substitution where

open import Data.Nat hiding (_⊔_)
open import Data.Fin using (Fin; zero; suc)
open import Data.Vec
open import Function as Fun using (flip)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
  as Star using (Star; ε; _◅_)
open import Level using (Level; _⊔_)
import Level as L
open import Relation.Unary using (Pred)

------------------------------------------------------------------------
-- General functionality

-- A Sub T m n is a substitution which, when applied to something with
-- at most m variables, yields something with at most n variables.

Sub : ∀ {ℓ} → Pred ℕ ℓ → ℕ → ℕ → Set ℓ
Sub T m n = Vec (T n) m

-- A /reversed/ sequence of matching substitutions.

Subs : ∀ {ℓ} → Pred ℕ ℓ → ℕ → ℕ → Set ℓ
Subs T = flip (Star (flip (Sub T)))

-- Some simple substitutions.

record Simple {ℓ : Level} (T : Pred ℕ ℓ) : Set ℓ where
  infix  10 _↑
  infixl 10 _↑⋆_ _↑✶_

  field
    var    : ∀ {n} → Fin n → T n      -- Takes variables to Ts.
    weaken : ∀ {n} → T n → T (suc n)  -- Weakens Ts.

  -- Lifting.

  _↑ : ∀ {m n} → Sub T m n → Sub T (suc m) (suc n)
  ρ ↑ = var zero ∷ map weaken ρ

  _↑⋆_ : ∀ {m n} → Sub T m n → ∀ k → Sub T (k + m) (k + n)
  ρ ↑⋆ zero  = ρ
  ρ ↑⋆ suc k = (ρ ↑⋆ k) ↑

  _↑✶_ : ∀ {m n} → Subs T m n → ∀ k → Subs T (k + m) (k + n)
  ρs ↑✶ k = Star.gmap (_+_ k) (λ ρ → ρ ↑⋆ k) ρs

  -- The identity substitution.

  id : ∀ {n} → Sub T n n
  id {zero}  = []
  id {suc n} = id ↑

  -- Weakening.

  wk⋆ : ∀ k {n} → Sub T n (k + n)
  wk⋆ zero    = id
  wk⋆ (suc k) = map weaken (wk⋆ k)

  wk : ∀ {n} → Sub T n (suc n)
  wk = wk⋆ 1

  -- A substitution which only replaces the first variable.

  sub : ∀ {n} → T n → Sub T (suc n) n
  sub t = t ∷ id

-- Application of substitutions.

record Application {ℓ₁ ℓ₂ : Level} (T₁ : Pred ℕ ℓ₁) (T₂ : Pred ℕ ℓ₂) :
    Set (ℓ₁ ⊔ ℓ₂) where
  infixl 8 _/_ _/✶_
  infixl 9 _⊙_

  -- Post-application of substitutions to things.

  field _/_ : ∀ {m n} → T₁ m → Sub T₂ m n → T₁ n

  -- Reverse composition. (Fits well with post-application.)

  _⊙_ : ∀ {m n k} → Sub T₁ m n → Sub T₂ n k → Sub T₁ m k
  ρ₁ ⊙ ρ₂ = map (λ t → t / ρ₂) ρ₁

  -- Application of multiple substitutions.

  _/✶_ : ∀ {m n} → T₁ m → Subs T₂ m n → T₁ n
  _/✶_ = Star.gfold Fun.id _ (flip _/_) {k = zero}

-- A combination of the two records above.

record Subst {ℓ : Level} (T : Pred ℕ ℓ) : Set ℓ where
  field
    simple      : Simple      T
    application : Application T T

  open Simple      simple      public
  open Application application public

  -- Composition of multiple substitutions.

  ⨀ : ∀ {m n} → Subs T m n → Sub T m n
  ⨀ ε        = id
  ⨀ (ρ ◅ ε)  = ρ  -- Convenient optimisation; simplifies some proofs.
  ⨀ (ρ ◅ ρs) = ⨀ ρs ⊙ ρ

------------------------------------------------------------------------
-- Instantiations and code for facilitating instantiations

-- Liftings from T₁ to T₂.

record Lift {ℓ₁ ℓ₂ : Level} (T₁ : Pred ℕ ℓ₁) (T₂ : Pred ℕ ℓ₂) :
    Set (ℓ₁ ⊔ ℓ₂) where
  field
    simple : Simple T₁
    lift   : ∀ {n} → T₁ n → T₂ n

  open Simple simple public

-- Variable substitutions (renamings).

module VarSubst where

  subst : Subst Fin
  subst = record
    { simple      = record { var = Fun.id; weaken = suc }
    ; application = record { _/_ = flip lookup }
    }

  open Subst subst public

-- "Term" substitutions.

record TermSubst (T : Pred ℕ L.zero) : Set₁ where
  field
    var : ∀ {n} → Fin n → T n
    app : ∀ {T′ : Pred ℕ L.zero} → Lift T′ T → ∀ {m n} → T m → Sub T′ m n → T n

  module Lifted {T′ : Pred ℕ L.zero} (lift : Lift T′ T) where
    application : Application T T′
    application = record { _/_ = app lift }

    open Lift lift public
    open Application application public

  varLift : Lift Fin T
  varLift = record { simple = VarSubst.simple; lift = var }

  infix 8 _/Var_

  _/Var_ : ∀ {m n} → T m → Sub Fin m n → T n
  _/Var_ = app varLift

  simple : Simple T
  simple = record
    { var    = var
    ; weaken = λ t → t /Var VarSubst.wk
    }

  termLift : Lift T T
  termLift = record { simple = simple; lift = Fun.id }

  subst : Subst T
  subst = record
    { simple      = simple
    ; application = Lifted.application termLift
    }

  open Subst subst public hiding (var; simple)

ext: agda


text:
module IORef where

  data Unit : Set where
    unit : Unit

  data Pair (A B : Set) : Set where
    pair : A -> B -> Pair A B

  fst : {A B : Set} -> Pair A B -> A
  fst (pair a b) = a

  snd : {A B : Set} -> Pair A B -> B
  snd (pair a b) = b

  data Nat : Set where
    zero : Nat
    suc : Nat -> Nat

  data Fin : Nat -> Set where
    fz : {n : Nat} -> Fin (suc n)
    fs : {n : Nat} -> Fin n -> Fin (suc n)

  infixr 40 _::_
  infixl 20 _!_

  data Vec (A : Set) : Nat -> Set where
    []   : Vec A zero
    _::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

  _!_ : {A : Set}{n : Nat} -> Vec A n -> Fin n -> A
  []	  ! ()
  x :: _  ! fz	   = x
  _ :: xs ! (fs i) = xs ! i

  Loc : Nat -> Set
  Loc = Fin

  -- A universe. IORefs can store data of type el(u), for some u : U
  postulate
    U : Set
    el : U -> Set

  -- Shapes tell you what types live on the heap.
  Shape : Nat -> Set
  Shape n = Vec U n -- Fin n -> U

  -- Shapes can grow as you allocate new memory
  _||_ : {n : Nat} -> Shape n -> U -> Shape (suc n)
  xs || u = u :: xs

  infixl 40 _▻_
  infixl 60 _[_:=_] _[_]

  -- The heap maps locations to elements of the right type.
  data Heap : {n : Nat}(s : Shape n) -> Set where
    ε	: Heap []
    _▻_ : {n : Nat}{s : Shape n}{a : U} -> Heap s -> el a -> Heap (s || a)

--   Heap : {n : Nat} -> Shape n -> Set
--   Heap {n} shape = (k : Fin n) -> el (shape ! k)

  _[_:=_] : {n : Nat}{s : Shape n} -> Heap s -> (l : Loc n) -> el (s ! l) -> Heap s
  ε	  [ ()   := _ ]
  (h ▻ _) [ fz   := x ] = h ▻ x
  (h ▻ y) [ fs i := x ] = h [ i := x ] ▻ y

  _[_] : {n : Nat}{s : Shape n} -> Heap s -> (l : Loc n) -> el (s ! l)
  ε	  [ ()	 ]
  (h ▻ x) [ fz	 ] = x
  (h ▻ _) [ fs i ] = h [ i ]

--   (h [ fz := x ]) fz = x
--   (h [ fz := x ]) (fs i) = h (fs i)
--   (h [ fs i := x ]) fz = h fz
--   _[_:=_] {._}{_ :: s} h (fs i) x (fs j) = _[_:=_] {s = s} (\z -> h (fs z)) i x j

  -- Well-scoped, well-typed IORefs
  data IO (A : Set) : {n m : Nat} -> Shape n -> Shape m -> Set where
    Return : {n : Nat}{s : Shape n} -> A -> IO A s s
    WriteIORef : {n m : Nat}{s : Shape n}{t : Shape m} ->
      (loc : Loc n) -> el (s ! loc) -> IO A s t -> IO A s t
    ReadIORef : {n m : Nat}{s : Shape n}{t : Shape m} ->
      (loc : Loc n) -> (el (s ! loc) -> IO A s t) -> IO A s t
    NewIORef : {n m : Nat}{s : Shape n}{t : Shape m}{u : U} ->
      el u -> IO A (s || u) t -> IO A s t

  -- Running IO programs
  run : {A : Set} -> {n m : Nat} -> {s : Shape n} -> {t : Shape m}
       -> Heap s -> IO A s t -> Pair A (Heap t)
  run heap (Return x) = pair x heap
  run heap (WriteIORef l x io) = run (heap [ l := x ]) io
  run heap (ReadIORef l k) = run heap (k (heap [ l ]))
  run heap (NewIORef x k) = run (heap ▻ x) k

  infixr 10 _>>=_ _>>_

  _>>=_ : {A B : Set}{n₁ n₂ n₃ : Nat}{s₁ : Shape n₁}{s₂ : Shape n₂}{s₃ : Shape n₃} ->
	  IO A s₁ s₂ -> (A -> IO B s₂ s₃) -> IO B s₁ s₃
  Return x	   >>= f = f x
  WriteIORef r x k >>= f = WriteIORef r x (k >>= f)
  ReadIORef r k	   >>= f = ReadIORef r (\x -> k x >>= f)
  NewIORef x k	   >>= f = NewIORef x (k >>= f)

  _>>_ : {A B : Set}{n₁ n₂ n₃ : Nat}{s₁ : Shape n₁}{s₂ : Shape n₂}{s₃ : Shape n₃} ->
	 IO A s₁ s₂ -> IO B s₂ s₃ -> IO B s₁ s₃
  a >> b = a >>= \_ -> b

  -- The operations without CPS

  data IORef : {n : Nat}(s : Shape n) -> U -> Set where
    ioRef : {n : Nat}{s : Shape n}(r : Loc n) -> IORef s (s ! r)

  return : {A : Set}{n : Nat}{s : Shape n} -> A -> IO A s s
  return = Return

  writeIORef : {n : Nat}{s : Shape n}{a : U} ->
	       IORef s a -> el a -> IO Unit s s
  writeIORef (ioRef r) x = WriteIORef r x (Return unit)

  readIORef : {n : Nat}{s : Shape n}{a : U} -> IORef s a -> IO (el a) s s
  readIORef (ioRef r) = ReadIORef r Return

  newIORef : {n : Nat}{s : Shape n}{a : U} -> el a -> IO (IORef (s || a) a) s (s || a)
  newIORef x = NewIORef x (Return (ioRef fz))

  -- Some nice properties

  infix 10 _==_ _≡_

  data _==_ {A : Set}(x : A) : A -> Set where
    refl : x == x

  subst : {A : Set}(P : A -> Set){x y : A} -> x == y -> P y -> P x
  subst {A} P refl Px = Px

  cong : {A B : Set}(f : A -> B){x y : A} -> x == y -> f x == f y
  cong {A} f refl = refl

  trans : {A : Set}{x y z : A} -> x == y -> y == z -> x == z
  trans {A} refl p = p

  fsteq : {A B : Set}{x y : A}{z w : B} -> pair x z == pair y w -> x == y
  fsteq {A}{B} refl = refl

  -- Lemmas

  update-lookup : {n : Nat}{s : Shape n}(h : Heap s)(r : Loc n)(x : el (s ! r)) ->
		  h [ r := x ] [ r ] == x
  update-lookup ε	()     _
  update-lookup	(h ▻ _) fz     x = refl
  update-lookup (h ▻ _) (fs i) x = update-lookup h i x

  update-update : {n : Nat}{s : Shape n}(h : Heap s)(r : Loc n)(x y : el (s ! r)) ->
		  h [ r := x ] [ r := y ] == h [ r := y ]
  update-update ε	()     _ _
  update-update (h ▻ _)  fz    x y = refl
  update-update (h ▻ z) (fs i) x y = cong (\ ∙ -> ∙ ▻ z) (update-update h i x y)

  -- Equality of monadic computations

  data _≡_ {A : Set}{n m : Nat}{s : Shape n}{t : Shape m}(io₁ io₂ : IO A s t) : Set where
    eqIO : ((h : Heap s) -> run h io₁ == run h io₂) -> io₁ ≡ io₂

  uneqIO : {A : Set}{n m : Nat}{s : Shape n}{t : Shape m}{io₁ io₂ : IO A s t} ->
	   io₁ ≡ io₂ -> (h : Heap s) -> run h io₁ == run h io₂
  uneqIO (eqIO e) = e

  -- Congruence properties

  cong->> : {A B : Set}{n₁ n₂ n₃ : Nat}{s₁ : Shape n₁}{s₂ : Shape n₂}{s₃ : Shape n₃}
	    {io₁₁ io₁₂ : IO A s₁ s₂}{io₂₁ io₂₂ : A -> IO B s₂ s₃} ->
	    io₁₁ ≡ io₁₂ -> ((x : A) -> io₂₁ x ≡ io₂₂ x) -> io₁₁ >>= io₂₁ ≡ io₁₂ >>= io₂₂
  cong->> {A}{B}{s₁ = s₁}{s₂}{s₃}{io₁₁}{io₁₂}{io₂₁}{io₂₂}(eqIO eq₁) eq₂ =
      eqIO (prf io₁₁ io₁₂ io₂₁ io₂₂ eq₁ eq₂)
    where
      prf : {n₁ n₂ n₃ : Nat}{s₁ : Shape n₁}{s₂ : Shape n₂}{s₃ : Shape n₃}
	    (io₁₁ io₁₂ : IO A s₁ s₂)(io₂₁ io₂₂ : A -> IO B s₂ s₃) ->
	    ((h : Heap s₁) -> run h io₁₁ == run h io₁₂) ->
	    ((x : A) -> io₂₁ x ≡ io₂₂ x) ->
	    (h : Heap s₁) -> run h (io₁₁ >>= io₂₁) == run h (io₁₂ >>= io₂₂)
      prf (Return x) (Return y) k₁ k₂ eq₁ eq₂ h =
	  subst (\ ∙ -> run h (k₁ ∙) == run h (k₂ y)) x=y (uneqIO (eq₂ y) h)
	where
	  x=y : x == y
	  x=y = fsteq (eq₁ h)
      prf (WriteIORef r₁ x₁ k₁) (Return y) k₂ k₃ eq₁ eq₂ h = ?
      -- ... boring proofs

  -- Monad laws

    -- boring...

  -- IO laws

  new-read : {n : Nat}{s : Shape n}{a : U}(x : el a) ->
	     newIORef {s = s} x >>= readIORef ≡
	     newIORef x >> return x
  new-read x = eqIO \h -> refl

  write-read : {n : Nat}{s : Shape n}{a : U}(r : IORef s a)(x : el a) ->
	       writeIORef r x >> readIORef r
	       ≡ writeIORef r x >> return x
  write-read (ioRef r) x =
    eqIO \h -> cong (\ ∙ -> pair ∙ (h [ r := x ]))
		    (update-lookup h r x)

  write-write : {n : Nat}{s : Shape n}{a : U}(r : IORef s a)(x y : el a) ->
		writeIORef r x >> writeIORef r y
		≡ writeIORef r y
  write-write (ioRef r) x y =
    eqIO \h -> cong (\ ∙ -> pair unit ∙) (update-update h r x y)

  -- Some separation properties would be nice

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
{-# OPTIONS --cubical --no-import-sorts --prop #-}

module Utils where

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)
open import Function.Base

variable
  ℓ ℓ' ℓ'' : Level

module Test where
  import Algebra.Properties.BooleanAlgebra

  open import Algebra.Bundles

  module _ (B : BooleanAlgebra ℓ ℓ') where
    open BooleanAlgebra B
    open import Algebra.Definitions _≈_

    ∨-complementˡ : LeftInverse ⊤ ¬_ _∨_
    ∨-complementˡ = {! comm+invʳ⇒invˡ ∨-comm ∨-complementʳ !}

    ∨-complement : Inverse ⊤ ¬_ _∨_
    ∨-complement = {! ∨-complementˡ , ∨-complementʳ !}

    ∧-complementˡ : LeftInverse ⊥ ¬_ _∧_
    ∧-complementˡ = {! comm+invʳ⇒invˡ ∧-comm ∧-complementʳ !}

    ∧-complement : Inverse ⊥ ¬_ _∧_
    ∧-complement = {! ∧-complementˡ , ∧-complementʳ !}

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
-- open import Cubical.Structures.CommRing
-- open import Cubical.Relation.Nullary.Base -- ¬_
-- open import Cubical.Relation.Binary.Base
-- open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)
-- open import Cubical.Data.Empty renaming (elim to ⊥-elim) -- `⊥` and `elim`
-- -- open import Cubical.Structures.Poset
-- open import Cubical.Foundations.Function
-- open import Function.Base using (_∋_)
-- open import Function.Base using (it) -- instance search

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Logic
-- open import Algebra.Definitions
-- open import Cubical.Data.Empty
open import Cubical.HITs.PropositionalTruncation

import Cubical.Data.Empty as ⊥
open import Cubical.Data.Unit.Base

⊥↑ : ∀{ℓ} → hProp ℓ
⊥↑ = Lift ⊥.⊥ , λ ()

⊤↑ : ∀{ℓ} → hProp ℓ
⊤↑ = Lift Unit , isOfHLevelLift 1 (λ _ _ _ → tt)

-- _ = {! ⇔toPath!}

⊔-complementˡ :  ∀ x → ¬ x ⊔ x ≡ ⊤↑ -- LeftInverse _≡_ ⊤ ¬_ _⊔_
⊔-complementˡ = {! comm+invʳ⇒invˡ ⊔-comm ⊔-complementʳ !}

-- ⊔-complementʳ : ∀ x → x ⊔ ¬ x ≡ ∥ [ ⊤ ] ∥ₚ
-- ⊔-complementʳ : ∀(x : hProp ℓ) → x ⊔ ¬ x ≡ ((hProp ℓ) ∋ ⊤)
⊔-complementʳ : ∀(x : hProp ℓ) → x ⊔ ¬ x ≡ ⊤↑
⊔-complementʳ x =  λ i → {! ⊔-comm x (¬ x) i !}

⊔-complement : (∀ x → ¬ x ⊔ x ≡ ⊤↑) × (∀ x → x ⊔ ¬ x ≡ ⊤↑) -- Inverse _≡_ ⊤ ¬_ _⊔_
⊔-complement = ⊔-complementˡ , {! ⊔-complementʳ !}

-- agda deduces
--         Σ Type (λ A → (x y : A) → x ≡ y)
-- hProp normalizes to
--    λ ℓ → Σ (Type ℓ) (λ A → (x y : A) → x ≡ y)
--
⊓-complementˡ :  ∀ x → ¬ x ⊓ x ≡ ⊥ -- LeftInverse _≡_ ⊥ ¬_ _⊓_
⊓-complementˡ = {! isProp!} -- comm+invʳ⇒invˡ ⊓-comm ⊓-complementʳ

⊓-complementʳ :  ∀ x → x ⊓ ¬ x ≡ ⊥
⊓-complementʳ = {!!}

⊓-complement : (∀ x → ¬ x ⊓ x ≡ ⊥) × (∀ x → x ⊓ ¬ x ≡ ⊥) -- Inverse _≡_ ⊥ ¬_ _⊓_
⊓-complement = ⊓-complementˡ , ⊓-complementʳ

⊓-⊔-distribʳ : (P : hProp ℓ) (Q : hProp ℓ')(R : hProp ℓ'')
  → (Q ⊔ R) ⊓ P ≡ (Q ⊓ P) ⊔ (R ⊓ P)
⊓-⊔-distribʳ P Q R = (
  (Q ⊔ R) ⊓ P       ≡⟨ ⊓-comm _ _ ⟩
   P ⊓ (Q ⊔ R)      ≡⟨ ⊓-⊔-distribˡ P Q R ⟩
  (P ⊓ Q) ⊔ (P ⊓ R) ≡⟨ ( λ i → ⊓-comm P Q i ⊔ ⊓-comm P R i) ⟩
  (Q ⊓ P) ⊔ (R ⊓ P) ∎)

_ : isProp ≡ (λ(A : Type ℓ) → (x y : A) → x ≡ y)
_ = refl

-- `sq` stands for "squashed" and |_| is the constructor for ∥_∥
--
--   data ∥_∥ {ℓ} (A : Type ℓ) : Type ℓ where
--     ∣_∣ : A → ∥ A ∥
--     squash : ∀ (x y : ∥ A ∥) → x ≡ y
--
-- (see https://ice1000.org/2018/12-06-CubicalAgda.html#propositional-truncation )
-- we also have
--
--   hProp    ℓ  = Σ[ A ∈ Type ℓ ]  (∀( x  y : A)    → x ≡ y)
--   isContr {ℓ} = λ( A : Type ℓ ) → Σ[ x ∈ A ] (∀ y → x ≡ y)
--   isProp  {ℓ} = λ( A : Type ℓ ) → ∀( x  y : A)    → x ≡ y
--
-- and in `Cubical.Foundations.Id` we have
--
--   postulate
--     Id : ∀ {ℓ} {A : Set ℓ} → A → A → Set ℓ
--   _≡_ : ∀ {ℓ} {A : Type ℓ} → A → A → Type ℓ
--   _≡_ = Id
--
-- which is imported in `Cubical.Foundations.Everything`, but _≡_ is hidden in favour of the _≡_ from `Agda.Builtin.Cubical.Path`:
--
--   _≡_ : ∀ {ℓ} {A : Set ℓ} → A → A → Set ℓ
--   _≡_ {A = A} = PathP (λ i → A)
--
-- we have conversion functions between `Id` and `PathP`

-- recall from https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html
--
--   is-center                X c = (x   : X) → c ≡ x
--   is-singleton             X   = Σ  c ꞉ X , is-center X c
--   is-subsingleton          X   = (x y : X) → x ≡ y
--   𝟘-is-subsingleton            : is-subsingleton 𝟘
--   singletons-are-subsingletons : (X : 𝓤 ̇ ) → is-singleton X → is-subsingleton X
--   𝟙-is-subsingleton            : is-subsingleton 𝟙
--
-- now,
--   see https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#axiomatic-approach
--   see https://ice1000.org/2018/12-06-CubicalAgda.html#propositional-truncation
--     However I would not only use recPropTrunc explicitly as we can just use pattern-matching to define functions out of HITs.
--   see https://cstheory.stackexchange.com/questions/30542/squash-type-vs-propositional-truncation-type
--     Squash types correspond to judgmental truncation, not propositional truncation.
--     In a type theory without a type for judgmental equality, there's non much of a way to make use of an inhabitant of a squash type;
--     there's no way to write an eliminator into any type except another squash type.
--     Relatedly, having squash types, as presented in the book you linked, makes typechecking undecidable;
--     having propositional truncation types does not result in this drawback.
--   there is https://github.com/agda/cubical/pull/136
--     Elimination of propositional truncation to higher types

import Cubical.Foundations.Id
import Cubical.HITs.PropositionalTruncation.Properties -- look here for examples

∥∥-isProp : {A : Type ℓ} → ∀ (x y : ∥ A ∥) → x ≡ y
∥∥-isProp {ℓ = ℓ} {A = A} x y = (squash x y)

_ = propTruncIsProp

propTruncIsProp' : {A : Type ℓ} → isProp ∥ A ∥
propTruncIsProp' x y = squash x y

{-

t0 : {A : Type ℓ} → (x y : ∥ A ∥) → x ≡ y -- isProp (∥ A ∥)
t0 x ∣ y ∣ = squash x ∣ y ∣
-- Goal: ∥ A ∥
-- ———— Boundary ——————————————————————————————————————————————
-- i = i0 ⊢ t0 x y₀ j
-- i = i1 ⊢ t0 x y₁ j
-- j = i0 ⊢ x
-- j = i1 ⊢ squash y₀ y₁ i
t0 x (squash y₀ y₁ i) j = {! t0  !}

-}

{-
-- Goal: ∣ x ∣ ≡ ∣ y ∣
t0 ∣ x ∣ ∣ y ∣ = squash ∣ x ∣ ∣ y ∣

-- Goal: ∣ x ∣ ≡ squash y₀ y₁ i
-- ———— Boundary ——————————————————————————————————————————————
-- i = i0 ⊢ t0 ∣ x ∣ y₀
-- i = i1 ⊢ t0 ∣ x ∣ y₁
t0 ∣ x ∣ (squash y₀ y₁ i) = squash ∣ x ∣ (squash y₀ y₁ i) -- {! squash ∣ x ∣ (squash y₀ y₁ i)!} -- {! λ j → squash ∣ x ∣ (squash y₁ y₂ j) {!  !}  !}
t0 (squash x₁ x₂ i) ∣ y ∣ = squash (squash x₁ x₂ i) ∣ y ∣
t0 (squash x₁ x₂ i) (squash y₁ y₂ j) = squash (squash x₁ x₂ i) (squash y₁ y₂ j)
-}

-- Definition 2.4.3. The propositional truncation of a type X
--   is a proposition ∥ X ∥
--   together with a truncation map |_| : X → ∥ X ∥
--   such that for any other proposition Q, given a map g : X → Q, we obtain a map h : ∥ X ∥ → Q.
--
-- Remark 2.4.4. The uniqueness of the obtained map ∥ X ∥ → Q follows from the fact that Q is a proposition, and function extensionality
--
-- The propositional truncation ∥ X ∥ of a type X is a proposition. We may say, quite simply,
-- that we have a constructor sq which is a proof that the type ∥ X ∥ is a squashed to be a propo-
-- sition: it takes two elements of ∥ X ∥ and gives a proof that they are identical, i.e. squashed
-- together.

-- Definition 2.4.7.
-- We refer to types that are propositions as properties.
-- We refer to types that potentially have several witnesses as structure.

{-
module _ {ℓ} (X Y : Type ℓ) (g : X → Y) where

  f : ∥ X ∥ → Y
  f ∣ x ∣ = g x
  f (squash x₀ x₁ i) = {!  !}
-}

-- well, that might not work at all
-- ⊓-unliftˡ : {P : hProp ℓ} {Q : hProp ℓ'}

import Cubical.HITs.PropositionalTruncation.Properties

-- _ : (P : hProp P.ℓ) (Q : hProp Q.ℓ) (R : hProp R.ℓ) → (hProp P.ℓ → hProp Q.ℓ → hProp R.ℓ) → h
-- _ = ?

--_ = _≡ₚ_

⊓-identityˡ-↑ : (P : hProp ℓ) → ⊤↑ {ℓ} ⊓ P ≡ P
⊓-identityˡ-↑ _ = ⇔toPath snd  λ x → lift tt , x

-- \ is \\
-- ↑ is \u

private
  lemma : ∀ x y → x ⊓ y ≡ ⊥ → x ⊔ y ≡ ⊤ → ¬ x ≡ y
  lemma x y x⊓y=⊥ x⊔y=⊤ = (
    ¬ x                    ≡⟨ sym (⊓-identityʳ _) ⟩
    ¬ x ⊓ ⊤                ≡⟨ (λ i → ¬ x ⊓ x⊔y=⊤ (~ i) ) ⟩
    ¬ x ⊓ (x ⊔ y)          ≡⟨ ⊓-⊔-distribˡ (¬ x) x y  ⟩
    (¬ x ⊓ x) ⊔ (¬ x ⊓ y)  ≡⟨ (λ i → ⊓-complementˡ x i ⊔ (¬ x ⊓ y)) ⟩
    ⊥ ⊔ (¬ x ⊓ y)          ≡⟨ (λ i → x⊓y=⊥ (~ i) ⊔ (¬ x ⊓ y)) ⟩
    (x ⊓ y) ⊔ (¬ x ⊓ y)    ≡⟨  sym (⊓-⊔-distribʳ y x (¬ x)) ⟩
    (x ⊔ ¬ x) ⊓ y          ≡⟨ (λ i → (⊔-complementʳ x) i ⊓ y ) ⟩
    ⊤↑ ⊓ y                 ≡⟨ ⊓-identityˡ-↑ _ ⟩
    y                      ∎)

data Prop2Type (P : Prop ℓ) : Type (ℓ-suc ℓ) where
  inₚ : (p : P) → Prop2Type P

Prop-to-hProp : Prop ℓ → hProp (ℓ-suc ℓ)
Prop-to-hProp P = Prop2Type P ,  λ{ (inₚ x) (inₚ y) → refl }

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some code related to propositional equality that relies on the K
-- rule
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Relation.Binary.PropositionalEquality.WithK where

open import Axiom.UniquenessOfIdentityProofs.WithK
open import Relation.Binary
open import Relation.Binary.PropositionalEquality.Core

------------------------------------------------------------------------
-- Re-exporting safe erasure function

-- ≡-erase ignores its `x ≡ y` argument and reduces to refl whenever
-- x and y are judgmentally equal. This is useful when the computation
-- producing the proof `x ≡ y` is expensive.

open import Agda.Builtin.Equality.Erase
  using ()
  renaming ( primEraseEquality to ≡-erase )
  public

------------------------------------------------------------------------
-- Proof irrelevance

≡-irrelevant : ∀ {a} {A : Set a} → Irrelevant {A = A} _≡_
≡-irrelevant = uip

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 1.0

≡-irrelevance = ≡-irrelevant
{-# WARNING_ON_USAGE ≡-irrelevance
"Warning: ≡-irrelevance was deprecated in v1.0.
Please use ≡-irrelevant instead."
#-}


text:
{-# OPTIONS --without-K --exact-split #-}

module 13-circle where

import 12-univalence
open 12-univalence public

{- Section 11.1 The induction principle of the circle -}

free-loops :
  { l1 : Level} (X : UU l1) → UU l1
free-loops X = Σ X (λ x → Id x x)

base-free-loop :
  { l1 : Level} {X : UU l1} → free-loops X → X
base-free-loop = pr1

loop-free-loop :
  { l1 : Level} {X : UU l1} (l : free-loops X) →
  Id (base-free-loop l) (base-free-loop l)
loop-free-loop = pr2

-- Now we characterize the identity types of free loops

Eq-free-loops :
  { l1 : Level} {X : UU l1} (l l' : free-loops X) → UU l1
Eq-free-loops (pair x l) l' =
  Σ (Id x (pr1 l')) (λ p → Id (l ∙ p) (p ∙ (pr2 l')))

reflexive-Eq-free-loops :
  { l1 : Level} {X : UU l1} (l : free-loops X) → Eq-free-loops l l
reflexive-Eq-free-loops (pair x l) = pair refl right-unit

Eq-free-loops-eq :
  { l1 : Level} {X : UU l1} (l l' : free-loops X) →
  Id l l' → Eq-free-loops l l'
Eq-free-loops-eq l .l refl = reflexive-Eq-free-loops l

abstract
  is-contr-total-Eq-free-loops :
    { l1 : Level} {X : UU l1} (l : free-loops X) →
    is-contr (Σ (free-loops X) (Eq-free-loops l))
  is-contr-total-Eq-free-loops (pair x l) =
    is-contr-total-Eq-structure
      ( λ x l' p → Id (l ∙ p) (p ∙ l'))
      ( is-contr-total-path x)
      ( pair x refl)
      ( is-contr-is-equiv'
        ( Σ (Id x x) (λ l' → Id l l'))
        ( tot (λ l' α → right-unit ∙ α))
        ( is-equiv-tot-is-fiberwise-equiv
          ( λ l' → is-equiv-concat right-unit l'))
        ( is-contr-total-path l))

abstract
  is-equiv-Eq-free-loops-eq :
    { l1 : Level} {X : UU l1} (l l' : free-loops X) →
    is-equiv (Eq-free-loops-eq l l')
  is-equiv-Eq-free-loops-eq l =
    fundamental-theorem-id l
      ( reflexive-Eq-free-loops l)
      ( is-contr-total-Eq-free-loops l)
      ( Eq-free-loops-eq l)

dependent-free-loops :
  { l1 l2 : Level} {X : UU l1} (l : free-loops X) (P : X → UU l2) → UU l2
dependent-free-loops l P =
  Σ ( P (base-free-loop l))
    ( λ p₀ → Id (tr P (loop-free-loop l) p₀) p₀)

Eq-dependent-free-loops :
  { l1 l2 : Level} {X : UU l1} (l : free-loops X) (P : X → UU l2) →
  ( p p' : dependent-free-loops l P) → UU l2
Eq-dependent-free-loops (pair x l) P (pair y p) p' =
  Σ ( Id y (pr1 p'))
    ( λ q → Id (p ∙ q) ((ap (tr P l) q) ∙ (pr2 p')))

reflexive-Eq-dependent-free-loops :
  { l1 l2 : Level} {X : UU l1} (l : free-loops X) (P : X → UU l2) →
  ( p : dependent-free-loops l P) → Eq-dependent-free-loops l P p p
reflexive-Eq-dependent-free-loops (pair x l) P (pair y p) =
  pair refl right-unit

Eq-dependent-free-loops-eq :
  { l1 l2 : Level} {X : UU l1} (l : free-loops X) (P : X → UU l2) →
  ( p p' : dependent-free-loops l P) →
  Id p p' → Eq-dependent-free-loops l P p p'
Eq-dependent-free-loops-eq l P p .p refl =
  reflexive-Eq-dependent-free-loops l P p

abstract
  is-contr-total-Eq-dependent-free-loops :
    { l1 l2 : Level} {X : UU l1} (l : free-loops X) (P : X → UU l2) →
    ( p : dependent-free-loops l P) →
    is-contr (Σ (dependent-free-loops l P) (Eq-dependent-free-loops l P p))
  is-contr-total-Eq-dependent-free-loops (pair x l) P (pair y p) =
    is-contr-total-Eq-structure
      ( λ y' p' q → Id (p ∙ q) ((ap (tr P l) q) ∙ p'))
      ( is-contr-total-path y)
      ( pair y refl)
      ( is-contr-is-equiv'
        ( Σ (Id (tr P l y) y) (λ p' → Id p p'))
        ( tot (λ p' α → right-unit ∙ α))
        ( is-equiv-tot-is-fiberwise-equiv
          ( λ p' → is-equiv-concat right-unit p'))
        ( is-contr-total-path p))

abstract
  is-equiv-Eq-dependent-free-loops-eq :
    { l1 l2 : Level} {X : UU l1} (l : free-loops X) (P : X → UU l2)
    ( p p' : dependent-free-loops l P) →
    is-equiv (Eq-dependent-free-loops-eq l P p p')
  is-equiv-Eq-dependent-free-loops-eq l P p =
    fundamental-theorem-id p
      ( reflexive-Eq-dependent-free-loops l P p)
      ( is-contr-total-Eq-dependent-free-loops l P p)
      ( Eq-dependent-free-loops-eq l P p)

eq-Eq-dependent-free-loops :
  { l1 l2 : Level} {X : UU l1} (l : free-loops X) (P : X → UU l2)
  ( p p' : dependent-free-loops l P) →
  Eq-dependent-free-loops l P p p' → Id p p'
eq-Eq-dependent-free-loops l P p p' =
  inv-is-equiv (is-equiv-Eq-dependent-free-loops-eq l P p p')

ev-free-loop' :
  { l1 l2 : Level} {X : UU l1} (l : free-loops X) (P : X → UU l2) →
  ( (x : X) → P x) → dependent-free-loops l P
ev-free-loop' (pair x₀ p) P f = pair (f x₀) (apd f p)

induction-principle-circle :
  { l1 : Level} (l2 : Level) {X : UU l1} (l : free-loops X) →
  UU ((lsuc l2) ⊔ l1)
induction-principle-circle l2 {X} l =
  (P : X → UU l2) → sec (ev-free-loop' l P)

{- Section 11.2 The universal property of the circle -}

{- We first state the universal property of the circle -}

ev-free-loop :
  { l1 l2 : Level} {X : UU l1} (l : free-loops X) (Y : UU l2) →
  ( X → Y) → free-loops Y
ev-free-loop l Y f = pair (f (pr1 l)) (ap f (pr2 l))

universal-property-circle :
  { l1 : Level} (l2 : Level) {X : UU l1} (l : free-loops X) → UU _
universal-property-circle l2 l =
  ( Y : UU l2) → is-equiv (ev-free-loop l Y)

{- A fairly straightforward proof of the universal property of the circle
   factors through the dependent universal property of the circle. -}

dependent-universal-property-circle :
  { l1 : Level} (l2 : Level) {X : UU l1} (l : free-loops X) →
  UU ((lsuc l2) ⊔ l1)
dependent-universal-property-circle l2 {X} l =
  ( P : X → UU l2) → is-equiv (ev-free-loop' l P)

{- We first prove that the dependent universal property of the circle follows
   from the induction principle of the circle. To show this, we have to show
   that the section of ev-free-loop' is also a retraction. This construction
   is also by the induction principle of the circle, but it requires (a minimal
   amount of) preparations. -}

Eq-subst :
  { l1 l2 : Level} {X : UU l1} {P : X → UU l2} (f g : (x : X) → P x) →
  X → UU _
Eq-subst f g x = Id (f x) (g x)

tr-Eq-subst :
  { l1 l2 : Level} {X : UU l1} {P : X → UU l2} (f g : (x : X) → P x)
  { x y : X} (p : Id x y) (q : Id (f x) (g x)) (r : Id (f y) (g y))→
  ( Id ((apd f p) ∙ r) ((ap (tr P p) q) ∙ (apd g p))) →
  ( Id (tr (Eq-subst f g) p q) r)
tr-Eq-subst f g refl q .((ap id q) ∙ refl) refl =
  inv (right-unit ∙ (ap-id q))

dependent-free-loops-htpy :
  {l1 l2 : Level} {X : UU l1} {l : free-loops X} {P : X → UU l2}
  {f g : (x : X) → P x} →
  ( Eq-dependent-free-loops l P (ev-free-loop' l P f) (ev-free-loop' l P g)) →
  ( dependent-free-loops l (λ x → Id (f x) (g x)))
dependent-free-loops-htpy {l = (pair x l)} (pair p q) =
  pair p (tr-Eq-subst _ _ l p p q)

isretr-ind-circle :
  { l1 l2 : Level} {X : UU l1} (l : free-loops X) →
  ( ind-circle : induction-principle-circle l2 l) (P : X → UU l2) →
  ( (pr1 (ind-circle P)) ∘ (ev-free-loop' l P)) ~ id
isretr-ind-circle l ind-circle P f =
  eq-htpy
    ( pr1
      ( ind-circle
        ( λ t → Id (pr1 (ind-circle P) (ev-free-loop' l P f) t) (f t)))
      ( dependent-free-loops-htpy
        ( Eq-dependent-free-loops-eq l P _ _
          ( pr2 (ind-circle P) (ev-free-loop' l P f)))))

abstract
  dependent-universal-property-induction-principle-circle :
    { l1 l2 : Level} {X : UU l1} (l : free-loops X) →
    induction-principle-circle l2 l → dependent-universal-property-circle l2 l
  dependent-universal-property-induction-principle-circle l ind-circle P =
    is-equiv-has-inverse
      ( pr1 (ind-circle P))
      ( pr2 (ind-circle P))
      ( isretr-ind-circle l ind-circle P)

{- Now that we have established the dependent universal property, we can
   reduce the (non-dependent) universal property to the dependent case. We do
   so by constructing a commuting triangle relating ev-free-loop to
   ev-free-loop' via a comparison equivalence. -}

tr-triv :
  {i j : Level} {A : UU i} {B : UU j} {x y : A} (p : Id x y) (b : B) →
  Id (tr (λ (a : A) → B) p b) b
tr-triv refl b = refl

apd-triv :
  {i j : Level} {A : UU i} {B : UU j} (f : A → B) {x y : A}
  (p : Id x y) → Id (apd f p) ((tr-triv p (f x)) ∙ (ap f p))
apd-triv f refl = refl

comparison-free-loops :
  { l1 l2 : Level} {X : UU l1} (l : free-loops X) (Y : UU l2) →
  free-loops Y → dependent-free-loops l (λ x → Y)
comparison-free-loops l Y =
  tot (λ y l' → (tr-triv (pr2 l) y) ∙ l')

abstract
  is-equiv-comparison-free-loops :
    { l1 l2 : Level} {X : UU l1} (l : free-loops X) (Y : UU l2) →
    is-equiv (comparison-free-loops l Y)
  is-equiv-comparison-free-loops l Y =
    is-equiv-tot-is-fiberwise-equiv
      ( λ y → is-equiv-concat (tr-triv (pr2 l) y) y)

triangle-comparison-free-loops :
  { l1 l2 : Level} {X : UU l1} (l : free-loops X) (Y : UU l2) →
  ( (comparison-free-loops l Y) ∘ (ev-free-loop l Y)) ~
  ( ev-free-loop' l (λ x → Y))
triangle-comparison-free-loops (pair x l) Y f =
  eq-Eq-dependent-free-loops
    ( pair x l)
    ( λ x → Y)
    ( comparison-free-loops (pair x l) Y (ev-free-loop (pair x l) Y f))
    ( ev-free-loop' (pair x l) (λ x → Y) f)
    ( pair refl (right-unit ∙ (inv (apd-triv f l))))

abstract
  universal-property-dependent-universal-property-circle :
    { l1 l2 : Level} {X : UU l1} (l : free-loops X) →
    ( dependent-universal-property-circle l2 l) →
    ( universal-property-circle l2 l)
  universal-property-dependent-universal-property-circle l dup-circle Y =
    is-equiv-right-factor
      ( ev-free-loop' l (λ x → Y))
      ( comparison-free-loops l Y)
      ( ev-free-loop l Y)
      ( htpy-inv (triangle-comparison-free-loops l Y))
      ( is-equiv-comparison-free-loops l Y)
      ( dup-circle (λ x → Y))

{- Now we get the universal property of the circle from the induction principle
   of the circle by composing the earlier two proofs. -}

abstract
  universal-property-induction-principle-circle :
    { l1 l2 : Level} {X : UU l1} (l : free-loops X) →
    induction-principle-circle l2 l → universal-property-circle l2 l
  universal-property-induction-principle-circle l =
    ( universal-property-dependent-universal-property-circle l) ∘
    ( dependent-universal-property-induction-principle-circle l)

unique-mapping-property-circle :
  { l1 : Level} (l2 : Level) {X : UU l1} (l : free-loops X) →
  UU (l1 ⊔ (lsuc l2))
unique-mapping-property-circle l2 {X} l =
  ( Y : UU l2) (l' : free-loops Y) →
    is-contr (Σ (X → Y) (λ f → Eq-free-loops (ev-free-loop l Y f) l'))

abstract
  unique-mapping-property-universal-property-circle :
    { l1 l2 : Level} {X : UU l1} (l : free-loops X) →
    universal-property-circle l2 l →
    unique-mapping-property-circle l2 l
  unique-mapping-property-universal-property-circle l up-circle Y l' =
    is-contr-is-equiv'
      ( fib (ev-free-loop l Y) l')
      ( tot (λ f → Eq-free-loops-eq (ev-free-loop l Y f) l'))
      ( is-equiv-tot-is-fiberwise-equiv
        ( λ f → is-equiv-Eq-free-loops-eq (ev-free-loop l Y f) l'))
      ( is-contr-map-is-equiv (up-circle Y) l')

{- We show that if a type with a free loop satisfies the induction principle
   of the circle with respect to any universe level, then it satisfies the
   induction principle with respect to the zeroth universe level. -}

naturality-tr-fiberwise-transformation :
  { l1 l2 l3 : Level} {X : UU l1} {P : X → UU l2} {Q : X → UU l3}
  ( f : (x : X) → P x → Q x) {x y : X} (α : Id x y) (p : P x) →
  Id (tr Q α (f x p)) (f y (tr P α p))
naturality-tr-fiberwise-transformation f refl p = refl

functor-dependent-free-loops :
  { l1 l2 l3 : Level} {X : UU l1} (l : free-loops X)
  { P : X → UU l2} {Q : X → UU l3} (f : (x : X) → P x → Q x) →
  dependent-free-loops l P → dependent-free-loops l Q
functor-dependent-free-loops l {P} {Q} f =
  toto
    ( λ q₀ → Id (tr Q (loop-free-loop l) q₀) q₀)
    ( f (base-free-loop l))
    ( λ p₀ α →
      ( naturality-tr-fiberwise-transformation f (loop-free-loop l) p₀) ∙
      ( ap (f (base-free-loop l)) α))

coherence-square-functor-dependent-free-loops :
  { l1 l2 l3 : Level} {X : UU l1} {P : X → UU l2} {Q : X → UU l3}
  ( f : (x : X) → P x → Q x) {x y : X} (α : Id x y)
  ( h : (x : X) → P x) →
  Id ( ( naturality-tr-fiberwise-transformation f α (h x)) ∙
       ( ap (f y) (apd h α)))
     ( apd (postcomp-Π f h) α)
coherence-square-functor-dependent-free-loops f refl h = refl

square-functor-dependent-free-loops :
  { l1 l2 l3 : Level} {X : UU l1} (l : free-loops X)
  { P : X → UU l2} {Q : X → UU l3} (f : (x : X) → P x → Q x) →
  ( (functor-dependent-free-loops l f) ∘ (ev-free-loop' l P)) ~
  ( (ev-free-loop' l Q) ∘ (postcomp-Π f))
square-functor-dependent-free-loops (pair x l) {P} {Q} f h =
  eq-Eq-dependent-free-loops (pair x l) Q
    ( functor-dependent-free-loops (pair x l) f
      ( ev-free-loop' (pair x l) P h))
    ( ev-free-loop' (pair x l) Q (postcomp-Π f h))
    ( pair refl
      ( right-unit ∙ (coherence-square-functor-dependent-free-loops f l h)))

abstract
  is-equiv-functor-dependent-free-loops-is-fiberwise-equiv :
    { l1 l2 l3 : Level} {X : UU l1} (l : free-loops X)
    { P : X → UU l2} {Q : X → UU l3} {f : (x : X) → P x → Q x}
    ( is-equiv-f : (x : X) → is-equiv (f x)) →
    is-equiv (functor-dependent-free-loops l f)
  is-equiv-functor-dependent-free-loops-is-fiberwise-equiv
    (pair x l) {P} {Q} {f} is-equiv-f =
    is-equiv-toto-is-fiberwise-equiv-is-equiv-base-map
      ( λ q₀ → Id (tr Q l q₀) q₀)
      ( _)
      ( _)
      ( is-equiv-f x)
      ( λ p₀ →
        is-equiv-comp'
          ( concat
            ( naturality-tr-fiberwise-transformation f l p₀)
            ( f x p₀))
          ( ap (f x))
          ( is-emb-is-equiv (f x) (is-equiv-f x) (tr P l p₀) p₀)
          ( is-equiv-concat
            ( naturality-tr-fiberwise-transformation f l p₀)
            ( f x p₀)))

abstract
  lower-dependent-universal-property-circle :
    { l1 l2 : Level} (l3 : Level) {X : UU l1} (l : free-loops X) →
    dependent-universal-property-circle (l2 ⊔ l3) l →
    dependent-universal-property-circle l3 l
  lower-dependent-universal-property-circle {l1} {l2} l3 l dup-circle P =
    is-equiv-left-is-equiv-right-square
      ( ev-free-loop' l P)
      ( ev-free-loop' l (λ x → raise l2 (P x)))
      ( postcomp-Π (λ x → map-raise l2 (P x)))
      ( functor-dependent-free-loops l (λ x → map-raise l2 (P x)))
      ( square-functor-dependent-free-loops l (λ x → map-raise l2 (P x)))
      ( is-equiv-postcomp-Π _ (λ x → is-equiv-map-raise l2 (P x)))
      ( is-equiv-functor-dependent-free-loops-is-fiberwise-equiv l
        ( λ x → is-equiv-map-raise l2 (P x)))
      ( dup-circle (λ x → raise l2 (P x)))

abstract
  lower-lzero-dependent-universal-property-circle :
    { l1 l2 : Level} {X : UU l1} (l : free-loops X) →
    dependent-universal-property-circle l2 l →
    dependent-universal-property-circle lzero l
  lower-lzero-dependent-universal-property-circle =
    lower-dependent-universal-property-circle lzero

{- The dependent universal property of the circle (and hence also the induction
   principle of the circle, implies that the circle is connected in the sense
   that for any family of propositions parametrized by the circle, if the
   proposition at the base holds, then it holds for any x : circle. -}

{- Exercises -}

-- Exercise 11.1

abstract
  is-connected-circle' :
    { l1 l2 : Level} {X : UU l1} (l : free-loops X) →
    ( dup-circle : dependent-universal-property-circle l2 l)
    ( P : X → UU l2) (is-prop-P : (x : X) → is-prop (P x)) →
    P (base-free-loop l) → (x : X) → P x
  is-connected-circle' l dup-circle P is-prop-P p =
    inv-is-equiv
      ( dup-circle P)
      ( pair p (center (is-prop-P _ (tr P (pr2 l) p) p)))

max_stars_repo_name: tadejpetric/HoTT-Intro

max_issues_repo_name: tadejpetric/HoTT-Intro

max_forks_repo_name: tadejpetric/HoTT-Intro


text:
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Data.Fin.Literals where

open import Agda.Builtin.Nat
  using (suc)
open import Agda.Builtin.FromNat
  renaming (Number to HasFromNat)
open import Cubical.Data.Fin.Base
  using (Fin; fromℕ≤)
open import Cubical.Data.Nat.Order.Recursive
  using (_≤_)

instance
  fromNatFin : {n : _} → HasFromNat (Fin (suc n))
  fromNatFin {n} = record
    { Constraint = λ m → m ≤ n
    ; fromNat    = λ m ⦃ m≤n ⦄ → fromℕ≤ m n m≤n
    }

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
{- Diamond operator. -}
module TemporalOps.Diamond.Functor where

open import CategoryTheory.Categories
open import CategoryTheory.Instances.Reactive
open import CategoryTheory.Functor
open import TemporalOps.Common
open import TemporalOps.Next
open import TemporalOps.Delay
open import Data.Product

-- Arbitrary delay
◇_ : τ -> τ
(◇ A) n = Σ[ k ∈ ℕ ] (delay A by k at n)
infixr 65 ◇_

-- ◇ instances
F-◇ : Endofunctor ℝeactive
F-◇ = record
    { omap      = ◇_
    ; fmap      = fmap-◇
    ; fmap-id   = fmap-◇-id
    ; fmap-∘    = fmap-◇-∘
    ; fmap-cong = fmap-◇-cong
    }
    where
    -- Lifting of ◇
    fmap-◇ : {A B : τ} -> A ⇴ B -> ◇ A ⇴ ◇ B
    fmap-◇ f n (k , v) = k , (Functor.fmap (F-delay k) f at n) v
    -- ◇ preserves identities
    fmap-◇-id : ∀ {A : τ} {n : ℕ} {a : (◇ A) n}
             -> (fmap-◇ (id {A}) at n) a ≡ a
    fmap-◇-id {A} {n} {zero , v} = refl
    fmap-◇-id {A} {zero} {suc k , v} = refl
    fmap-◇-id {A} {suc n} {suc k , v}
        rewrite delay-+ {A} 1 k n
              | Functor.fmap-id (F-delay (suc k)) {A} {suc n} {v}
        = refl
    -- ◇ preserves composition
    fmap-◇-∘ : ∀ {A B C : τ} {g : B ⇴ C} {f : A ⇴ B} {n : ℕ} {a : (◇ A) n}
            -> (fmap-◇ (g ∘ f) at n) a ≡ (fmap-◇ g ∘ fmap-◇ f at n) a
    fmap-◇-∘ {n = n} {zero , v} = refl
    fmap-◇-∘ {n = zero} {suc k , v} = refl
    fmap-◇-∘ {A} {B} {C} {g} {f} {suc n} {suc k , v}
        rewrite delay-+ {A} 1 k n
              | Functor.fmap-∘ (F-delay (suc k)) {A} {B} {C} {g} {f} {suc n} {v}
        = refl
    -- ▹ is congruent
    fmap-◇-cong : ∀{A B : τ} {f f′ : A ⇴ B}
            -> ({n : ℕ} {a : A at n}   -> f n a ≡ f′ n a)
            -> ({n : ℕ} {a : ◇ A at n} -> (fmap-◇ f at n) a
                                        ≡ (fmap-◇ f′ at n) a)
    fmap-◇-cong {A} e {n} {zero , a}
        rewrite delay-+-left0 {A} 0 n
              | e {n} {a} = refl
    fmap-◇-cong e {zero} {suc k , a} = refl
    fmap-◇-cong {A} {B} {f} {f′} e {suc n} {suc k , a}
        rewrite delay-+ {A} 1 k n
              | Functor.fmap-cong (F-delay (suc k)) {A} {B} {f} {f′} e {suc n} {a}
              = refl

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.SmashProduct.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Isomorphism
open import Cubical.HITs.Pushout.Base
open import Cubical.Data.Unit
open import Cubical.Data.Prod
open import Cubical.HITs.Wedge
open import Cubical.Foundations.Function
open import Cubical.Foundations.GroupoidLaws

data Smash {ℓ ℓ'} (A : Pointed ℓ) (B : Pointed ℓ') : Type (ℓ-max ℓ ℓ') where
  basel : Smash A B
  baser : Smash A B
  proj  : (x : typ A) → (y : typ B) → Smash A B
  gluel : (a : typ A) → proj a (pt B) ≡ basel
  gluer : (b : typ B) → proj (pt A) b ≡ baser

private
  variable
    ℓ ℓ' : Level
    A B C D : Pointed ℓ

Smash-map : (f : A →∙ C) (g : B →∙ D) → Smash A B → Smash C D
Smash-map f g basel = basel
Smash-map f g baser = baser
Smash-map (f , fpt) (g , gpt) (proj x y) = proj (f x) (g y)
Smash-map (f , fpt) (g , gpt) (gluel a i) = ((λ j → proj (f a) (gpt j)) ∙ gluel (f a)) i
Smash-map (f , fpt) (g , gpt) (gluer b i) = ((λ j → proj (fpt j) (g b)) ∙ gluer (g b)) i

-- Commutativity
comm : Smash A B → Smash B A
comm basel       = baser
comm baser       = basel
comm (proj x y)  = proj y x
comm (gluel a i) = gluer a i
comm (gluer b i) = gluel b i

commK : (x : Smash A B) → comm (comm x) ≡ x
commK basel       = refl
commK baser       = refl
commK (proj x y)  = refl
commK (gluel a x) = refl
commK (gluer b x) = refl

-- WIP below

SmashPt : (A : Pointed ℓ) (B : Pointed ℓ') → Pointed (ℓ-max ℓ ℓ')
SmashPt A B = (Smash A B , basel)

SmashPtProj : (A : Pointed ℓ) (B : Pointed ℓ') → Pointed (ℓ-max ℓ ℓ')
SmashPtProj A B = Smash A B , (proj (snd A) (snd B))

--- Alternative definition

i∧ : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'} → A ⋁ B → (typ A) × (typ B)
i∧ {A = A , ptA} {B = B , ptB} (inl x) = x , ptB
i∧ {A = A , ptA} {B = B , ptB} (inr x) = ptA , x
i∧ {A = A , ptA} {B = B , ptB} (push tt i) = ptA , ptB

_⋀_ : ∀ {ℓ ℓ'} → Pointed ℓ → Pointed ℓ' → Type (ℓ-max ℓ ℓ')
A ⋀ B = Pushout {A = (A ⋁ B)} (λ _ → tt) i∧

_⋀∙_ : ∀ {ℓ ℓ'} → Pointed ℓ → Pointed ℓ' → Pointed (ℓ-max ℓ ℓ')
A ⋀∙ B = Pushout {A = (A ⋁ B)} (λ _ → tt) i∧ , (inl tt)

_⋀→_ : (f : A →∙ C) (g : B →∙ D)  → A ⋀ B → C ⋀ D
(f ⋀→ g) (inl tt) = inl tt
((f , fpt) ⋀→ (g , gpt)) (inr (x , x₁)) = inr (f x , g x₁)
_⋀→_ {B = B} {D = D} (f ,  fpt) (b , gpt)  (push (inl x) i) = (push (inl (f x)) ∙ (λ i → inr (f x , gpt (~ i)))) i
_⋀→_ (f , fpt) (g , gpt) (push (inr x) i) = (push (inr (g x)) ∙ (λ i → inr (fpt (~ i) , g x))) i
_⋀→_ {A = A} {C = C} {B = B} {D = D} (f , fpt) (g , gpt) (push (push tt j) i) =
  hcomp (λ k → λ { (i = i0) → inl tt
                  ; (i = i1) → inr (fpt (~ k) , gpt (~ k))
                  ; (j = i0) → compPath-filler (push (inl (fpt (~ k))))
                                                ((λ i → inr (fpt (~ k) , gpt (~ i)))) k i
                  ; (j = i1) → compPath-filler (push (inr (gpt (~ k))))
                                                ((λ i → inr (fpt (~ i) , gpt (~ k)))) k i})
        (push (push tt j) i)

⋀→Smash : A ⋀ B → Smash A B
⋀→Smash (inl x) = basel
⋀→Smash (inr (x , x₁)) = proj x x₁
⋀→Smash (push (inl x) i) = gluel x (~ i)
⋀→Smash {A = A} {B = B} (push (inr x) i) = (sym (gluel (snd A)) ∙∙ gluer (snd B) ∙∙ sym (gluer x)) i
⋀→Smash {A = A} {B = B} (push (push a j) i) =
  hcomp (λ k → λ { (i = i0) → gluel (snd A) (k ∨ ~ j)
                  ; (i = i1) → gluer (snd B) (~ k ∧ j)
                  ; (j = i0) → gluel (snd A) (~ i)})
        (invSides-filler (gluel (snd A)) (gluer (snd B)) j (~ i))

Smash→⋀ : Smash A B → A ⋀ B
Smash→⋀ basel = inl tt
Smash→⋀ baser = inl tt
Smash→⋀ (proj x y) = inr (x , y)
Smash→⋀ (gluel a i) = push (inl a) (~ i)
Smash→⋀ (gluer b i) = push (inr b) (~ i)

{- associativity maps for smash produts. Proof pretty much direcly translated from https://github.com/ecavallo/redtt/blob/master/library/pointed/smash.red -}
private
  pivotl : (b b' : typ B)
         → Path (Smash A B) (proj (snd A) b) (proj (snd A) b')
  pivotl b b' i = (gluer b ∙ sym (gluer b')) i

  pivotr : (a a' : typ A)
         → Path (Smash A B) (proj a (snd B)) (proj a' (snd B))
  pivotr a a' i = (gluel a ∙ sym (gluel a')) i

  pivotlrId : {A : Pointed ℓ} {B : Pointed ℓ'} → _
  pivotlrId {A = A} {B = B} = rCancel (gluer (snd B)) ∙ sym (rCancel (gluel (snd A)))

  rearrange-proj : (c : fst C)
                → (Smash A B) → Smash (SmashPtProj C B) A
  rearrange-proj c basel = baser
  rearrange-proj c baser = basel
  rearrange-proj c (proj x y) = proj (proj c y) x
  rearrange-proj {C = C} c (gluel a i) =
    hcomp (λ k → λ { (i = i0) → proj (pivotr (snd C) c k) a
                    ; (i = i1) → baser})
          (gluer a i)
  rearrange-proj c (gluer b i) = gluel (proj c b) i

  rearrange-gluel : (s : Smash A B)
                 → Path (Smash (SmashPtProj C B) A) basel (rearrange-proj (snd C) s)
  rearrange-gluel {A = A} {B = B} {C = C} basel = sym (gluel (proj (snd C) (snd B))) ∙
                                                  gluer (snd A)
  rearrange-gluel baser = refl
  rearrange-gluel {A = A} {B = B} {C = C} (proj a b) i =
    hcomp (λ k → λ { (i = i0) → (sym (gluel (proj (snd C) (snd B))) ∙
                                                  gluer (snd A)) (~ k)
                    ; (i = i1) → proj (pivotl (snd B) b k) a})
          (gluer a (~ i))
  rearrange-gluel {A = A} {B = B} {C = C} (gluel a i) j =
    hcomp (λ k → λ { (i = i1) → ((λ i₁ → gluel (proj (snd C) (snd B)) (~ i₁)) ∙
                                  gluer (snd A)) (~ k ∨ j)
                    ; (j = i0) → ((λ i₁ → gluel (proj (snd C) (snd B)) (~ i₁)) ∙
                                  gluer (snd A)) (~ k)
                    ; (j = i1) → top-filler i k})
          (gluer a (i ∨ ~ j))
    where
      top-filler : I → I → Smash (SmashPtProj C B) A
      top-filler i j =
        hcomp (λ k → λ { (i = i0) → side-filler k j
                        ; (i = i1) → gluer a (j ∨ k)
                        ; (j = i0) → gluer a (i ∧ k)})
              (gluer a (i ∧ j))
       where
       side-filler : I → I → Smash (SmashPtProj C B) A
       side-filler i j =
         hcomp (λ k → λ { (i = i0) → proj (proj (snd C) (snd B)) a
                        ; (i = i1) → proj ((rCancel (gluel (snd C)) ∙ sym (rCancel (gluer (snd B)))) k j) a
                        ; (j = i0) → proj (proj (snd C) (snd B)) a
                        ; (j = i1) → (proj ((gluel (snd C) ∙ sym (gluel (snd C))) i) a)})
                (proj ((gluel (snd C) ∙ sym (gluel (snd C))) (j ∧ i)) a)
  rearrange-gluel {A = A} {B = B} {C = C} (gluer b i) j =
    hcomp (λ k → λ {(i = i1) → ((sym (gluel (proj (snd C) (snd B)))) ∙ gluer (snd A)) (~ k)
                   ; (j = i0) → ((sym (gluel (proj (snd C) (snd B)))) ∙ gluer (snd A)) (~ k)
                   ; (j = i1) → top-filler1 i k})
          (gluer (snd A) (i ∨ (~ j)))
    where
    top-filler1 : I → I → Smash (SmashPtProj C B) A
    top-filler1 i j =
      hcomp (λ k → λ { (i = i0) → congFunct (λ x → proj x (snd A)) (gluer (snd B)) (sym (gluer b)) (~ k) j
                   ; (i = i1) → (sym (gluel (proj (snd C) (snd B))) ∙ gluer (snd A)) (~ j)
                   ; (j = i0) → gluer (snd A) i
                   ; (j = i1) → gluel (proj (snd C) b) i})
          (top-filler2 i j)
      where
      top-filler2 : I → I → Smash (SmashPtProj C B) A
      top-filler2 i j =
        hcomp (λ k → λ { (j = i0) → gluer (snd A) (i ∧ k)
                          ; (j = i1) → gluel (gluer b (~ k)) i})
                (hcomp (λ k → λ { (j = i0) → gluel (gluer (snd B) i0) (~ k ∧ (~ i))
                                 ; (j = i1) → gluel (baser) (~ k ∨ i)
                                 ; (i = i0) → gluel (gluer (snd B) j) (~ k)
                                 ; (i = i1) → gluel (proj (snd C) (snd B)) j })
                       (gluel (proj (snd C) (snd B)) (j ∨ (~ i))))

  rearrange : Smash (SmashPtProj A B) C → Smash (SmashPtProj C B) A
  rearrange basel = basel
  rearrange baser = baser
  rearrange (proj x y) = rearrange-proj y x
  rearrange (gluel a i) = rearrange-gluel a (~ i)
  rearrange {A = A} {B = B} {C = C} (gluer b i) = ((λ j → proj (pivotr b (snd C) j) (snd A)) ∙
                                                  gluer (snd A)) i

  ⋀∙→SmashPtProj : (A ⋀∙ B) →∙ SmashPtProj A B
  ⋀∙→SmashPtProj {A = A} {B = B} = fun , refl
    where
    fun : (A ⋀ B) → Smash A B
    fun (inl x) = proj (snd A) (snd B)
    fun (inr (x , x₁)) = proj x x₁
    fun (push (inl x) i) = pivotr (snd A) x i
    fun (push (inr x) i) = pivotl (snd B) x i
    fun (push (push a j) i) = pivotlrId (~ j) i

  SmashPtProj→⋀∙ : (SmashPtProj A B) →∙ (A ⋀∙ B)
  SmashPtProj→⋀∙ {A = A} {B = B} = Smash→⋀ , sym (push (inr (snd B)))

SmashAssociate : Smash (SmashPtProj A B) C → Smash A (SmashPtProj B C)
SmashAssociate = comm ∘ Smash-map  (comm , refl) (idfun∙ _) ∘ rearrange

SmashAssociate⁻ : Smash A (SmashPtProj B C) → Smash (SmashPtProj A B) C
SmashAssociate⁻ = rearrange ∘ comm ∘ Smash-map (idfun∙ _) (comm , refl)

⋀-associate : (A ⋀∙ B) ⋀ C → A ⋀ (B ⋀∙ C)
⋀-associate = (idfun∙ _ ⋀→ SmashPtProj→⋀∙) ∘ Smash→⋀ ∘ SmashAssociate ∘ ⋀→Smash ∘ (⋀∙→SmashPtProj ⋀→ idfun∙ _)

⋀-associate⁻ : A ⋀ (B ⋀∙ C) → (A ⋀∙ B) ⋀ C
⋀-associate⁻ = (SmashPtProj→⋀∙ ⋀→ idfun∙ _) ∘ Smash→⋀ ∘ SmashAssociate⁻ ∘ ⋀→Smash ∘ (idfun∙ _ ⋀→ ⋀∙→SmashPtProj)


text:
module Issue616 where

open import Common.Coinduction

const : ∀ {a b}{A : Set a}{B : Set b} → A → B → A
const x _ = x

-- The recursive call should be ignored by the termination checker,
-- since ♭ is a projection function and shouldn't store its implicit
-- arguments.
contrived : Set₁
contrived = ♭ {A = const _ contrived} (♯ Set)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Categories.Category
open import Categories.Category.Cocomplete.Finitely

module Categories.Category.Cocomplete.Finitely.Properties {o ℓ e} {C : Category o ℓ e} (finite : FinitelyCocomplete C) where

open import Categories.Category.Duality C
private
  module C = Category C
  open C

open import Categories.Category.Finite.Fin
open import Categories.Category.Complete.Finitely C.op
open import Categories.Category.Complete.Finitely.Properties (FinitelyCocomplete⇒coFinitelyComplete finite)

open import Categories.Diagram.Colimit
open import Categories.Diagram.Limit
open import Categories.Diagram.Duality C
open import Categories.Functor

finiteColimit : (shape : FinCatShape) (F : Functor (FinCategory shape) C) → Colimit F
finiteColimit shape F = coLimit⇒Colimit (finiteLimit shape.op F.op)
  where module shape = FinCatShape shape
        module F = Functor F

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
------------------------------------------------------------------------
-- Some algebraic structures (not packed up with sets, operations,
-- etc.)
------------------------------------------------------------------------

open import Relation.Binary

module Algebra.Structures where

import Algebra.FunctionProperties as FunctionProperties
open FunctionProperties using (Op₁; Op₂)
import Relation.Binary.EqReasoning as EqR
open import Data.Function
open import Data.Product

------------------------------------------------------------------------
-- One binary operation

record IsSemigroup {A} (≈ : Rel A) (∙ : Op₂ A) : Set where
  open FunctionProperties ≈
  field
    isEquivalence : IsEquivalence ≈
    assoc         : Associative ∙
    ∙-pres-≈      : ∙ Preserves₂ ≈ ⟶ ≈ ⟶ ≈

  open IsEquivalence isEquivalence public

record IsMonoid {A} (≈ : Rel A) (∙ : Op₂ A) (ε : A) : Set where
  open FunctionProperties ≈
  field
    isSemigroup : IsSemigroup ≈ ∙
    identity    : Identity ε ∙

  open IsSemigroup isSemigroup public

record IsCommutativeMonoid
         {A} (≈ : Rel A) (∙ : Op₂ A) (ε : A) : Set where
  open FunctionProperties ≈
  field
    isMonoid : IsMonoid ≈ ∙ ε
    comm     : Commutative ∙

  open IsMonoid isMonoid public

record IsGroup
         {A} (≈ : Rel A) (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set where
  open FunctionProperties ≈
  infixl 7 _-_
  field
    isMonoid  : IsMonoid ≈ _∙_ ε
    inverse   : Inverse ε _⁻¹ _∙_
    ⁻¹-pres-≈ : _⁻¹ Preserves ≈ ⟶ ≈

  open IsMonoid isMonoid public

  _-_ : Op₂ A
  x - y = x ∙ (y ⁻¹)

record IsAbelianGroup
         {A} (≈ : Rel A) (∙ : Op₂ A) (ε : A) (⁻¹ : Op₁ A) : Set where
  open FunctionProperties ≈
  field
    isGroup : IsGroup ≈ ∙ ε ⁻¹
    comm    : Commutative ∙

  open IsGroup isGroup public

  isCommutativeMonoid : IsCommutativeMonoid ≈ ∙ ε
  isCommutativeMonoid = record
    { isMonoid = isMonoid
    ; comm     = comm
    }

------------------------------------------------------------------------
-- Two binary operations

record IsNearSemiring {A} (≈ : Rel A) (+ * : Op₂ A) (0# : A) : Set where
  open FunctionProperties ≈
  field
    +-isMonoid    : IsMonoid ≈ + 0#
    *-isSemigroup : IsSemigroup ≈ *
    distribʳ      : * DistributesOverʳ +
    zeroˡ         : LeftZero 0# *

  open IsMonoid +-isMonoid public
         renaming ( assoc       to +-assoc
                  ; ∙-pres-≈    to +-pres-≈
                  ; isSemigroup to +-isSemigroup
                  ; identity    to +-identity
                  )

  open IsSemigroup *-isSemigroup public
         using ()
         renaming ( assoc    to *-assoc
                  ; ∙-pres-≈ to *-pres-≈
                  )

record IsSemiringWithoutOne
         {A} (≈ : Rel A) (+ * : Op₂ A) (0# : A) : Set where
  open FunctionProperties ≈
  field
    +-isCommutativeMonoid : IsCommutativeMonoid ≈ + 0#
    *-isSemigroup         : IsSemigroup ≈ *
    distrib               : * DistributesOver +
    zero                  : Zero 0# *

  open IsCommutativeMonoid +-isCommutativeMonoid public
         renaming ( assoc       to +-assoc
                  ; ∙-pres-≈    to +-pres-≈
                  ; isSemigroup to +-isSemigroup
                  ; identity    to +-identity
                  ; isMonoid    to +-isMonoid
                  ; comm        to +-comm
                  )

  open IsSemigroup *-isSemigroup public
         using ()
         renaming ( assoc       to *-assoc
                  ; ∙-pres-≈    to *-pres-≈
                  )

  isNearSemiring : IsNearSemiring ≈ + * 0#
  isNearSemiring = record
    { +-isMonoid    = +-isMonoid
    ; *-isSemigroup = *-isSemigroup
    ; distribʳ      = proj₂ distrib
    ; zeroˡ         = proj₁ zero
    }

record IsSemiringWithoutAnnihilatingZero
         {A} (≈ : Rel A) (+ * : Op₂ A) (0# 1# : A) : Set where
  open FunctionProperties ≈
  field
    -- Note that these structures do have an additive unit, but this
    -- unit does not necessarily annihilate multiplication.
    +-isCommutativeMonoid : IsCommutativeMonoid ≈ + 0#
    *-isMonoid            : IsMonoid ≈ * 1#
    distrib               : * DistributesOver +

  open IsCommutativeMonoid +-isCommutativeMonoid public
         renaming ( assoc       to +-assoc
                  ; ∙-pres-≈    to +-pres-≈
                  ; isSemigroup to +-isSemigroup
                  ; identity    to +-identity
                  ; isMonoid    to +-isMonoid
                  ; comm        to +-comm
                  )

  open IsMonoid *-isMonoid public
         using ()
         renaming ( assoc       to *-assoc
                  ; ∙-pres-≈    to *-pres-≈
                  ; isSemigroup to *-isSemigroup
                  ; identity    to *-identity
                  )

record IsSemiring {A} (≈ : Rel A) (+ * : Op₂ A) (0# 1# : A) : Set where
  open FunctionProperties ≈
  field
    isSemiringWithoutAnnihilatingZero :
      IsSemiringWithoutAnnihilatingZero ≈ + * 0# 1#
    zero : Zero 0# *

  open IsSemiringWithoutAnnihilatingZero
         isSemiringWithoutAnnihilatingZero public

  isSemiringWithoutOne : IsSemiringWithoutOne ≈ + * 0#
  isSemiringWithoutOne = record
    { +-isCommutativeMonoid = +-isCommutativeMonoid
    ; *-isSemigroup         = *-isSemigroup
    ; distrib               = distrib
    ; zero                  = zero
    }

  open IsSemiringWithoutOne isSemiringWithoutOne public
         using (isNearSemiring)

record IsCommutativeSemiringWithoutOne
         {A} (≈ : Rel A) (+ * : Op₂ A) (0# : A) : Set where
  open FunctionProperties ≈
  field
    isSemiringWithoutOne : IsSemiringWithoutOne ≈ + * 0#
    *-comm               : Commutative *

  open IsSemiringWithoutOne isSemiringWithoutOne public

record IsCommutativeSemiring
         {A} (≈ : Rel A) (+ * : Op₂ A) (0# 1# : A) : Set where
  open FunctionProperties ≈
  field
    isSemiring : IsSemiring ≈ + * 0# 1#
    *-comm     : Commutative *

  open IsSemiring isSemiring public

  *-isCommutativeMonoid : IsCommutativeMonoid ≈ * 1#
  *-isCommutativeMonoid = record
      { isMonoid = *-isMonoid
      ; comm     = *-comm
      }

  isCommutativeSemiringWithoutOne :
    IsCommutativeSemiringWithoutOne ≈ + * 0#
  isCommutativeSemiringWithoutOne = record
    { isSemiringWithoutOne = isSemiringWithoutOne
    ; *-comm               = *-comm
    }

record IsRing {A} (≈ : Rel A)
              (_+_ _*_ : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set where
  open FunctionProperties ≈
  field
    +-isAbelianGroup : IsAbelianGroup ≈ _+_ 0# -_
    *-isMonoid       : IsMonoid ≈ _*_ 1#
    distrib          : _*_ DistributesOver _+_

  open IsAbelianGroup +-isAbelianGroup public
         renaming ( assoc               to +-assoc
                  ; ∙-pres-≈            to +-pres-≈
                  ; isSemigroup         to +-isSemigroup
                  ; identity            to +-identity
                  ; isMonoid            to +-isMonoid
                  ; inverse             to -‿inverse
                  ; ⁻¹-pres-≈           to -‿pres-≈
                  ; isGroup             to +-isGroup
                  ; comm                to +-comm
                  ; isCommutativeMonoid to +-isCommutativeMonoid
                  )

  open IsMonoid *-isMonoid public
         using ()
         renaming ( assoc       to *-assoc
                  ; ∙-pres-≈    to *-pres-≈
                  ; isSemigroup to *-isSemigroup
                  ; identity    to *-identity
                  )

  zero : Zero 0# _*_
  zero = (zeroˡ , zeroʳ)
    where
    open EqR (record { isEquivalence = isEquivalence })

    zeroˡ : LeftZero 0# _*_
    zeroˡ x = begin
        0# * x                              ≈⟨ sym $ proj₂ +-identity _ ⟩
       (0# * x) +            0#             ≈⟨ refl ⟨ +-pres-≈ ⟩ sym (proj₂ -‿inverse _) ⟩
       (0# * x) + ((0# * x)  + - (0# * x))  ≈⟨ sym $ +-assoc _ _ _ ⟩
      ((0# * x) +  (0# * x)) + - (0# * x)   ≈⟨ sym (proj₂ distrib _ _ _) ⟨ +-pres-≈ ⟩ refl ⟩
             ((0# + 0#) * x) + - (0# * x)   ≈⟨ (proj₂ +-identity _ ⟨ *-pres-≈ ⟩ refl)
                                                 ⟨ +-pres-≈ ⟩
                                               refl ⟩
                    (0# * x) + - (0# * x)   ≈⟨ proj₂ -‿inverse _ ⟩
                             0#             ∎

    zeroʳ : RightZero 0# _*_
    zeroʳ x = begin
      x * 0#                              ≈⟨ sym $ proj₂ +-identity _ ⟩
      (x * 0#) + 0#                       ≈⟨ refl ⟨ +-pres-≈ ⟩ sym (proj₂ -‿inverse _) ⟩
      (x * 0#) + ((x * 0#) + - (x * 0#))  ≈⟨ sym $ +-assoc _ _ _ ⟩
      ((x * 0#) + (x * 0#)) + - (x * 0#)  ≈⟨ sym (proj₁ distrib _ _ _) ⟨ +-pres-≈ ⟩ refl ⟩
      (x * (0# + 0#)) + - (x * 0#)        ≈⟨ (refl ⟨ *-pres-≈ ⟩ proj₂ +-identity _)
                                               ⟨ +-pres-≈ ⟩
                                             refl ⟩
      (x * 0#) + - (x * 0#)               ≈⟨ proj₂ -‿inverse _ ⟩
      0#                                  ∎

  isSemiringWithoutAnnihilatingZero
    : IsSemiringWithoutAnnihilatingZero ≈ _+_ _*_ 0# 1#
  isSemiringWithoutAnnihilatingZero = record
    { +-isCommutativeMonoid = +-isCommutativeMonoid
    ; *-isMonoid            = *-isMonoid
    ; distrib               = distrib
    }

  isSemiring : IsSemiring ≈ _+_ _*_ 0# 1#
  isSemiring = record
    { isSemiringWithoutAnnihilatingZero =
        isSemiringWithoutAnnihilatingZero
    ; zero = zero
    }

  open IsSemiring isSemiring public
         using (isNearSemiring; isSemiringWithoutOne)

record IsCommutativeRing {A}
         (≈ : Rel A) (+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) : Set where
  open FunctionProperties ≈
  field
    isRing : IsRing ≈ + * - 0# 1#
    *-comm : Commutative *

  open IsRing isRing public

  isCommutativeSemiring : IsCommutativeSemiring ≈ + * 0# 1#
  isCommutativeSemiring = record
    { isSemiring = isSemiring
    ; *-comm     = *-comm
    }

  open IsCommutativeSemiring isCommutativeSemiring public
         using (isCommutativeSemiringWithoutOne)

record IsLattice {A} (≈ : Rel A) (∨ ∧ : Op₂ A) : Set where
  open FunctionProperties ≈
  field
    isEquivalence : IsEquivalence ≈
    ∨-comm        : Commutative ∨
    ∨-assoc       : Associative ∨
    ∨-pres-≈      : ∨ Preserves₂ ≈ ⟶ ≈ ⟶ ≈
    ∧-comm        : Commutative ∧
    ∧-assoc       : Associative ∧
    ∧-pres-≈      : ∧ Preserves₂ ≈ ⟶ ≈ ⟶ ≈
    absorptive    : Absorptive ∨ ∧

  open IsEquivalence isEquivalence public

record IsDistributiveLattice {A} (≈ : Rel A) (∨ ∧ : Op₂ A) : Set where
  open FunctionProperties ≈
  field
    isLattice    : IsLattice ≈ ∨ ∧
    ∨-∧-distribʳ : ∨ DistributesOverʳ ∧

  open IsLattice isLattice public

record IsBooleanAlgebra
         {A} (≈ : Rel A) (∨ ∧ : Op₂ A) (¬ : Op₁ A) (⊤ ⊥ : A) : Set where
  open FunctionProperties ≈
  field
    isDistributiveLattice : IsDistributiveLattice ≈ ∨ ∧
    ∨-complementʳ         : RightInverse ⊤ ¬ ∨
    ∧-complementʳ         : RightInverse ⊥ ¬ ∧
    ¬-pres-≈              : ¬ Preserves ≈ ⟶ ≈

  open IsDistributiveLattice isDistributiveLattice public

max_issues_repo_name: larrytheliquid/Lemmachine


text:
-- Andreas, 2018-05-28, issue #3095, cannot make hidden shadowing variable visible
-- Andreas, 2019-07-15, issue #3919, make hidden variable visible in par. module

open import Agda.Builtin.Equality

module _ (A : Set) where

data Nat : Set where
  suc : {n : Nat} → Nat

data IsSuc : Nat → Set where
  isSuc : ∀{n} → IsSuc (suc {n})

test₁ : ∀{n} → IsSuc n → Set
test₁ p = aux p
  where
  aux : ∀{n} → IsSuc n → Set
  aux isSuc = {!n!}  -- C-c C-c
  -- Expected: aux (isSuc {n}) = {!!}

-- Context:
-- p  : IsSuc n
-- n : Nat  (not in scope)
-- n₁ : Nat  (not in scope)

-- WAS: ERROR
-- Ambiguous variable n
-- when checking that the expression ? has type Set

test₂ : ∀{m} → IsSuc m → Set
test₂ p = aux p
  where
  aux : ∀{n} → IsSuc n → Set
  aux isSuc = {!m!} -- C-c C-c
  -- Expected: cannot make hidden module parameter m visible

test₃ : ∀ m → IsSuc m → Set
test₃ m p = aux p refl
  where
  aux : ∀{n} → IsSuc n → m ≡ n → Set
  aux isSuc refl = {!n!} -- C-c C-c
  -- Expected: aux (isSuc {n}) refl = ?

test₄ : Nat → Nat
test₄ x = bar x
  where
    bar : Nat → Nat
    bar y = {!x!} -- C-c C-c
    -- Expected: cannot split on module parameter x

test₅ : Nat → {n : Nat} → Nat → Nat
test₅ = λ x y → {!n!} -- C-c C-c
    -- Expected: cannot make hidden lambda-bound variable n visible

issue3919 : {n m : Nat} → n ≡ m
issue3919 = {!m!} -- C-c C-c
    -- Expected: issue3919 {m = m} = ?

max_stars_repo_name: strake/agda

max_issues_repo_name: strake/agda

max_forks_repo_name: strake/agda


text:
module PlfaInduction where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_ ; refl ; cong ; sym)
open Eq.≡-Reasoning using (begin_ ; _≡⟨⟩_ ; _≡⟨_⟩_ ; _∎ )
open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; _*_ ; _^_ )

+-assoc : ∀ (a b c : ℕ) → (a + b) + c ≡ a + (b + c)
+-assoc zero b c =
  begin
    (zero + b) + c
  ≡⟨⟩
    b + c
  ≡⟨⟩
    zero + (b + c)
  ∎

+-assoc (suc a) b c =
  begin
    (suc a + b) + c
  ≡⟨⟩
    suc (a + b) + c
  ≡⟨⟩
    suc ((a + b) + c)
  ≡⟨ cong suc (+-assoc a b c) ⟩
    suc (a + (b + c))
  ≡⟨⟩
    suc a + (b + c)
  ∎

+-identityʳ : ∀ (a : ℕ) → a + zero ≡ a
+-identityʳ zero =
  begin
    zero + zero
  ≡⟨⟩
    zero
  ∎

+-identityʳ (suc a) =
  begin
    suc a + zero
  ≡⟨⟩
    suc (a + zero)
  ≡⟨ cong suc (+-identityʳ a) ⟩
    suc a
  ∎

+-suc : ∀ (a b : ℕ) → a + suc b ≡ suc (a + b)
+-suc zero b =
  begin
    zero + suc b
  ≡⟨⟩
    suc b
  ≡⟨⟩
   suc (zero + b)
  ∎

+-suc (suc a) b =
  begin
    suc a + suc b
  ≡⟨⟩
    suc (a + suc b)
  ≡⟨ cong suc (+-suc a b) ⟩
    suc (suc a + b)
  ∎

+-comm : ∀ (a b : ℕ) → a + b ≡ b + a
+-comm zero b =
  begin
    zero + b
  ≡⟨⟩
    b
  ≡⟨ sym (+-identityʳ b) ⟩
    b + zero
  ∎

+-comm (suc a) b =
  begin
    suc a + b
  ≡⟨⟩
    suc (a + b)
  ≡⟨ cong suc (+-comm a b) ⟩
    suc (b + a)
  ≡⟨ sym (+-suc b a) ⟩
    b + suc a
  ∎

+-rearrange : ∀ (a b c d : ℕ) → (a + b) + (c + d)  ≡ (a + (b + c)) + d
+-rearrange a b c d =
  begin
    -- Because addition associates to the left
    -- a + b + (c + d)
    -- is the same as
    (a + b) + (c + d)
  ≡⟨ +-assoc a b (c + d) ⟩
    a + (b + (c + d))
  -- Lesson: The + and the _ in in (a +_) MUST be next to each other (no spaces allowed)
  ≡⟨ cong (a +_) (sym (+-assoc b c d)) ⟩
    a + ((b + c) + d)
  ≡⟨ sym (+-assoc a (b + c) d) ⟩
    (a + (b + c)) + d
  ∎

-- Let's do it again, now using the rewrite magic
--+-assoc' : ∀ (a b c : ℕ) → a + b + c ≡ a + (b + c)
--+-assoc' zero b c = refl
--+-assoc' (suc a) b c rewrite +-assoc' a b c = refl

--+-suc' : ∀ (a b : ℕ) → a + suc b ≡ suc (a + b)
--+-suc' zero b = refl
--+-suc' (suc a) b rewrite +-suc' a b = refl

+-swap : ∀ (a b c : ℕ) → a + (b + c) ≡ b + (a + c)
+-swap a b c rewrite sym (+-assoc a b c) | +-comm a b | +-assoc b a c = refl

*-zero : ∀ (a : ℕ) → a * zero ≡ zero
*-zero zero = refl
*-zero (suc a) rewrite *-zero a = refl

*-rsucdist : ∀ (n m : ℕ) → n * suc m ≡ n + n * m
*-rsucdist zero m = refl
*-rsucdist (suc n) m rewrite *-rsucdist n m | +-swap m n (n * m) = refl

*-distrib : ∀ (x b c : ℕ) → (b + c) * x ≡ b * x + c * x
*-distrib zero b c rewrite *-zero (b + c) | *-zero b | *-zero c = refl
*-distrib (suc x) b c rewrite *-rsucdist (b + c) x
                            | *-distrib x b c
                            | +-rearrange b c (b * x) (c * x)
                            | +-comm c (b * x)
                            | sym (+-rearrange b (b * x) c (c * x) )
                            | sym (*-rsucdist b x)
                            | sym (*-rsucdist c x) = refl

*-assoc : ∀ (a b c : ℕ) → (a * b) * c ≡ a * (b * c)
*-assoc zero b c = refl
*-assoc (suc a) b c =
  begin
    (suc a * b) * c
  ≡⟨⟩
    (b + a * b) * c
  ≡⟨ *-distrib c b (a * b) ⟩
    b * c + (a * b) * c
  ≡⟨ cong (λ { x → b * c + x }) (*-assoc a b c) ⟩
    suc a * (b * c)
  ∎

*-comm : ∀ (a b : ℕ) → a * b ≡ b * a
*-comm zero b rewrite *-zero b = refl
*-comm (suc a) b rewrite *-comm a b | sym (*-rsucdist b a) = refl

infixl 6 _∸_
_∸_ : ℕ → ℕ → ℕ
m ∸ zero = m
zero ∸ (suc n) = zero
(suc m) ∸ (suc n) = m ∸ n

∸-zero : ∀ (a : ℕ) → zero ∸ a ≡ zero
∸-zero zero = refl
∸-zero (suc a) = refl

∸-suc : ∀ (a b : ℕ) → a ∸ suc b ≡ a ∸ 1 ∸ b
∸-suc zero b rewrite ∸-zero b = refl
∸-suc (suc a) b = refl

-- ∸-+-assoc : ∀ (a b c : ℕ) → a ∸ b ∸ c ≡ a ∸ (b + c)
-- ∸-+-assoc a zero c = refl
-- ∸-+-assoc a (suc b) c =
--   begin
--     a ∸ suc b ∸ c
--   ≡⟨ cong (λ x → x ∸ c) (∸-suc a b) ⟩
--     a ∸ 1 ∸ b ∸ c -- Remember this is equal to ((a ∸ 1) ∸ b) ∸ c
--   ≡⟨ ∸-+-assoc  ⟩
--   ≡⟨ ∸-suc a (b + c) ⟩
--     a ∸ (b + c)
--   ∎


text:
------------------------------------------------------------------------------
-- Theorems which require a non-empty domain
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOL.NonEmptyDomain.TheoremsATP where

open import FOL.Base

------------------------------------------------------------------------------
-- We postulate some formulae and propositional functions.
postulate
  A  : Set
  A¹ : D → Set

postulate ∀→∃ : (∀ {x} → A¹ x) → ∃ A¹
{-# ATP prove ∀→∃ #-}

-- Let A be a formula. If x is not free in A then ⊢ (∃x)A ↔ A
-- (Mendelson 1997, proposition 2.18 (b), p. 70).
postulate ∃-erase-add₁ : (∃[ _ ] A) ↔ A
{-# ATP prove ∃-erase-add₁ #-}

-- Quantification over a variable that does not occur can be erased or
-- added.
postulate ∀-erase-add : ((x : D) → A) ↔ A
{-# ATP prove ∀-erase-add #-}

postulate ∃-erase-add₂ : (∃[ x ] (A ∨ A¹ x)) ↔ A ∨ (∃[ x ] A¹ x)
{-# ATP prove ∃-erase-add₂ #-}

------------------------------------------------------------------------------
-- References
--
-- Mendelson, Elliott (1997). Introduction to Mathematical Logic. 4th
-- ed. Chapman & Hall.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Digits and digit expansions
------------------------------------------------------------------------

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

module Data.Digit where

open import Data.Nat using (ℕ; zero; suc; pred; _+_; _*_; _≤?_; _≤′_)
open import Data.Nat.Properties
open import Data.Nat.Solver
open import Data.Fin as Fin using (Fin; zero; suc; toℕ)
open import Data.Char using (Char)
open import Data.List.Base
open import Data.Product
open import Data.Vec as Vec using (Vec; _∷_; [])
open import Data.Nat.DivMod
open import Induction.Nat using (<′-rec; <′-Rec)
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Decidable
open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
open import Function

open +-*-Solver

------------------------------------------------------------------------
-- Digits

-- Digit b is the type of digits in base b.

Digit : ℕ → Set
Digit b = Fin b

-- Some specific digit kinds.

Decimal = Digit 10
Bit     = Digit 2

-- Some named digits.

0b : Bit
0b = zero

1b : Bit
1b = suc zero

------------------------------------------------------------------------
-- Showing digits

-- The characters used to show the first 16 digits.

digitChars : Vec Char 16
digitChars =
  '0' ∷ '1' ∷ '2' ∷ '3' ∷ '4' ∷ '5' ∷ '6' ∷ '7' ∷ '8' ∷ '9' ∷
  'a' ∷ 'b' ∷ 'c' ∷ 'd' ∷ 'e' ∷ 'f' ∷ []

-- showDigit shows digits in base ≤ 16.

showDigit : ∀ {base} {base≤16 : True (base ≤? 16)} →
            Digit base → Char
showDigit {base≤16 = base≤16} d =
  Vec.lookup digitChars (Fin.inject≤ d (toWitness base≤16))

------------------------------------------------------------------------
-- Digit expansions

Expansion : ℕ → Set
Expansion base = List (Fin base)

-- fromDigits takes a digit expansion of a natural number, starting
-- with the _least_ significant digit, and returns the corresponding
-- natural number.

fromDigits : ∀ {base} → Expansion base → ℕ
fromDigits        []       = 0
fromDigits {base} (d ∷ ds) = toℕ d + fromDigits ds * base

-- toDigits b n yields the digits of n, in base b, starting with the
-- _least_ significant digit.
--
-- Note that the list of digits is always non-empty.

toDigits : (base : ℕ) {base≥2 : True (2 ≤? base)} (n : ℕ) →
           ∃ λ (ds : Expansion base) → fromDigits ds ≡ n
toDigits zero       {base≥2 = ()} _
toDigits (suc zero) {base≥2 = ()} _
toDigits (suc (suc k)) n = <′-rec Pred helper n
  where
  base = suc (suc k)
  Pred = λ n → ∃ λ ds → fromDigits ds ≡ n

  cons : ∀ {m} (r : Fin base) → Pred m → Pred (toℕ r + m * base)
  cons r (ds , eq) = (r ∷ ds , P.cong (λ i → toℕ r + i * base) eq)

  open ≤-Reasoning

  lem : ∀ x k r → 2 + x ≤′ r + (1 + x) * (2 + k)
  lem x k r = ≤⇒≤′ $ begin
    2 + x
      ≤⟨ m≤m+n _ _ ⟩
    2 + x + (x + (1 + x) * k + r)
      ≡⟨ solve 3 (λ x r k → con 2 :+ x :+ (x :+ (con 1 :+ x) :* k :+ r)
                              :=
                            r :+ (con 1 :+ x) :* (con 2 :+ k))
                 refl x r k ⟩
    r + (1 + x) * (2 + k)
      ∎

  helper : ∀ n → <′-Rec Pred n → Pred n
  helper n                       rec with n divMod base
  helper .(toℕ r + 0     * base) rec | result zero    r refl = ([ r ] , refl)
  helper .(toℕ r + suc x * base) rec | result (suc x) r refl =
    cons r (rec (suc x) (lem (pred (suc x)) k (toℕ r)))


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A solver for proving that one list is a sublist of the other.
------------------------------------------------------------------------

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

open import Relation.Binary using (DecSetoid)

module Data.List.Relation.Binary.Sublist.DecSetoid.Solver {c ℓ} (S : DecSetoid c ℓ) where

open DecSetoid S

open import Data.List.Relation.Binary.Sublist.Heterogeneous.Solver _≈_ refl _≟_
  using (Item; module Item; TList; module TList; prove) public


text:
postulate
  F : Set₁ → Set₁

record R : Set₁ where
  field
    f : F Set

{-# COMPILE GHC F = \ _ -> () #-}

{-# FOREIGN GHC data D = C () #-}
{-# COMPILE GHC R = data D (C) #-}


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

module Data.PolyP.Types where

open import Function hiding (_⟨_⟩_)
open import Data.Sum
open import Data.Sigma
open import Level
open import Data.Unit
open import Data.Nat
open import Data.Empty
open import WellFounded
open import Literals.Number
open import Data.Fin.Indexed.Literals
open import Data.Fin.Indexed.Properties
open import Data.Fin.Indexed
open import Data.Nat.Literals
open import Data.Maybe

open import Data.PolyP.Universe
open import Data.PolyP.Composition
open import Data.PolyP.Currying
open import Data.PolyP.RecursionSchemes

LIST : ∀ {n} → Functor (suc n)
LIST = μ⟨ ① ⊕ ! (fs f0) ⊗ ! f0 ⟩

-- The free near-semiring
FOREST : Functor 1
FOREST = μ⟨ LIST ⊚ (① ⊕ ! (fs f0) ⊗ ! f0) ⟩

-- Lists of lists
LEVELS : Functor 1
LEVELS = μ⟨ ① ⊕ ! (fs f0) ⊗ ! f0 ⟩ ⊚ μ⟨ ① ⊕ ! (fs f0) ⊗ ! f0 ⟩

-- The free monad
FREE : Functor 1 → Functor 1
FREE f = μ⟨ ! (fs f0) ⊕ f0 ⇑ f ⟩

COFREE : Functor 1 → Functor 1
COFREE f = μ⟨ ! (fs f0) ⊗ f0 ⇑ f ⟩

ROSE : Functor 1
ROSE = μ⟨ ! (fs f0) ⊗ f0 ⇑ LIST ⟩

module _ {A B : Type} where
  FOLDR : (A → B → B) → B → ⟦ LIST ⟧ ~ A → B
  FOLDR f b = cata (const b ▿ uncurry f)

open import Data.List
open import Data.List.Properties
open import Function.Isomorphism
open import Path

pattern _∷′_ x xs  = ⟨ inr (x , xs) ⟩
pattern []′        = ⟨ inl tt ⟩

generic-list : List A ⇔ ⟦ LIST ⟧ ~ A
generic-list .fun       = foldr  _∷′_  []′
generic-list .inv       = FOLDR  _∷_   []
generic-list .leftInv   = list-elim  _      (λ      x     xs     p    i → x ∷   p i)          λ   i → []
generic-list .rightInv  = elim       _ λ {  (inr (  x ,   xs ,   p))  i → x ∷′  p i   ; (inl  _)  i → []′ }

open import Data.Vec

STREAM : Type → Type
STREAM A = ν (! (fs f0) ⊗ ! f0) ~ A

nats : ℕ → STREAM ℕ
nats n .unfold = n , nats (suc n)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------
-- Extension The Agda standard library
--
-- Properties of indexed binary relations
------------------------------------------------------------------------

module Relation.Binary.Indexed.Extra where

open import Data.Product
open import Data.Sum
open import Function
open import Level
-- import Relation.Binary.PropositionalEquality.Core as PropEq
-- open import Relation.Binary.Consequences as Consequences
open import Relation.Binary.Core as Core using (_≡_)
open import Relation.Binary.Indexed.Core
open import Relation.Binary.Indexed
import Relation.Binary as B

------------------------------------------------------------------------
-- Simple properties and equivalence relations

-- open Core public hiding (_≡_; refl; _≢_)
--
-- open Consequences public using (Total)

------------------------------------------------------------------------
-- Simple properties of indexed binary relations

-- Implication/containment. Could also be written ⊆.
[_][_]_⇒_ : ∀ {i₁ i₂ a b ℓ₁ ℓ₂} {I₁ : Set i₁} {I₂ : Set i₂}
    (A : I₁ → Set a) (B : I₂ → Set b)
    → REL A B ℓ₁ → REL A B ℓ₂ → Set _
[ A ][ B ] P ⇒ Q = ∀ {i₁ i₂} {x : A i₁} {y : B i₂} → P x y → Q x y

-- _Preserves_⟶_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : A → Set b} →
--           ((x : A) → B x) → B.Rel A ℓ₁ → Rel B ℓ₂ → Set (ℓ₂ ⊔ (ℓ₁ ⊔ a))
-- f Preserves P ⟶ Q = P =[ f ]⇒ Q

_Respects_ : ∀ {𝒾 a ℓ₁ ℓ₂} {I : Set 𝒾} {A : I → Set a} {i : I}
    → (A i → Set ℓ₁) → Rel A ℓ₂ → Set (ℓ₂ ⊔ (ℓ₁ ⊔ a))
P Respects _∼_ = ∀ {x y} → x ∼ y → P x → P y

[_]_Respects₂_ : ∀ {𝒾 a ℓ₁ ℓ₂} {I : Set 𝒾} (A : I → Set a)
    → Rel A ℓ₁ → Rel A ℓ₂ → Set (ℓ₂ ⊔ (ℓ₁ ⊔ (a ⊔ 𝒾)))
[ A ] P Respects₂ _∼_ =
      (∀ {i} {x : A i} → _Respects_ {A = A} {i = i} (P x) _∼_) ×
      (∀ {i} {y : A i} → _Respects_ {A = A} {i = i} (flip P y) _∼_)

------------------------------------------------------------------------
-- Preorders

record IsPreorder {𝒾 a ℓ₁ ℓ₂} {I : Set 𝒾} (A : I → Set a)
                  (_≈_ : Rel A ℓ₁) -- The underlying equality.
                  (_∼_ : Rel A ℓ₂) -- The relation.
                  : Set (𝒾 ⊔ a ⊔ ℓ₁ ⊔ ℓ₂) where
    field
        isEquivalence : IsEquivalence A _≈_
        -- Reflexivity is expressed in terms of an underlying equality:
        reflexive     : [ A ][ A ] _≈_ ⇒ _∼_
        trans         : Transitive A _∼_

    module Eq = IsEquivalence isEquivalence

    refl : Reflexive A _∼_
    refl = reflexive Eq.refl

    ∼-resp-≈ : [ A ] _∼_ Respects₂ _≈_
    ∼-resp-≈ = (λ x≈y z∼x → trans z∼x (reflexive x≈y))
           , (λ x≈y x∼z → trans (reflexive $ Eq.sym x≈y) x∼z)

record Preorder {i} (I : Set i) c ℓ₁ ℓ₂ : Set (suc (i ⊔ c ⊔ ℓ₁ ⊔ ℓ₂)) where
    infix 4 _≈_ _∼_
    field
        Carrier    : I → Set c
        _≈_        : Rel Carrier ℓ₁  -- The underlying equality.
        _∼_        : Rel Carrier ℓ₂  -- The relation.
        isPreorder : IsPreorder Carrier _≈_ _∼_

    open IsPreorder isPreorder public

SetoidIsPreorder : ∀ {𝒾} {I : Set 𝒾} {c ℓ} (S : Setoid I c ℓ) → IsPreorder (Setoid.Carrier S) (Setoid._≈_ S) (Setoid._≈_ S)
SetoidIsPreorder {𝒾} {I} S = record
    { isEquivalence = isEquivalence
    ; reflexive = id
    ; trans = IsEquivalence.trans isEquivalence
    }
    where
        open Setoid S

Setoid⇒Preorder : ∀ {𝒾} {I : Set 𝒾} {c ℓ} (S : Setoid I c ℓ) → Preorder I c ℓ ℓ
Setoid⇒Preorder S = record { isPreorder = SetoidIsPreorder S }
    -- record
    -- { Carrier = {!   !}
    -- ; _≈_ = {!   !}
    -- ; _∼_ = {!   !}
    -- ; isPreorder = {!   !}
    -- }

    -- IsEquivalence.reflexive (Setoid.isEquivalence S)
    -- where   open IsEquivalence {!   !}
    --
    -- isPreorder : IsPreorder _≡_ _≈_
    -- isPreorder = record
    --     { isEquivalence = PropEq.isEquivalence
    --     ; reflexive     = reflexive
    --     ; trans         = trans
    --     }
      --
      -- preorder : Preorder c c ℓ
      -- preorder = record { isPreorder = isPreorder }

max_stars_repo_name: banacorn/categories

max_issues_repo_name: banacorn/categories

max_forks_repo_name: banacorn/categories