text:
{-# OPTIONS --cubical --no-import-sorts --guardedness --safe #-}

module Cubical.Codata.M.AsLimit.helper where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv using (_≃_)
open import Cubical.Foundations.Function using (_∘_)

open import Cubical.Data.Unit
open import Cubical.Data.Prod
open import Cubical.Data.Nat as ℕ using (ℕ ; suc ; _+_ )
open import Cubical.Data.Sigma hiding (_×_)

open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Path

open import Cubical.Functions.Embedding
open import Cubical.Functions.FunExtEquiv

open Iso

-- General

iso→fun-Injection :
  ∀ {ℓ} {A B C : Type ℓ} (isom : Iso A B)
  → ∀ {f g : C -> A}
  → (x : C) → (Iso.fun isom (f x) ≡ Iso.fun isom (g x)) ≡ (f x ≡ g x)
iso→fun-Injection {A = A} {B} {C} isom {f = f} {g} =
  isEmbedding→Injection {A = A} {B} {C} (Iso.fun isom) (iso→isEmbedding {A = A} {B} isom) {f = f} {g = g}

abstract
  iso→Pi-fun-Injection :
    ∀ {ℓ} {A B C : Type ℓ} (isom : Iso A B)
    → ∀ {f g : C -> A}
    → Iso (∀ x → (fun isom) (f x) ≡ (fun isom) (g x)) (∀ x → f x ≡ g x)
  iso→Pi-fun-Injection {A = A} {B} {C} isom {f = f} {g} =
    pathToIso (cong (λ k → ∀ x → k x) (funExt (iso→fun-Injection isom {f = f} {g = g})))

iso→fun-Injection-Iso :
  ∀ {ℓ} {A B C : Type ℓ} (isom : Iso A B)
  → ∀ {f g : C -> A}
  → Iso (fun isom ∘ f ≡ fun isom ∘ g) (f ≡ g)
iso→fun-Injection-Iso {A = A} {B} {C} isom {f = f} {g} =
  (fun isom) ∘ f ≡ (fun isom) ∘ g
    Iso⟨ invIso funExtIso ⟩
  (∀ x → (fun isom) (f x) ≡ (fun isom) (g x))
     Iso⟨ iso→Pi-fun-Injection isom ⟩
  (∀ x → f x ≡ g x)
     Iso⟨ funExtIso ⟩
  f ≡ g ∎Iso

iso→fun-Injection-Path :
  ∀ {ℓ} {A B C : Type ℓ} (isom : Iso A B)
  → ∀ {f g : C -> A}
  → (fun isom ∘ f ≡ fun isom ∘ g) ≡ (f ≡ g)
iso→fun-Injection-Path {A = A} {B} {C} isom {f = f} {g} =
  isoToPath (iso→fun-Injection-Iso isom)

iso→inv-Injection-Path :
  ∀ {ℓ} {A B C : Type ℓ} (isom : Iso A B) →
  ∀ {f g : C -> B} →
  -----------------------
  ((inv isom) ∘ f ≡ (inv isom) ∘ g) ≡ (f ≡ g)
iso→inv-Injection-Path {A = A} {B} {C} isom {f = f} {g} = iso→fun-Injection-Path (invIso isom)

iso→fun-Injection-Iso-x :
    ∀ {ℓ} {A B : Type ℓ}
    → (isom : Iso A B)
    → ∀ {x y : A}
    → Iso ((fun isom) x ≡ (fun isom) y) (x ≡ y)
iso→fun-Injection-Iso-x isom {x} {y} =
    let tempx = λ {(lift tt) → x}
        tempy = λ {(lift tt) → y} in
    fun isom x ≡ fun isom y
      Iso⟨ iso (λ x₁ t → x₁)
               (λ x₁ → x₁ (lift tt))
               (λ x → refl)
               (λ x → refl) ⟩
    (∀ (t : Lift Unit) -> (((fun isom) ∘ tempx) t ≡ ((fun isom) ∘ tempy) t))
      Iso⟨ iso→Pi-fun-Injection isom ⟩
    (∀ (t : Lift Unit) -> tempx t ≡ tempy t)
      Iso⟨ iso (λ x₁ → x₁ (lift tt))
               (λ x₁ t → x₁)
               (λ x → refl)
               (λ x → refl) ⟩
    x ≡ y ∎Iso

iso→inv-Injection-Iso-x :
  ∀ {ℓ} {A B : Type ℓ}
  → (isom : Iso A B)
  → ∀ {x y : B}
  → Iso ((inv isom) x ≡ (inv isom) y) (x ≡ y)
iso→inv-Injection-Iso-x {A = A} {B = B} isom =
  iso→fun-Injection-Iso-x {A = B} {B = A} (invIso isom)

iso→fun-Injection-Path-x :
  ∀ {ℓ} {A B : Type ℓ}
  → (isom : Iso A B)
  → ∀ {x y : A}
  → ((fun isom) x ≡ (fun isom) y) ≡ (x ≡ y)
iso→fun-Injection-Path-x isom {x} {y} =
  isoToPath (iso→fun-Injection-Iso-x isom)

iso→inv-Injection-Path-x :
  ∀ {ℓ} {A B : Type ℓ}
  → (isom : Iso A B)
  → ∀ {x y : B}
  → ((inv isom) x ≡ (inv isom) y) ≡ (x ≡ y)
iso→inv-Injection-Path-x isom =
  isoToPath (iso→inv-Injection-Iso-x isom)

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:
-- Andreas, 2016-07-13, issue reported by Mietek Bak

-- {-# OPTIONS -v tc.size:20  #-}
-- {-# OPTIONS -v tc.meta.assign:30 #-}

open import Agda.Builtin.Size

data Cx (U : Set) : Set where
  ⌀   : Cx U
  _,_ : Cx U → U → Cx U

data _∈_ {U : Set} (A : U) : Cx U → Set where
  top : ∀ {Γ} → A ∈ (Γ , A)
  pop : ∀ {C Γ} → A ∈ Γ → A ∈ (Γ , C)

infixr 3 _⊃_
data Ty : Set where
  ι   : Ty
  _⊃_ : Ty → Ty → Ty

infix 1 _⊢⟨_⟩_
data _⊢⟨_⟩_ (Γ : Cx Ty) : Size → Ty → Set where
  var : ∀ {m A}                     → A ∈ Γ → Γ ⊢⟨ m ⟩ A
  lam : ∀ {m A B} {m′ : Size< m}    → Γ , A ⊢⟨ m′ ⟩ B → Γ ⊢⟨ m ⟩ A ⊃ B
  app : ∀ {m A B} {m′ m″ : Size< m} → Γ ⊢⟨ m′ ⟩ A ⊃ B → Γ ⊢⟨ m″ ⟩ A → Γ ⊢⟨ m ⟩ B

works : ∀ {m A B Γ} → Γ ⊢⟨ ↑ ↑ ↑ ↑ m ⟩ (A ⊃ A ⊃ B) ⊃ A ⊃ B
works = lam (lam (app (app (var (pop top)) (var top)) (var top)))

test : ∀ {m A B Γ} → Γ ⊢⟨ {!↑ ↑ ↑ ↑ m!} ⟩ (A ⊃ A ⊃ B) ⊃ A ⊃ B
test = lam (lam (app (app (var (pop top)) (var top)) (var top)))

-- This interaction meta should be solvable with
--   ↑ ↑ ↑ ↑ m
-- Give should succeed.
-- The problem was: premature instantiation to ∞.

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --type-in-type #-}
module Data where

open import Prelude

data Sigma (A : Set)(B : A -> Set) : Set
data Sigma A B where
  pair : (x : A) -> B x -> Sigma A B

fst : {A : _} {B : _} -> Sigma A B -> A
fst (pair x y) = x

snd : {A : _} {B : _} (p : Sigma A B) -> B (fst p)
snd (pair x y) = y

data Unit : Set
data Unit where
  tt : Unit

Cat : Set
Cat =
  Sigma Set                                                  (\ Obj ->
  Sigma (Obj -> Obj -> Set)                                  (\ Hom ->
  Sigma ((X : _) -> Hom X X)                                 (\ id ->
  Sigma ((X Y Z : _) -> Hom Y Z -> Hom X Y -> Hom X Z)       (\ comp ->
  Sigma ((X Y : _)(f : Hom X Y) -> comp _ _ _ (id Y) f == f) (\ idl ->
  Sigma ((X Y : _)(f : Hom X Y) -> comp _ _ _ f (id X) == f) (\ idr ->
  Sigma ((W X Y Z : _)
         (f : Hom W X)(g : Hom X Y)(h : Hom Y Z) ->
           comp _ _ _ (comp _ _ _ h g) f ==
           comp _ _ _ h (comp _ _ _ g f))                    (\ assoc ->
  Unit)))))))

Obj : (C : Cat) -> Set
Obj C = fst C

Hom : (C : Cat) -> Obj C -> Obj C -> Set
Hom C = fst (snd C)

id : (C : Cat) -> (X : _) -> Hom C X X
id C = fst (snd (snd C))

comp : (C : Cat) -> (X Y Z : _) -> Hom C Y Z -> Hom C X Y -> Hom C X Z
comp C = fst (snd (snd (snd C)))

idl : (C : Cat) -> (X Y : _)(f : Hom C X Y) ->
      comp C _ _ _ (id C Y) f == f
idl C = fst (snd (snd (snd (snd C))))

idr : (C : Cat) -> (X Y : _)(f : Hom C X Y) ->
      comp C _ _ _ f (id C X) == f
idr C = fst (snd (snd (snd (snd (snd C)))))

assoc : (C : Cat) ->
        (W X Y Z : _) (f : Hom C W X)(g : Hom C X Y)(h : Hom C Y Z) ->
        comp C _ _ _ (comp C _ _ _ h g) f ==
        comp C _ _ _ h (comp C _ _ _ g f)
assoc C = fst (snd (snd (snd (snd (snd (snd C))))))

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The lifting of a strict order to incorporate new extrema
------------------------------------------------------------------------

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

-- This module is designed to be used with
-- Relation.Nullary.Construct.Add.Extrema

open import Relation.Binary

module Relation.Binary.Construct.Add.Extrema.Strict
  {a ℓ} {A : Set a} (_<_ : Rel A ℓ) where

open import Level
open import Function
open import Relation.Nullary

import Relation.Nullary.Construct.Add.Infimum as I
open import Relation.Nullary.Construct.Add.Extrema
import Relation.Binary.Construct.Add.Infimum.Strict as AddInfimum
import Relation.Binary.Construct.Add.Supremum.Strict as AddSupremum
import Relation.Binary.Construct.Add.Extrema.Equality as Equality
import Relation.Binary.Construct.Add.Extrema.NonStrict as NonStrict

------------------------------------------------------------------------
-- Definition

private
  module Inf = AddInfimum _<_
  module Sup = AddSupremum Inf._<₋_

open Sup using () renaming (_<⁺_ to _<±_) public

------------------------------------------------------------------------
-- Useful pattern synonyms

pattern ⊥±<[_] l = Sup.[ Inf.⊥₋<[ l ] ]
pattern [_] p    = Sup.[ Inf.[ p ] ]
pattern ⊥±<⊤±    = Sup.[ I.⊥₋ ]<⊤⁺
pattern [_]<⊤± k = Sup.[ I.[ k ] ]<⊤⁺

------------------------------------------------------------------------
-- Relational properties

[<]-injective : ∀ {k l} → [ k ] <± [ l ] → k < l
[<]-injective = Inf.[<]-injective ∘′ Sup.[<]-injective

<±-asym : Asymmetric _<_ → Asymmetric _<±_
<±-asym = Sup.<⁺-asym ∘′ Inf.<₋-asym

<±-trans : Transitive _<_ → Transitive _<±_
<±-trans = Sup.<⁺-trans ∘′ Inf.<₋-trans

<±-dec : Decidable _<_ → Decidable _<±_
<±-dec = Sup.<⁺-dec ∘′ Inf.<₋-dec

<±-irrelevant : Irrelevant _<_ → Irrelevant _<±_
<±-irrelevant = Sup.<⁺-irrelevant ∘′ Inf.<₋-irrelevant

module _ {e} {_≈_ : Rel A e} where

  open Equality _≈_

  <±-cmp : Trichotomous _≈_ _<_ → Trichotomous _≈±_ _<±_
  <±-cmp = Sup.<⁺-cmp ∘′ Inf.<₋-cmp

  <±-irrefl : Irreflexive _≈_ _<_ → Irreflexive _≈±_ _<±_
  <±-irrefl = Sup.<⁺-irrefl ∘′ Inf.<₋-irrefl

  <±-respˡ-≈± : _<_ Respectsˡ _≈_ → _<±_ Respectsˡ _≈±_
  <±-respˡ-≈± = Sup.<⁺-respˡ-≈⁺ ∘′ Inf.<₋-respˡ-≈₋

  <±-respʳ-≈± : _<_ Respectsʳ _≈_ → _<±_ Respectsʳ _≈±_
  <±-respʳ-≈± = Sup.<⁺-respʳ-≈⁺ ∘′ Inf.<₋-respʳ-≈₋

  <±-resp-≈± : _<_ Respects₂ _≈_ → _<±_ Respects₂ _≈±_
  <±-resp-≈± = Sup.<⁺-resp-≈⁺ ∘′ Inf.<₋-resp-≈₋

module _ {r} {_≤_ : Rel A r} where

  open NonStrict _≤_

  <±-transʳ : Trans _≤_ _<_ _<_ → Trans _≤±_ _<±_ _<±_
  <±-transʳ = Sup.<⁺-transʳ ∘′ Inf.<₋-transʳ

  <±-transˡ : Trans _<_ _≤_ _<_ → Trans _<±_ _≤±_ _<±_
  <±-transˡ = Sup.<⁺-transˡ ∘′ Inf.<₋-transˡ

------------------------------------------------------------------------
-- Structures

module _ {e} {_≈_ : Rel A e} where

  open Equality _≈_

  <±-isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_ →
                            IsStrictPartialOrder _≈±_ _<±_
  <±-isStrictPartialOrder =
    Sup.<⁺-isStrictPartialOrder ∘′ Inf.<₋-isStrictPartialOrder

  <±-isDecStrictPartialOrder : IsDecStrictPartialOrder _≈_ _<_ →
                               IsDecStrictPartialOrder _≈±_ _<±_
  <±-isDecStrictPartialOrder =
    Sup.<⁺-isDecStrictPartialOrder ∘′ Inf.<₋-isDecStrictPartialOrder

  <±-isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_ →
                          IsStrictTotalOrder _≈±_ _<±_
  <±-isStrictTotalOrder =
    Sup.<⁺-isStrictTotalOrder ∘′ Inf.<₋-isStrictTotalOrder


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Convenient syntax for reasoning with a setoid
------------------------------------------------------------------------

-- Example use:

-- n*0≡0 : ∀ n → n * 0 ≡ 0
-- n*0≡0 zero    = refl
-- n*0≡0 (suc n) = begin
--   suc n * 0 ≈⟨ refl ⟩
--   n * 0 + 0 ≈⟨ ... ⟩
--   n * 0     ≈⟨ n*0≡0 n ⟩
--   0         ∎

-- Module `≡-Reasoning` in `Relation.Binary.PropositionalEquality`
-- is recommended for equational reasoning when the underlying equality is
-- `_≡_`.

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

open import Relation.Binary

module Relation.Binary.Reasoning.Setoid {s₁ s₂} (S : Setoid s₁ s₂) where

open Setoid S

------------------------------------------------------------------------
-- Reasoning combinators

open import Relation.Binary.Reasoning.PartialSetoid partialSetoid public
open import Relation.Binary.Reasoning.Base.Single _≈_ refl trans public
  using (_∎)


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

open import Base
open import Integers

module Spaces.FlatteningLoopSpaceWedgeCircles {i} (A : Set i) (set : is-set A)
  where

import Spaces.WedgeCircles
import Algebra.FreeGroup
import Algebra.FreeGroupProps
import Algebra.FreeGroupAsReducedWords

open Spaces.WedgeCircles A renaming (wedge-circles to WA; base to baseWA)
open Algebra.FreeGroup A renaming (freegroup to FA)
open Algebra.FreeGroupProps A

-- Path fibration

path-fib : WA → Set (suc i)
path-fib t = (t ≡ baseWA)

tot-path-fib : Set (suc i)
tot-path-fib = Σ (WA) path-fib

abstract
  tot-path-fib-is-contr : is-contr tot-path-fib
  tot-path-fib-is-contr = pathto-is-contr baseWA

-- Universal cover

x·-path : A → FA ≡ FA
x·-path x = eq-to-path (_ , x·-is-equiv x)

universal-cover : WA → Set i
universal-cover = wedge-circles-rec-nondep (Set _) FA x·-path

tot-cover : Set _
tot-cover = Σ WA universal-cover

trans-universal-cover : {u v : WA} (p : u ≡ v) (q : universal-cover u)
  → transport universal-cover p q
    ≡ transport (λ A → A) (ap universal-cover p) q
trans-universal-cover refl _ = refl

abstract
  loops-to-x· : (t : A) (u : FA) → transport universal-cover (loops t) u ≡ t · u
  loops-to-x· t u =
    trans-universal-cover (loops t) u
    ∘ (ap (λ t' → transport (λ B → B) t' u) (β-nondep (Set _) FA x·-path t)
    ∘ trans-id-eq-to-path (_ , x·-is-equiv t) u)

{-
Here is an HIT declaration for the Cayley graph of the free group over A:

data cayley : Set where
  z : FA → cayley
  e : (t : A) (u : FA) → z u ≡ z (t · u)

We will see that [cayley] is contractible.
We want to show that [tot-cover] has the same introduction and elimination
rules, so that we can prove that [tot-cover] is contractible too.
We do not need to actually have the type [cayley], it is enough to show
that [tot-cover] has the same rules and then we can copy the proof of the
contractibility using the new rules.
-}

-- Introduction rules
CA-z : FA → tot-cover
CA-z u = (baseWA , u)

CA-e : (t : A) (u : FA) → CA-z u ≡ CA-z (t · u)
CA-e t u = Σ-eq (loops t) (loops-to-x· t u)

-- Elimination rule
module equivCA
  {i}
  (P : tot-cover → Set i)
  (z : (u : FA) → P (CA-z u))
  (e : (t : A) (u : FA) → transport P (CA-e t u) (z u) ≡ z (t · u)) where

  CA-e' : (t : A) (u : FA)
    → CA-z u ≡ CA-z (transport universal-cover (loops t) u)
  CA-e' t u = Σ-eq (loops t) refl

  abstract
    e' : (t : A) (u : FA)
      → transport P (CA-e' t u) (z u)
        ≡ z (transport universal-cover (loops t) u)
    e' t u = (trans-totalpath universal-cover P {x = (baseWA , u)}
               {y = (baseWA , transport universal-cover (loops t) u)} (loops t)
               refl z
             ∘ move!-transp-left (λ z → P (baseWA , z)) _ (loops-to-x· t u)
                                 (z (t · u))
             (! (trans-totalpath universal-cover P
                  {x = (baseWA , u)} {y = (baseWA , (t · u))}
                  (loops t) (loops-to-x· t u) z)
              ∘ e t u))
              ∘ apd z (! (loops-to-x· t u))

  P-base : (u : universal-cover (baseWA)) → P (baseWA , u)
  P-base u = z u

  abstract
    P-loops : (t : A) (u : universal-cover (baseWA))
      → transport (λ x → (t : universal-cover x) → P (x , t)) (loops t) P-base u
        ≡ P-base u
    P-loops t u =
      transport (λ u → transport (λ x → (t : universal-cover x) → P (x , t))
                                 (loops t) P-base u ≡ P-base u)
        (trans-trans-opposite universal-cover (loops t) u)
        (! (trans-totalpath universal-cover P
             {x = (baseWA , transport universal-cover (! (loops t)) u)}
             {y = (baseWA , transport universal-cover (loops t)
               (transport universal-cover (! (loops t)) u))}
             (loops t) refl z)
        ∘ e' t (transport universal-cover (! (loops t)) u))

  P-CA-rec : (x : WA) → (t : universal-cover x) → P (x , t)
  P-CA-rec = wedge-circles-rec (λ x → (t : universal-cover x) → P (x , t))
                               P-base (λ t → funext (P-loops t))

  -- Here is the conclusion of the elimination rule
  abstract
    CA-rec : (t : tot-cover) → P t
    CA-rec (x , y) = P-CA-rec x y

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

--open import HoTT
open import homotopy.3x3.PushoutPushout
open import homotopy.3x3.Transpose
import homotopy.3x3.To as To
import homotopy.3x3.From as From
open import homotopy.3x3.Common

module homotopy.3x3.FromTo {i} (d : Span^2 {i}) where

open Span^2 d
open M d hiding (Pushout^2)
open M (transpose d) using () renaming (module F₁∙ to F∙₁; f₁∙ to f∙₁;
                                        module F₃∙ to F∙₃; f₃∙ to f∙₃;
                                        v-h-span to h-v-span)
open M using (Pushout^2)

open To d
open From d

open import homotopy.3x3.FromToInit d
open import homotopy.3x3.FromTo2 d
open import homotopy.3x3.FromTo3 d

from-to-g-g : (c : A₂₂) → (from-to-g-l (f₂₁ c) , ↓-='-out (apd (from-to-r ∘ f₃∙) (glue c)) , ↓-='-out (apd (ap from ∘ ap to ∘ glue) (glue c))
                        =□□ ↓-='-out (apd glue (glue c)) , ↓-='-out (apd (from-to-l ∘ f₁∙) (glue c)) , from-to-g-r (f₂₃ c))
from-to-g-g c = coh _ lemma1 lemma3 _ _ (↓-='-out (apd glue (glue c))) lemma2
                    where
                open M2 c
                open M3 c

from-to-g-g' : (c : A₂₂) → from-to-g-l (f₂₁ c) == from-to-g-r (f₂₃ c) [ (λ c → (from-to-l (f₁∙ c) , glue c =□ ap from (ap to (glue c)) , from-to-r (f₃∙ c))) ↓ glue c ]
from-to-g-g' c = ↓-=□-in (from-to-g-g c)

module FromToG = PushoutElim {d = span _ _ _ f₂₁ f₂₃} {P = λ c → (from-to-l (f₁∙ c) , glue c =□ ap from (ap to (glue c)) , from-to-r (f₃∙ c))}
                 from-to-g-l from-to-g-r from-to-g-g'

from-to-g : (c : A₂∙) → (from-to-l (f₁∙ c) , glue c =□ ap from (ap to (glue c)) , from-to-r (f₃∙ c))
from-to-g = FromToG.f

from-to-g' : (c : A₂∙) → from-to-l (f₁∙ c) == from-to-r (f₃∙ c) [ (λ z → from (to z) == z) ↓ glue c ]
from-to-g' c = ↓-∘=idf-in from to (from-to-g c)

from-to : (x : Pushout^2 d) → from (to x) == x
from-to = Pushout-elim from-to-l from-to-r from-to-g'

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda


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

module Cubical.Data.SumFin.Properties where

open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence

open import Cubical.Data.Empty as ⊥
import Cubical.Data.Fin as Fin
open import Cubical.Data.Nat
open import Cubical.Data.SumFin.Base as SumFin

private
  variable
    ℓ : Level
    k : ℕ

SumFin→Fin : Fin k → Fin.Fin k
SumFin→Fin = SumFin.elim (λ {k} _ → Fin.Fin k) Fin.fzero Fin.fsuc

Fin→SumFin : Fin.Fin k → Fin k
Fin→SumFin = Fin.elim (λ {k} _ → Fin k) fzero fsuc

Fin→SumFin-fsuc : (fk : Fin.Fin k) → Fin→SumFin (Fin.fsuc fk) ≡ fsuc (Fin→SumFin fk)
Fin→SumFin-fsuc = Fin.elim-fsuc (λ {k} _ → Fin k) fzero fsuc

SumFin→Fin→SumFin : (fk : Fin k) → Fin→SumFin (SumFin→Fin fk) ≡ fk
SumFin→Fin→SumFin = SumFin.elim (λ fk → Fin→SumFin (SumFin→Fin fk) ≡ fk)
                                refl λ {k} {fk} eq →
  Fin→SumFin (Fin.fsuc (SumFin→Fin fk)) ≡⟨ Fin→SumFin-fsuc (SumFin→Fin fk) ⟩
  fsuc (Fin→SumFin (SumFin→Fin fk))     ≡⟨ cong fsuc eq ⟩
  fsuc fk                               ∎

Fin→SumFin→Fin : (fk : Fin.Fin k) → SumFin→Fin (Fin→SumFin fk) ≡ fk
Fin→SumFin→Fin = Fin.elim (λ fk → SumFin→Fin (Fin→SumFin fk) ≡ fk)
                          refl λ {k} {fk} eq →
  SumFin→Fin (Fin→SumFin (Fin.fsuc fk)) ≡⟨ cong SumFin→Fin (Fin→SumFin-fsuc fk) ⟩
  Fin.fsuc (SumFin→Fin (Fin→SumFin fk)) ≡⟨ cong Fin.fsuc eq ⟩
  Fin.fsuc fk                           ∎

SumFin≃Fin : ∀ k → Fin k ≃ Fin.Fin k
SumFin≃Fin _ =
  isoToEquiv (iso SumFin→Fin Fin→SumFin Fin→SumFin→Fin SumFin→Fin→SumFin)

SumFin≡Fin : ∀ k → Fin k ≡ Fin.Fin k
SumFin≡Fin k = ua (SumFin≃Fin k)


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

module Cubical.Algebra.Group.EilenbergMacLane1 where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.GroupoidLaws renaming (assoc to ∙assoc)
open import Cubical.Foundations.Path
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.SIP
open import Cubical.Data.Unit
open import Cubical.Data.Sigma
open import Cubical.Relation.Binary.Base
open import Cubical.Structures.Axioms
open import Cubical.Structures.Auto
open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Properties
open import Cubical.Homotopy.Connected
open import Cubical.HITs.Nullification as Null hiding (rec; elim)
open import Cubical.HITs.Truncation.FromNegOne as Trunc renaming (rec to trRec; elim to trElim)
open import Cubical.HITs.EilenbergMacLane1

private
  variable ℓ : Level

module _ (G : Group {ℓ}) where

  open Group G

  emloop-id : emloop 0g ≡ refl
  emloop-id =
    -- emloop 0g ≡⟨ rUnit (emloop 0g) ⟩
    emloop 0g ≡⟨ rUnit (emloop 0g) ⟩
    emloop 0g ∙ refl ≡⟨ cong (emloop 0g ∙_) (rCancel (emloop 0g) ⁻¹) ⟩
    emloop 0g ∙ (emloop 0g ∙ (emloop 0g) ⁻¹) ≡⟨ ∙assoc _ _ _ ⟩
    (emloop 0g ∙ emloop 0g) ∙ (emloop 0g) ⁻¹ ≡⟨ cong (_∙ emloop 0g ⁻¹) ((emloop-comp G 0g 0g) ⁻¹) ⟩
    emloop (0g + 0g) ∙ (emloop 0g) ⁻¹ ≡⟨ cong (λ g → emloop {G = G} g ∙ (emloop 0g) ⁻¹)  (rid 0g) ⟩
    emloop 0g ∙ (emloop 0g) ⁻¹ ≡⟨ rCancel (emloop 0g) ⟩
    refl ∎

  emloop-inv : (g : Carrier) → emloop (- g) ≡ (emloop g) ⁻¹
  emloop-inv g =
    emloop (- g) ≡⟨ rUnit (emloop (- g)) ⟩
    emloop (- g) ∙ refl ≡⟨ cong (emloop (- g) ∙_) (rCancel (emloop g) ⁻¹) ⟩
    emloop (- g) ∙ (emloop g ∙ (emloop g) ⁻¹) ≡⟨ ∙assoc _ _ _ ⟩
    (emloop (- g) ∙ emloop g) ∙ (emloop g) ⁻¹ ≡⟨ cong (_∙ emloop g ⁻¹) ((emloop-comp G (- g) g) ⁻¹) ⟩
    emloop (- g + g) ∙ (emloop g) ⁻¹ ≡⟨ cong (λ h → emloop {G = G} h ∙ (emloop g) ⁻¹) (invl g) ⟩
    emloop 0g ∙ (emloop g) ⁻¹ ≡⟨ cong (_∙ (emloop g) ⁻¹) emloop-id ⟩
    refl ∙ (emloop g) ⁻¹ ≡⟨ (lUnit ((emloop g) ⁻¹)) ⁻¹ ⟩
    (emloop g) ⁻¹ ∎

  EM₁Groupoid : isGroupoid (EM₁ G)
  EM₁Groupoid = emsquash

  EM₁Connected : isConnected 2 (EM₁ G)
  EM₁Connected = ∣ embase ∣ , h
    where
      h : (y : hLevelTrunc 2 (EM₁ G)) → ∣ embase ∣ ≡ y
      h = trElim (λ y → isOfHLevelSuc 1 (isOfHLevelTrunc 2 ∣ embase ∣ y))
            (elimProp G (λ x → isOfHLevelTrunc 2 ∣ embase ∣ ∣ x ∣) refl)

  {- since we write composition in diagrammatic order,
     and function composition in the other order,
     we need right multiplication here -}
  rightEquiv : (g : Carrier) → Carrier ≃ Carrier
  rightEquiv g = isoToEquiv (iso (_+ g) (_+ - g)
    (λ h → (h + - g) + g ≡⟨ (assoc h (- g) g) ⁻¹ ⟩
             h + - g + g ≡⟨ cong (h +_) (invl g) ⟩
                  h + 0g ≡⟨ rid h ⟩ h ∎)
    λ h → (h + g) + - g ≡⟨ (assoc h g (- g)) ⁻¹ ⟩
            h + g + - g ≡⟨ cong (h +_) (invr g) ⟩
                 h + 0g ≡⟨ rid h ⟩ h ∎)

  compRightEquiv : (g h : Carrier)
    → compEquiv (rightEquiv g) (rightEquiv h) ≡ rightEquiv (g + h)
  compRightEquiv g h = equivEq _ _ (funExt (λ x → (assoc x g h) ⁻¹))

  CodesSet : EM₁ G → hSet ℓ
  CodesSet = rec G (isOfHLevelTypeOfHLevel 2) (Carrier , is-set) RE REComp
    where
      RE : (g : Carrier) → Path (hSet ℓ) (Carrier , is-set) (Carrier , is-set)
      RE g = Σ≡Prop (λ X → isPropIsOfHLevel {A = X} 2) (ua (rightEquiv g))

      lemma₁ : (g h : Carrier) → Square
        (ua (rightEquiv g)) (ua (rightEquiv (g + h)))
        refl (ua (rightEquiv h))
      lemma₁ g h = invEq
                   (Square≃doubleComp (ua (rightEquiv g)) (ua (rightEquiv (g + h)))
                     refl (ua (rightEquiv h)))
                   (ua (rightEquiv g) ∙ ua (rightEquiv h)
                       ≡⟨ (uaCompEquiv (rightEquiv g) (rightEquiv h)) ⁻¹ ⟩
                    ua (compEquiv (rightEquiv g) (rightEquiv h))
                       ≡⟨ cong ua (compRightEquiv g h) ⟩
                    ua (rightEquiv (g + h)) ∎)

      lemma₂ : {A₀₀ A₀₁ : hSet ℓ} (p₀₋ : A₀₀ ≡ A₀₁)
               {A₁₀ A₁₁ : hSet ℓ} (p₁₋ : A₁₀ ≡ A₁₁)
               (p₋₀ : A₀₀ ≡ A₁₀) (p₋₁ : A₀₁ ≡ A₁₁)
                 (s : Square (cong fst p₀₋) (cong fst p₁₋) (cong fst p₋₀) (cong fst p₋₁))
               → Square p₀₋ p₁₋ p₋₀ p₋₁
      fst (lemma₂ p₀₋ p₁₋ p₋₀ p₋₁ s i j) = s i j
      snd (lemma₂ p₀₋ p₁₋ p₋₀ p₋₁ s i j) =
        isSet→isSetDep (λ X → isProp→isSet (isPropIsOfHLevel {A = X} 2))
          (cong fst p₀₋) (cong fst p₁₋) (cong fst p₋₀) (cong fst p₋₁) s
          (cong snd p₀₋) (cong snd p₁₋) (cong snd p₋₀) (cong snd p₋₁) i j

      REComp : (g h : Carrier) → Square (RE g) (RE (g + h)) refl (RE h)
      REComp g h = lemma₂ (RE g) (RE (g + h)) refl (RE h) (lemma₁ g h)

  Codes : EM₁ G → Type ℓ
  Codes x = CodesSet x .fst

  encode : (x : EM₁ G) → embase ≡ x → Codes x
  encode x p = subst Codes p 0g

  decode : (x : EM₁ G) → Codes x → embase ≡ x
  decode = elimSet G (λ x → isOfHLevelΠ 2 (λ c → EM₁Groupoid (embase) x))
    emloop lem₂
    where
      module _ (g : Carrier) where
        lem₁ : (h : Carrier) → PathP (λ i → embase ≡ emloop g i) (emloop h) (emloop (h + g))
        lem₁ h = emcomp h g
        lem₂ : PathP (λ i → Codes (emloop g i) → embase ≡ emloop g i) emloop emloop
        lem₂ = ua→ {A₀ = Carrier} {A₁ = Carrier} {e = rightEquiv g} lem₁

  decode-encode : (x : EM₁ G) (p : embase ≡ x) → decode x (encode x p) ≡ p
  decode-encode x p = J (λ y q → decode y (encode y q) ≡ q)
    (emloop (transport refl 0g) ≡⟨ cong emloop (transportRefl 0g) ⟩
     emloop 0g ≡⟨ emloop-id ⟩ refl ∎) p

  encode-decode : (x : EM₁ G) (c : Codes x) → encode x (decode x c) ≡ c
  encode-decode = elimProp G (λ x → isOfHLevelΠ 1 (λ c → CodesSet x .snd _ _))
    λ g → encode embase (decode embase g) ≡⟨ refl ⟩
          encode embase (emloop g) ≡⟨ refl ⟩
          transport (ua (rightEquiv g)) 0g ≡⟨ uaβ (rightEquiv g) 0g ⟩
          0g + g ≡⟨ lid g ⟩
          g ∎

  ΩEM₁Iso : Iso (Path (EM₁ G) embase embase) Carrier
  Iso.fun ΩEM₁Iso = encode embase
  Iso.inv ΩEM₁Iso = emloop
  Iso.rightInv ΩEM₁Iso = encode-decode embase
  Iso.leftInv ΩEM₁Iso = decode-encode embase

  ΩEM₁≡ : (Path (EM₁ G) embase embase) ≡ Carrier
  ΩEM₁≡ = isoToPath ΩEM₁Iso

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


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

open import library.Basics hiding (Type ; Σ)
open import library.types.Sigma
open import library.NType2

open import Sec2preliminaries
open import Sec3hedberg

module Sec4hasConstToSplit where

-- Auxiliary Lemma 4.2
transport-is-comp : {X Y : Type} → {x₁ x₂ : X}
  → (h k : X → Y) → (t : x₁ == x₂) → (p : h x₁ == k x₁)
  → (transport _ t p) == ! (ap h t) ∙ p ∙ ap k t
transport-is-comp h k idp p = ! (∙-unit-r _)

-- Auxiliary Lemma 4.3, part 1
wconstant-implies-path-wconstant : {X Y : Type} → (f : X → Y) → (const f)
  → (x₁ x₂ : X) → const (ap f {x = x₁} {y = x₂})
wconstant-implies-path-wconstant {X} f c x₁ x₂ p₁ p₂ = claim-cor where
  claim : {x₃ x₄ : X} → {p : x₃ == x₄} → (ap f p) == ! (c x₃ x₃) ∙ (c x₃ x₄)
  claim {x₃} {p = idp} = ! (!-inv-l (c x₃ x₃))
  claim-cor : ap f p₁ == ap f p₂
  claim-cor =
    ap f p₁                 =⟨ claim ⟩
    ! (c x₁ x₁) ∙ (c x₁ x₂) =⟨ ! claim ⟩
    ap f p₂                 ∎

-- Auxiliary Lemma 4.3, part 2
wconstant-refl : {X Y : Type} → (f : X → Y) → (const f)
  → (x : X) → (p : x == x) → ap f p == idp
wconstant-refl f c x p = wconstant-implies-path-wconstant f c x x p idp

-- We also need the following very simple lemma:
ap-id-trivial : {X : Type} → {x₁ x₂ : X} → (p : x₁ == x₂) → ap (idf X) p == p
ap-id-trivial idp = idp

-- Lemma 4.1 needs a bit of preparation.
fix : {X : Type} → (f : X → X) → Type
fix {X} f = Σ X λ x → x == f x

-- let us give a name to the map X → fix f:
to-fix : {X : Type} → (f : X → X) → (const f) → X → fix f
to-fix f c x₀ = f x₀ , c _ _

-- the other direction is just projection:
from-fix : {X : Type} → (f : X → X) → fix f → X
from-fix f (x₀ , p₀) = x₀

-- let us structure the proof of the fixed point lemma a bit:
module fixedpoint {X : Type} (f : X → X) (c : const f) where

  -- let us show that (x , p) == (x , q) first
  module _ (x : X) (p q : x == f x) where
    t : x == x
    t = p ∙ ! q

    r : f x == f x
    r = ap f t

    r-is-triv : r == idp
    r-is-triv = wconstant-refl f c x t

    t' : x == x
    t' = ap (idf X) t

    t'-is-t : t' == t
    t'-is-t = ap-id-trivial t

    trans-t-p-is-q : transport (λ y → y == f y) t p == q
    trans-t-p-is-q =
      transport (λ y → y == f y) t p   =⟨  transport-is-comp (idf X) f t p  ⟩
      ! t' ∙ p ∙ r                     =⟨ ap (λ s → ! s ∙ p ∙ r) t'-is-t ⟩
      ! t ∙ p ∙ r                      =⟨ ! (∙-assoc (! t) _ _) ⟩
      (! t ∙ p) ∙ r                    =⟨ ap (λ s → (! t ∙ p) ∙ s) r-is-triv ⟩
      (! t ∙ p) ∙ idp                  =⟨ ∙-unit-r _ ⟩
      ! t ∙ p                          =⟨ ap (λ s → s ∙ p) (!-∙ p (! q)) ⟩
      (! (! q) ∙ ! p) ∙ p              =⟨ ∙-assoc (! (! q)) _ _ ⟩
      ! (! q) ∙ ! p ∙ p                =⟨ ap (λ s → ! (! q) ∙ s) (!-inv-l p) ⟩
      ! (! q) ∙ idp                    =⟨ ∙-unit-r _ ⟩
      ! (! q)                          =⟨ !-! _ ⟩
      q                                ∎

    single-x-claim : (x , p) == (x , q)
    single-x-claim = pair= t (from-transp _ _ trans-t-p-is-q)

  -- Now, we can prove that (x₁ , p₁) and (x₂ , p₂) are always equal:
  fix-paths : has-all-paths (fix f)
  fix-paths (x₁ , p₁) (x₂ , p₂) =
    (x₁ , p₁) =⟨ pair= (p₁ ∙ c x₁ x₂ ∙ ! p₂) (from-transp _ (p₁ ∙ c x₁ x₂ ∙ ! p₂) idp) ⟩
    (x₂ , _)  =⟨ single-x-claim x₂ _ _ ⟩
    (x₂ , p₂) ∎

-- finally, the proof of the fixed point lemma
fixed-point : {X : Type} → (f : X → X) → (const f) → is-prop (fix f)
fixed-point {X} f c = all-paths-is-prop (fixedpoint.fix-paths f c)

-- Sattler's argument
fixed-point-alt : {X : Type} → (f : X → X) → (const f) → is-prop (fix f)
fixed-point-alt {X} f c = inhab-to-contr-is-prop inh→contr where
  inh→contr : fix f → is-contr (fix f)
  inh→contr (x₀ , p₀) = equiv-preserves-level {A = Σ X λ x → x == f x₀} {B = fix f} claim-Σ (pathto-is-contr _) where
    claim : (x : X) → (x == f x₀) ≃ (x == f x)
    claim x = (λ p → p ∙ c x₀ x) , post∙-is-equiv _
    claim-Σ : (Σ X λ x → x == f x₀) ≃ fix f
    claim-Σ = equiv-Σ-snd claim

-- Corollary 4.4
-- let us define the following map:
trunc-to-fix : {X : Type} → (fc : hasConst X) → Trunc X → fix (fst fc)
trunc-to-fix (f , c) z = rec (fixed-point f c) (to-fix f c) z

hasConst→splitSup : {X : Type} → hasConst X → splitSup X
hasConst→splitSup (f , c) = (from-fix f) ∘ trunc-to-fix (f , c)

-- Theorem 4.5
hasConst↔splitSup : {X : Type} → hasConst X ↔ splitSup X
hasConst↔splitSup {X} = hasConst→splitSup , splitSup→hasConst where
  splitSup→hasConst : splitSup X → hasConst X
  splitSup→hasConst hst = f , c where
    f = hst ∘ ∣_∣
    c : const f
    c x₁ x₂ =
      f x₁      =⟨ idp ⟩
      hst ∣ x₁ ∣ =⟨ ap hst (prop-has-all-paths (h-tr _) _ _) ⟩
      hst ∣ x₂ ∣ =⟨ idp ⟩
      f x₂      ∎

-- preparation for Theorem 4.6 - we need to prove that
-- f : X → X with an inhabitant of Trunc (wconst f) is enough
-- to show that fix f is propositional.
fixed-point-strong : {X : Type} → (f : X → X) → (Trunc (const f)) → is-prop (fix f)
fixed-point-strong {X} f = rec {X = const f} {P = is-prop(fix f)} is-prop-is-prop (fixed-point f)

-- Theorem 4.6 (we exclude the part which is already included in 4.5)
-- to get an easy proof of the addendum, we structure it in the following way:
module thm46 {X : Type} where
  module _ (fhc : Σ (X → X) (Trunc ∘ const))  where
    f = fst fhc
    hc = snd fhc
    trunc-wconst-fix : Trunc X → Trunc(const f) → fix f
    trunc-wconst-fix z = rec {X = const f} {P = fix f} (fixed-point-strong f hc) (λ c → trunc-to-fix (f , c) z)
    trunc-fix : Trunc X → fix f
    trunc-fix z = trunc-wconst-fix z hc
    g : X → X
    g = fst ∘ trunc-fix ∘ ∣_∣
    g-wconst : const g
    g-wconst x₁ x₂ = ap (fst ∘ trunc-fix) (prop-has-all-paths (h-tr _) _ _)

hasConst↔hideProof : {X : Type} → hasConst X ↔ Σ (X → X) (Trunc ∘ const)
hasConst↔hideProof {X} = one , two where
  one : hasConst X → Σ (X → X) (Trunc ∘ const)
  one (f , c) = f , ∣ c ∣
  two : (Σ (X → X) (Trunc ∘ const)) → hasConst X
  two fhc = thm46.g fhc , thm46.g-wconst fhc

-- Theorem 4.6 addendum
merely-equal : {X : Type} → (fhc : Σ (X → X) (Trunc ∘ const)) → Trunc ((x : X) → fst fhc x == thm46.g fhc x)
merely-equal {X} (f , hc) = rec (h-tr _) (∣_∣ ∘ wconst-equal) hc where
  open thm46 hiding (f ; hc)
  wconst-equal : const f → (x : X) → f x == thm46.g (f , hc) x
  wconst-equal c x =
    f x                                     =⟨ idp ⟩
    fst (to-fix f c x)                      =⟨ ap fst (! (trunc-β _ _ x)) ⟩
    fst (trunc-to-fix (f , c) ∣ x ∣)          =⟨ ap fst (! (trunc-β _ _ c)) ⟩
    fst (trunc-wconst-fix (f , hc) ∣ x ∣ ∣ c ∣) =⟨ ap (λ hc' → fst (trunc-wconst-fix (f , hc) ∣ x ∣ hc')) (prop-has-all-paths (h-tr _) _ _) ⟩
    fst (trunc-wconst-fix (f , hc) ∣ x ∣ hc)   =⟨ idp ⟩
    fst (trunc-fix (f , hc) ∣ x ∣)            =⟨ idp ⟩
    g (f , hc) x                             ∎

max_stars_repo_name: nicolaikraus/HoTT-Agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.Monoid.Morphism where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Functions.Embedding

open import Cubical.Algebra
open import Cubical.Algebra.Semigroup.Morphism

private
  variable
    m n : Level

record IsMonoidHom (M : Monoid m) (N : Monoid n) (f : ⟨ M ⟩ → ⟨ N ⟩) : Type (ℓ-max m n) where
  constructor ismonoidhom
  field
    preservesOp : Homomorphic₂ f (Monoid._•_ M) (Monoid._•_ N)
    preservesId : Homomorphic₀ f (Monoid.ε M)   (Monoid.ε N)

record MonoidHom (M : Monoid m) (N : Monoid n) : Type (ℓ-max m n) where
  constructor monoidhom
  field
    fun : ⟨ M ⟩ → ⟨ N ⟩
    isHom : IsMonoidHom M N fun

  open IsMonoidHom isHom public

record MonoidEquiv (M : Monoid m) (N : Monoid n) : Type (ℓ-max m n) where
  constructor monoidequiv
  field
    eq : ⟨ M ⟩ ≃ ⟨ N ⟩
    isHom : IsMonoidHom M N (equivFun eq)

  open IsMonoidHom isHom public

  hom : MonoidHom M N
  hom = record { isHom = isHom }

instance
  MonoidHomOperators : HomOperators (Monoid m) (Monoid n) (ℓ-max m n)
  MonoidHomOperators = record { _⟶ᴴ_ = MonoidHom; _≃ᴴ_ = MonoidEquiv }

private
  variable
    M : Monoid m
    N : Monoid n

IsMonoidHom→IsSemigroupHom : {f : ⟨ M ⟩ → ⟨ N ⟩} → IsMonoidHom M N f → IsSemigroupHom (Monoid.semigroup M) (Monoid.semigroup N) f
IsMonoidHom→IsSemigroupHom = IsMonoidHom.preservesOp

MonoidHom→SemigroupHom : (M ⟶ᴴ N) → (Monoid.semigroup M ⟶ᴴ Monoid.semigroup N)
MonoidHom→SemigroupHom hom .SemigroupHom.fun = hom .MonoidHom.fun
MonoidHom→SemigroupHom hom .SemigroupHom.isHom = IsMonoidHom→IsSemigroupHom (hom .MonoidHom.isHom)

MonoidEquiv→SemigroupEquiv : M ≃ᴴ N → Monoid.semigroup M ≃ᴴ Monoid.semigroup N
MonoidEquiv→SemigroupEquiv eq .SemigroupEquiv.eq = eq .MonoidEquiv.eq
MonoidEquiv→SemigroupEquiv eq .SemigroupEquiv.isHom = IsMonoidHom→IsSemigroupHom (eq .MonoidEquiv.isHom)


text:
open import bool

module braun-tree{ℓ} (A : Set ℓ) (_<A_ : A → A → 𝔹) where

open import bool-thms
open import eq
open import list
open import nat
open import nat-thms
open import product
open import sum

-- the index n is the size of the tree (number of elements of type A)
data braun-tree : (n : ℕ) → Set ℓ where
  bt-empty : braun-tree 0
  bt-node : ∀ {n m : ℕ} →
            A → braun-tree n → braun-tree m →
            n ≡ m ∨ n ≡ suc m →
            braun-tree (suc (n + m))

{- we will keep smaller (_<A_) elements closer to the root of the Braun tree as we insert -}
bt-insert : ∀ {n : ℕ} → A → braun-tree n → braun-tree (suc n)

bt-insert a bt-empty = bt-node a bt-empty bt-empty (inj₁ refl)

bt-insert a (bt-node{n}{m} a' l r p)
  rewrite +comm n m with p | if a <A a' then (a , a') else (a' , a)
bt-insert a (bt-node{n}{m} a' l r _) | inj₁ p | (a1 , a2)
  rewrite p = (bt-node a1 (bt-insert a2 r) l (inj₂ refl))
bt-insert a (bt-node{n}{m} a' l r _) | inj₂ p | (a1 , a2) =
  (bt-node a1 (bt-insert a2 r) l (inj₁ (sym p)))

bt-replace-min : ∀{n : ℕ} → A → braun-tree (suc n) → braun-tree (suc n)
bt-replace-min a (bt-node _ bt-empty bt-empty u) = (bt-node a bt-empty bt-empty u)
bt-replace-min a (bt-node _ bt-empty (bt-node _ _ _ _) (inj₁ ()))
bt-replace-min a (bt-node _ bt-empty (bt-node _ _ _ _) (inj₂ ()))
bt-replace-min a (bt-node _ (bt-node _ _ _ _) bt-empty (inj₁ ()))
bt-replace-min a (bt-node a' (bt-node x l r u) bt-empty (inj₂ y)) with a <A x
bt-replace-min a (bt-node a' (bt-node x l r u) bt-empty (inj₂ y)) | tt = (bt-node a (bt-node x l r u) bt-empty (inj₂ y))
bt-replace-min a (bt-node a' (bt-node x l r u) bt-empty (inj₂ y)) | ff =
 (bt-node x (bt-replace-min a (bt-node x l r u)) bt-empty (inj₂ y))
bt-replace-min a (bt-node a' (bt-node x l r u) (bt-node x' l' r' u') v) with a <A x && a <A x'
bt-replace-min a (bt-node a' (bt-node x l r u) (bt-node x' l' r' u') v) | tt =
 (bt-node a (bt-node x l r u) (bt-node x' l' r' u') v)
bt-replace-min a (bt-node a' (bt-node x l r u) (bt-node x' l' r' u') v) | ff with x <A x'
bt-replace-min a (bt-node a' (bt-node x l r u) (bt-node x' l' r' u') v) | ff | tt =
 (bt-node x (bt-replace-min a (bt-node x l r u)) (bt-node x' l' r' u') v)
bt-replace-min a (bt-node a' (bt-node x l r u) (bt-node x' l' r' u') v) | ff | ff =
 (bt-node x' (bt-node x l r u) (bt-replace-min a (bt-node x' l' r' u')) v)

{- thanks to Matías Giovannini for the excellent post
     http://alaska-kamtchatka.blogspot.com/2010/02/braun-trees.html
   explaining how to do delete -}
bt-delete-min : ∀ {p : ℕ} → braun-tree (suc p) → braun-tree p
bt-delete-min (bt-node a bt-empty bt-empty u) = bt-empty
bt-delete-min (bt-node a bt-empty (bt-node _ _ _ _) (inj₁ ()))
bt-delete-min (bt-node a bt-empty (bt-node _ _ _ _) (inj₂ ()))
bt-delete-min (bt-node a (bt-node{n'}{m'} a' l' r' u') bt-empty u) rewrite +0 (n' + m') = bt-node a' l' r' u'
bt-delete-min (bt-node a
                (bt-node{n}{m} x l1 r1 u1)
                (bt-node{n'}{m'} x' l2 r2 u2) u)
  rewrite +suc(n + m)(n' + m') | +suc n (m + (n' + m'))
        | +comm(n + m)(n' + m') =
  if (x <A x') then
    (bt-node x (bt-node x' l2 r2 u2)
      (bt-delete-min (bt-node x l1 r1 u1)) (lem{n}{m}{n'}{m'} u))
  else
    (bt-node x' (bt-replace-min x (bt-node x' l2 r2 u2))
      (bt-delete-min (bt-node x l1 r1 u1)) (lem{n}{m}{n'}{m'} u))
  where lem : {n m n' m' : ℕ} → suc (n + m) ≡ suc (n' + m') ∨ suc (n + m) ≡ suc (suc (n' + m')) →
              suc (n' + m') ≡ n + m ∨ suc (n' + m') ≡ suc (n + m)
        lem{n}{m}{n'}{m'} (inj₁ x) = inj₂ (sym x)
        lem (inj₂ y) = inj₁ (sym (suc-inj y))

bt-remove-min : ∀ {p : ℕ} → braun-tree (suc p) → A × braun-tree p
bt-remove-min (bt-node a l r u) = a , bt-delete-min (bt-node a l r u)

----------------------------------------------------------------------
-- this version stores data at the leaves instead of at the nodes
----------------------------------------------------------------------
data braun-tree' : (n : ℕ) → Set ℓ where
  bt'-leaf : A → braun-tree' 1
  bt'-node : ∀ {n m : ℕ} →
            braun-tree' n → braun-tree' m →
            n =ℕ m ≡ tt ⊎ n =ℕ m + 1 ≡ tt →
            braun-tree' (n + m)

bt'-insert : ∀ {n : ℕ} → A → braun-tree' n → braun-tree' (suc n)
bt'-insert a (bt'-leaf a') = bt'-node (bt'-leaf a) (bt'-leaf a') (inj₁ refl)
bt'-insert a (bt'-node{n}{m} l r p) rewrite +comm n m with p
bt'-insert a (bt'-node{n}{m} l r p) | inj₁ p' rewrite =ℕ-to-≡{n} p' = (bt'-node (bt'-insert a r) l (inj₂ lem))
  where lem : suc m =ℕ m + 1 ≡ tt
        lem rewrite +comm m 1 = =ℕ-refl m
bt'-insert a (bt'-node{n}{m} l r p) | inj₂ p' = (bt'-node (bt'-insert a r) l (inj₁ (lem n m p')))
  where lem : ∀ n m → n =ℕ m + 1 ≡ tt → suc m =ℕ n ≡ tt
        lem n m p' rewrite =ℕ-to-≡{n} p' | +comm m 1 = =ℕ-refl m

𝕃-to-braun-tree' : A → (l : 𝕃 A) → braun-tree' (suc (length l))
𝕃-to-braun-tree' a [] = bt'-leaf a
𝕃-to-braun-tree' a (a' :: as) = bt'-insert a (𝕃-to-braun-tree' a' as)

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
open import Silica
open import HeapProperties
import Context

open TypeEnvContext

open import Data.Nat
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Empty
import Relation.Binary.PropositionalEquality as Eq

data Preservation : Expr → Set where
  pres : ∀ {e e' : Expr}
       → ∀ {T T' : Type}
       → ∀ {Δ Δ'' Δ''' : StaticEnv}
       → ∀ {Σ Σ' : RuntimeEnv }
       → Δ ⊢ e ⦂ T ⊣ Δ''
       → Σ & Δ ok
       -- TODO: hdref(e)
       → Σ , e ⟶ Σ' , e'
       → (Δ' : StaticEnv)
       → (Δ' ⊢ e' ⦂ T' ⊣ Δ''')
       → (Σ' & Δ' ok)  --
       → (Δ''' <* Δ'')
       -----------------
       → Preservation e

splitIdempotent : ∀ {Γ T₁ T₂ T₃}
                    → Γ ⊢ T₁ ⇛ T₂ / T₃
                    → Γ ⊢ T₂ ⇛ T₂ / T₃
splitIdempotent {Γ} {.(base Void)} {.(base Void)} {.(base Void)} voidSplit = voidSplit
splitIdempotent {Γ} {.(base Boolean)} {.(base Boolean)} {.(base Boolean)} booleanSplit = booleanSplit
splitIdempotent {Γ} {.(contractType _)} {.(contractType _)} {.(contractType _)} (unownedSplit namesEq1 namesEq2 permsEq permUnowned) =
  unownedSplit refl (Eq.trans (Eq.sym namesEq1) namesEq2) refl permUnowned
splitIdempotent {Γ} {.(contractType _)} {.(contractType _)} {.(contractType _)} (shared-shared-shared x) =
  shared-shared-shared x
splitIdempotent {Γ} {.(contractType (tc _ Owned))} {.(contractType (tc _ Shared))} {.(contractType (tc _ Shared))} (owned-shared x) =
  shared-shared-shared refl
splitIdempotent {Γ} {.(contractType (record { contractName = _ ; perm = S _ }))}
                    {.(contractType (record { contractName = _ ; perm = Shared }))}
                    {.(contractType (record { contractName = _ ; perm = Shared }))}
                    (states-shared x) =
                    shared-shared-shared refl

preservation : ∀ {e e' : Expr}
               → {Γ : ContractEnv.ctx}
               → ∀ {T : Type}
               → ∀ {Δ Δ'' : StaticEnv}
               → ∀ {Σ Σ' : RuntimeEnv}
               → Δ ⊢ e ⦂ T ⊣ Δ''
               → Σ & Δ ok
               → Σ , e ⟶ Σ' , e'
               -----------------------
               → Preservation e

-- Proof proceeds by induction on the dynamic semantics.

preservation ty@(locTy {Γ} {Δ₀} l voidSplit) consis st@(SElookup {l = l} {v = voidVal} _ lookupL) =
  let
    Δ = (Δ₀ ,ₗ l ⦂ base Void)
    Δ' = Δ
    e'TypingJudgment = voidTy {Γ} {Δ = Δ'}
  in
    pres ty consis st Δ' e'TypingJudgment consis <*-refl
preservation ty@(locTy {Γ} {Δ₀} l booleanSplit) consis st@(SElookup {l = l} {v = boolVal b} _ lookupL) =
 let
    Δ = (Δ₀ ,ₗ l ⦂ base Boolean)
    Δ' = Δ
    e'TypingJudgment = boolTy {Γ} {Δ = Δ'} b
  in
    pres {Δ = Δ} ty consis st Δ' e'TypingJudgment consis <*-refl
-- The code duplication below is very sad, but I haven't figured out a way that doesn't require refactoring the split judgment to be two-level.
preservation ty@(locTy {Γ} {Δ₀} {T₁ = contractType t₁} {T₂ = contractType t₂} {T₃ = contractType t₃} l spl@(unownedSplit _ _ _ _))
                       consis@(ok Δ voidLookup boolLookup objLookup refConsistencyFunc)
                       st@(SElookup {Σ} {l = l} {v = objVal o} _ lookupL) =
  let
    spl' = splitIdempotent spl
    e'TypingJudgment = objTy {Γ} {Δ = Δ''} {T₁ = contractType t₂} {T₂ = contractType t₂} {T₃ = contractType t₃} o spl'

    consis' = ok {Σ} Δ' voidLookup' boolLookup' objLookup' refConsistency'
  in
    pres {_} {_} {_} {_} {Δ = Δ} {Δ'' = Δ''} {_} {_} {_} ty consis st Δ' e'TypingJudgment consis' <*-o-extension
  where
    splT = splitType spl
    Δ'' = Δ₀ ,ₗ l ⦂ (SplitType.t₃ splT) -- This is the result of checking e.
    Δ' = Δ'' ,ₒ o ⦂ (SplitType.t₂ splT) -- This is the typing context in which we need to typecheck e'.
    --Δ = Δ₀ ,ₗ l ⦂ (SplitType.t₁ splT)
    -- Show that if you look up l in the new context, you get the same type as before.
    voidLookup' : (∀ (l' : IndirectRef)
                  → ((StaticEnv.locEnv Δ') ∋ l' ⦂ base Void
                  → (RuntimeEnv.ρ Σ IndirectRefContext.∋ l' ⦂ voidVal)))
    voidLookup' l' l'InΔ' with l' Data.Nat.≟ l
    voidLookup' l' (Context.S l'NeqL l'VoidType) | yes eq = ⊥-elim (l'NeqL eq)
    voidLookup' l' l'InΔ' | no nEq = voidLookup l' (S nEq (irrelevantReductionsOK l'InΔ' nEq))

    boolLookup' : (∀ (l' : IndirectRef)
                  → ((StaticEnv.locEnv Δ') ∋ l' ⦂ base Boolean
                  → ∃[ b ] (RuntimeEnv.ρ Σ IndirectRefContext.∋ l' ⦂ boolVal b)))
    boolLookup' l' l'InΔ' with l' Data.Nat.≟ l
    boolLookup' l' (Context.S l'NeqL l'BoolType) | yes eq = ⊥-elim (l'NeqL eq)
    boolLookup' l' l'InΔ' | no nEq = boolLookup l' (S nEq (irrelevantReductionsOK l'InΔ' nEq))

    objLookup' : (l' : IndirectRef) → (T : Tc)
                  → ((StaticEnv.locEnv Δ') ∋ l' ⦂ (contractType T)
                  → ∃[ o ] (RuntimeEnv.ρ Σ IndirectRefContext.∋ l' ⦂ objVal o × (o ObjectRefContext.∈dom (RuntimeEnv.μ Σ))))
    objLookup' l' _ l'InΔ' with l' Data.Nat.≟ l
    objLookup' l' _ (Context.S l'NeqL l'ObjType) | yes eq = ⊥-elim (l'NeqL eq)
    objLookup' l' t l'InΔ'@(Z {a = contractType t₃}) | yes eq = objLookup l' t₁ Z
    objLookup' l' t l'InΔ' | no nEq = objLookup l' t (S nEq (irrelevantReductionsOK l'InΔ' nEq))

    lookupUnique : objVal o ≡ objVal ( proj₁ (objLookup l t₁ Z))
    lookupUnique = IndirectRefContext.contextLookupUnique {RuntimeEnv.ρ Σ} lookupL (proj₁ (proj₂ (objLookup l t₁ Z)))
    oLookupUnique = objValInjectiveContrapositive lookupUnique

    -- Show that all location-based aliases from the previous environment are compatible with the new alias.
    -- Note that Σ is unchanged, so we use Σ instead of defining a separate Σ'.
    refConsistency' : (o' : ObjectRef) → o' ObjectRefContext.∈dom (RuntimeEnv.μ Σ) → ReferenceConsistency Σ Δ' o'
    refConsistency' o' o'Inμ =
      let
        origRefConsistency = refConsistencyFunc o' o'Inμ
        origConnected =  referencesConsistentImpliesConnectivity origRefConsistency
        newConnected = splitReplacementOK {Γ} {Σ} {Δ₀} {o} {o'} {l} {t₁} {t₂} {SplitType.t₁ splT} {SplitType.t₂ splT} {SplitType.t₃ splT}
                                          refl refl consis oLookupUnique (proj₁ origConnected) (proj₂ origConnected) spl
      in
        referencesConsistent {_} {_} {o'} newConnected

preservation ty@(locTy {Γ} {Δ₀} {T₁ = contractType t₁} {T₂ = contractType t₂} {T₃ = contractType t₃} l spl@(shared-shared-shared _))
                       consis@(ok Δ voidLookup boolLookup objLookup refConsistencyFunc)
                       st@(SElookup {Σ} {l = l} {v = objVal o} _ lookupL) =
   let
    spl' = splitIdempotent spl
    e'TypingJudgment = objTy {Γ} {Δ = Δ''} {T₁ = contractType t₂} {T₂ = contractType t₂} {T₃ = contractType t₃} o spl'

    consis' = ok {Σ} Δ' voidLookup' boolLookup' objLookup' refConsistency'
  in
    pres {_} {_} {_} {_} {Δ = Δ} {Δ'' = Δ''} {_} {_} {_} ty consis st Δ' e'TypingJudgment consis' <*-o-extension
  where
    splT = splitType spl
    Δ'' = Δ₀ ,ₗ l ⦂ (SplitType.t₃ splT) -- This is the result of checking e.
    Δ' = Δ'' ,ₒ o ⦂ (SplitType.t₂ splT) -- This is the typing context in which we need to typecheck e'.
    --Δ = Δ₀ ,ₗ l ⦂ (SplitType.t₁ splT)
    -- Show that if you look up l in the new context, you get the same type as before.
    voidLookup' : (∀ (l' : IndirectRef)
                  → ((StaticEnv.locEnv Δ') ∋ l' ⦂ base Void
                  → (RuntimeEnv.ρ Σ IndirectRefContext.∋ l' ⦂ voidVal)))
    voidLookup' l' l'InΔ' with l' Data.Nat.≟ l
    voidLookup' l' (Context.S l'NeqL l'VoidType) | yes eq = ⊥-elim (l'NeqL eq)
    voidLookup' l' l'InΔ' | no nEq = voidLookup l' (S nEq (irrelevantReductionsOK l'InΔ' nEq))

    boolLookup' : (∀ (l' : IndirectRef)
                  → ((StaticEnv.locEnv Δ') ∋ l' ⦂ base Boolean
                  → ∃[ b ] (RuntimeEnv.ρ Σ IndirectRefContext.∋ l' ⦂ boolVal b)))
    boolLookup' l' l'InΔ' with l' Data.Nat.≟ l
    boolLookup' l' (Context.S l'NeqL l'BoolType) | yes eq = ⊥-elim (l'NeqL eq)
    boolLookup' l' l'InΔ' | no nEq = boolLookup l' (S nEq (irrelevantReductionsOK l'InΔ' nEq))

    objLookup' : (l' : IndirectRef) → (T : Tc)
                  → ((StaticEnv.locEnv Δ') ∋ l' ⦂ (contractType T)
                  → ∃[ o ] (RuntimeEnv.ρ Σ IndirectRefContext.∋ l' ⦂ objVal o × (o ObjectRefContext.∈dom (RuntimeEnv.μ Σ))))
    objLookup' l' _ l'InΔ' with l' Data.Nat.≟ l
    objLookup' l' _ (Context.S l'NeqL l'ObjType) | yes eq = ⊥-elim (l'NeqL eq)
    objLookup' l' t l'InΔ'@(Z {a = contractType t₃}) | yes eq = objLookup l' t₁ Z
    objLookup' l' t l'InΔ' | no nEq = objLookup l' t (S nEq (irrelevantReductionsOK l'InΔ' nEq))

    lookupUnique : objVal o ≡ objVal ( proj₁ (objLookup l t₁ Z))
    lookupUnique = IndirectRefContext.contextLookupUnique {RuntimeEnv.ρ Σ} lookupL (proj₁ (proj₂ (objLookup l t₁ Z)))
    oLookupUnique = objValInjectiveContrapositive lookupUnique

    -- Show that all location-based aliases from the previous environment are compatible with the new alias.
    -- Note that Σ is unchanged, so we use Σ instead of defining a separate Σ'.
    refConsistency' : (o' : ObjectRef) → o' ObjectRefContext.∈dom (RuntimeEnv.μ Σ) → ReferenceConsistency Σ Δ' o'
    refConsistency' o' o'Inμ =
      let
        origRefConsistency = refConsistencyFunc o' o'Inμ
        origConnected =  referencesConsistentImpliesConnectivity origRefConsistency
        newConnected = splitReplacementOK {Γ} {Σ} {Δ₀} {o} {o'} {l} {t₁} {t₂} {SplitType.t₁ splT} {SplitType.t₂ splT} {SplitType.t₃ splT}
                                          refl refl consis oLookupUnique (proj₁ origConnected) (proj₂ origConnected) spl
      in
        referencesConsistent {_} {_} {o'} newConnected
preservation ty@(locTy {Γ} {Δ₀} {T₁ = contractType t₁} {T₂ = contractType t₂} {T₃ = contractType t₃} l spl@(owned-shared _))
                       consis@(ok Δ voidLookup boolLookup objLookup refConsistencyFunc)
                       st@(SElookup {Σ} {l = l} {v = objVal o} _ lookupL) =
   let
    spl' = splitIdempotent spl
    e'TypingJudgment = objTy {Γ} {Δ = Δ''} {T₁ = contractType t₂} {T₂ = contractType t₂} {T₃ = contractType t₃} o spl'

    consis' = ok {Σ} Δ' voidLookup' boolLookup' objLookup' refConsistency'
  in
    pres {_} {_} {_} {_} {Δ = Δ} {Δ'' = Δ''} {_} {_} {_} ty consis st Δ' e'TypingJudgment consis' <*-o-extension
  where
    splT = splitType spl
    Δ'' = Δ₀ ,ₗ l ⦂ (SplitType.t₃ splT) -- This is the result of checking e.
    Δ' = Δ'' ,ₒ o ⦂ (SplitType.t₂ splT) -- This is the typing context in which we need to typecheck e'.
    --Δ = Δ₀ ,ₗ l ⦂ (SplitType.t₁ splT)
    -- Show that if you look up l in the new context, you get the same type as before.
    voidLookup' : (∀ (l' : IndirectRef)
                  → ((StaticEnv.locEnv Δ') ∋ l' ⦂ base Void
                  → (RuntimeEnv.ρ Σ IndirectRefContext.∋ l' ⦂ voidVal)))
    voidLookup' l' l'InΔ' with l' Data.Nat.≟ l
    voidLookup' l' (Context.S l'NeqL l'VoidType) | yes eq = ⊥-elim (l'NeqL eq)
    voidLookup' l' l'InΔ' | no nEq = voidLookup l' (S nEq (irrelevantReductionsOK l'InΔ' nEq))

    boolLookup' : (∀ (l' : IndirectRef)
                  → ((StaticEnv.locEnv Δ') ∋ l' ⦂ base Boolean
                  → ∃[ b ] (RuntimeEnv.ρ Σ IndirectRefContext.∋ l' ⦂ boolVal b)))
    boolLookup' l' l'InΔ' with l' Data.Nat.≟ l
    boolLookup' l' (Context.S l'NeqL l'BoolType) | yes eq = ⊥-elim (l'NeqL eq)
    boolLookup' l' l'InΔ' | no nEq = boolLookup l' (S nEq (irrelevantReductionsOK l'InΔ' nEq))

    objLookup' : (l' : IndirectRef) → (T : Tc)
                  → ((StaticEnv.locEnv Δ') ∋ l' ⦂ (contractType T)
                  → ∃[ o ] (RuntimeEnv.ρ Σ IndirectRefContext.∋ l' ⦂ objVal o × (o ObjectRefContext.∈dom (RuntimeEnv.μ Σ))))
    objLookup' l' _ l'InΔ' with l' Data.Nat.≟ l
    objLookup' l' _ (Context.S l'NeqL l'ObjType) | yes eq = ⊥-elim (l'NeqL eq)
    objLookup' l' t l'InΔ'@(Z {a = contractType t₃}) | yes eq = objLookup l' t₁ Z
    objLookup' l' t l'InΔ' | no nEq = objLookup l' t (S nEq (irrelevantReductionsOK l'InΔ' nEq))

    lookupUnique : objVal o ≡ objVal ( proj₁ (objLookup l t₁ Z))
    lookupUnique = IndirectRefContext.contextLookupUnique {RuntimeEnv.ρ Σ} lookupL (proj₁ (proj₂ (objLookup l t₁ Z)))
    oLookupUnique = objValInjectiveContrapositive lookupUnique

    -- Show that all location-based aliases from the previous environment are compatible with the new alias.
    -- Note that Σ is unchanged, so we use Σ instead of defining a separate Σ'.
    refConsistency' : (o' : ObjectRef) → o' ObjectRefContext.∈dom (RuntimeEnv.μ Σ) → ReferenceConsistency Σ Δ' o'
    refConsistency' o' o'Inμ =
      let
        origRefConsistency = refConsistencyFunc o' o'Inμ
        origConnected =  referencesConsistentImpliesConnectivity origRefConsistency
        newConnected = splitReplacementOK {Γ} {Σ} {Δ₀} {o} {o'} {l} {t₁} {t₂} {SplitType.t₁ splT} {SplitType.t₂ splT} {SplitType.t₃ splT}
                                          refl refl consis oLookupUnique (proj₁ origConnected) (proj₂ origConnected) spl
      in
        referencesConsistent {_} {_} {o'} newConnected
preservation ty@(locTy {Γ} {Δ₀} {T₁ = contractType t₁} {T₂ = contractType t₂} {T₃ = contractType t₃} l spl@(states-shared _))
                       consis@(ok Δ voidLookup boolLookup objLookup refConsistencyFunc)
                       st@(SElookup {Σ} {l = l} {v = objVal o} _ lookupL) =
   let
    spl' = splitIdempotent spl
    e'TypingJudgment = objTy {Γ} {Δ = Δ''} {T₁ = contractType t₂} {T₂ = contractType t₂} {T₃ = contractType t₃} o spl'

    consis' = ok {Σ} Δ' voidLookup' boolLookup' objLookup' refConsistency'
  in
    pres {_} {_} {_} {_} {Δ = Δ} {Δ'' = Δ''} {_} {_} {_} ty consis st Δ' e'TypingJudgment consis' <*-o-extension
  where
    splT = splitType spl
    Δ'' = Δ₀ ,ₗ l ⦂ (SplitType.t₃ splT) -- This is the result of checking e.
    Δ' = Δ'' ,ₒ o ⦂ (SplitType.t₂ splT) -- This is the typing context in which we need to typecheck e'.
    --Δ = Δ₀ ,ₗ l ⦂ (SplitType.t₁ splT)
    -- Show that if you look up l in the new context, you get the same type as before.
    voidLookup' : (∀ (l' : IndirectRef)
                  → ((StaticEnv.locEnv Δ') ∋ l' ⦂ base Void
                  → (RuntimeEnv.ρ Σ IndirectRefContext.∋ l' ⦂ voidVal)))
    voidLookup' l' l'InΔ' with l' Data.Nat.≟ l
    voidLookup' l' (Context.S l'NeqL l'VoidType) | yes eq = ⊥-elim (l'NeqL eq)
    voidLookup' l' l'InΔ' | no nEq = voidLookup l' (S nEq (irrelevantReductionsOK l'InΔ' nEq))

    boolLookup' : (∀ (l' : IndirectRef)
                  → ((StaticEnv.locEnv Δ') ∋ l' ⦂ base Boolean
                  → ∃[ b ] (RuntimeEnv.ρ Σ IndirectRefContext.∋ l' ⦂ boolVal b)))
    boolLookup' l' l'InΔ' with l' Data.Nat.≟ l
    boolLookup' l' (Context.S l'NeqL l'BoolType) | yes eq = ⊥-elim (l'NeqL eq)
    boolLookup' l' l'InΔ' | no nEq = boolLookup l' (S nEq (irrelevantReductionsOK l'InΔ' nEq))

    objLookup' : (l' : IndirectRef) → (T : Tc)
                  → ((StaticEnv.locEnv Δ') ∋ l' ⦂ (contractType T)
                  → ∃[ o ] (RuntimeEnv.ρ Σ IndirectRefContext.∋ l' ⦂ objVal o × (o ObjectRefContext.∈dom (RuntimeEnv.μ Σ))))
    objLookup' l' _ l'InΔ' with l' Data.Nat.≟ l
    objLookup' l' _ (Context.S l'NeqL l'ObjType) | yes eq = ⊥-elim (l'NeqL eq)
    objLookup' l' t l'InΔ'@(Z {a = contractType t₃}) | yes eq = objLookup l' t₁ Z
    objLookup' l' t l'InΔ' | no nEq = objLookup l' t (S nEq (irrelevantReductionsOK l'InΔ' nEq))

    lookupUnique : objVal o ≡ objVal ( proj₁ (objLookup l t₁ Z))
    lookupUnique = IndirectRefContext.contextLookupUnique {RuntimeEnv.ρ Σ} lookupL (proj₁ (proj₂ (objLookup l t₁ Z)))
    oLookupUnique = objValInjectiveContrapositive lookupUnique

    -- Show that all location-based aliases from the previous environment are compatible with the new alias.
    -- Note that Σ is unchanged, so we use Σ instead of defining a separate Σ'.
    refConsistency' : (o' : ObjectRef) → o' ObjectRefContext.∈dom (RuntimeEnv.μ Σ) → ReferenceConsistency Σ Δ' o'
    refConsistency' o' o'Inμ =
      let
        origRefConsistency = refConsistencyFunc o' o'Inμ
        origConnected =  referencesConsistentImpliesConnectivity origRefConsistency
        newConnected = splitReplacementOK {Γ} {Σ} {Δ₀} {o} {o'} {l} {t₁} {t₂} {SplitType.t₁ splT} {SplitType.t₂ splT} {SplitType.t₃ splT}
                                          refl refl consis oLookupUnique (proj₁ origConnected) (proj₂ origConnected) spl
      in
        referencesConsistent {_} {_} {o'} newConnected

preservation {T = contractType t₂}
  (locTy {Γ} {Δ₀} {contractType t₁} {.(contractType t₂)} {contractType t₃} l spl)
  (ok .(Δ₀ ,ₗ l ⦂ contractType t₁) voidLookup boolLookup objLookup refConsistencyFunc)
  (SElookup {Σ} {l = l} {boolVal b} _ lookupL) =
    -- The context says the location refers to a contract, but also a boolean value?? Inconsistent.
      ⊥-elim (lookupNeq lookupUnique)
    where
      objLookupResult = objLookup l t₁ Z
      o = proj₁ objLookupResult
      lHasObjType = proj₁ (proj₂ objLookupResult)
      lookupUnique = IndirectRefContext.contextLookupUnique lHasObjType lookupL
      lookupNeq : (objVal o) ≢ boolVal b
      lookupNeq ()

preservation {T = contractType t₂}
  (locTy {Γ} {Δ₀} {contractType t₁} {.(contractType t₂)} {contractType t₃} l spl)
  (ok .(Δ₀ ,ₗ l ⦂ contractType t₁) voidLookup boolLookup objLookup refConsistencyFunc)
  (SElookup {Σ} {l = l} {voidVal} _ lookupL) =
    -- The context says the location refers to a contract, but also a boolean value?? Inconsistent.
      ⊥-elim (lookupNeq lookupUnique)
    where
      objLookupResult = objLookup l t₁ Z
      o = proj₁ objLookupResult
      lHasObjType = proj₁ (proj₂ objLookupResult)
      lookupUnique = IndirectRefContext.contextLookupUnique lHasObjType lookupL
      lookupNeq : (objVal o) ≢ voidVal
      lookupNeq ()

preservation
  (locTy {Γ} {Δ₀} {.(base Void)} l voidSplit)
  (ok .(Δ₀ ,ₗ l ⦂ base Void) voidLookup boolLookup objLookup refConsistencyFunc)
  (SElookup {Σ} {Δ} {T = T} {l = l} {boolVal b} lookupLType lookupL) =
            ⊥-elim (lookupNeq lookupUnique)
    where
      lLookupResult = voidLookup l Z
      lookupUnique = IndirectRefContext.contextLookupUnique lLookupResult lookupL
      lookupNeq : voidVal ≢ boolVal b
      lookupNeq ()

preservation
  (locTy {Γ} {Δ₀} {.(base Void)} l voidSplit)
  (ok .(Δ₀ ,ₗ l ⦂ base Void) voidLookup boolLookup objLookup refConsistencyFunc)
  (SElookup {Σ} {Δ} {T = T} {l = l} {objVal o} lookupLType lookupL) =
            ⊥-elim (lookupNeq lookupUnique)
    where
      lLookupResult = voidLookup l Z
      lookupUnique = IndirectRefContext.contextLookupUnique lLookupResult lookupL
      lookupNeq : voidVal ≢ objVal o
      lookupNeq ()

preservation
  (locTy {Γ} {Δ₀} {.(base Boolean)} l booleanSplit)
  (ok .(Δ₀ ,ₗ l ⦂ base Boolean) voidLookup boolLookup objLookup refConsistencyFunc)
  (SElookup {Σ} {Δ} {T = T} {l = l} {voidVal} lookupLType lookupL) =
            ⊥-elim (lookupNeq lookupUnique)
    where
      lLookupResult = boolLookup l Z
      lookupUnique = IndirectRefContext.contextLookupUnique (proj₂ lLookupResult) lookupL
      lookupNeq : boolVal (proj₁ lLookupResult) ≢ voidVal
      lookupNeq ()

preservation
  (locTy {Γ} {Δ₀} {.(base Boolean)} l booleanSplit)
  (ok .(Δ₀ ,ₗ l ⦂ base Boolean) voidLookup boolLookup objLookup refConsistencyFunc)
  (SElookup {Σ} {Δ} {T = T} {l = l} {objVal o} lookupLType lookupL) =
            ⊥-elim (lookupNeq lookupUnique)
    where
      lLookupResult = boolLookup l Z
      lookupUnique = IndirectRefContext.contextLookupUnique (proj₂ lLookupResult) lookupL
      lookupNeq : boolVal (proj₁ lLookupResult) ≢ objVal o
      lookupNeq ()

preservation {Γ = Γ} {Δ = Δ} {Δ'' = Δ''} ty@(assertTyₓ _ _) consis st@(SEassertₓ x s) =
  pres ty consis st Δ (voidTy {Γ = Γ} {Δ = Δ}) consis <*-refl
preservation {Γ = Γ} {Δ = Δ} {Δ'' = Δ''} ty@(assertTyₗ _ _) consis st@(SEassertₗ x s) =
  pres ty consis st Δ (voidTy {Γ = Γ} {Δ = Δ}) consis <*-refl

preservation  {Γ = Γ} {Δ = Δ} {Δ'' = Δ''}
  ty@(newTy {C = C} {st = st} stOK ty₁ ty₂ CInΓ refl)
  consis
  step@(SEnew {Σ} {o = o} oFresh refl refl) =
    pres ty consis step Δ' newTypeJudgment {!!} {!!}
    where
      T = contractType (tc C (S [ st ]) )
      Δ' = Δ ,ₒ o ⦂ T
      spl = unownedSplit {Γ} refl refl refl refl
      newTypeJudgment = objTy o spl

max_stars_repo_name: ivoysey/Obsidian

max_issues_repo_name: ivoysey/Obsidian

max_forks_repo_name: ivoysey/Obsidian


text:
{-

Set quotients:

-}

{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.SetQuotients.Properties where

open import Cubical.HITs.SetQuotients.Base

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.Univalence

open import Cubical.Data.Sigma

open import Cubical.Relation.Nullary
open import Cubical.Relation.Binary.Base

open import Cubical.HITs.PropositionalTruncation as PropTrunc using (∥_∥; ∣_∣; squash)
open import Cubical.HITs.SetTruncation as SetTrunc using (∥_∥₂; ∣_∣₂; squash₂)

-- Type quotients

private
  variable
    ℓ : Level
    A : Type ℓ
    R : A → A → Type ℓ
    B : A / R → Type ℓ
    C : A / R → A / R → Type ℓ
    D : A / R → A / R → A / R → Type ℓ

elimEq/ : (Bprop : (x : A / R ) → isProp (B x))
          {x y : A / R}
          (eq : x ≡ y)
          (bx : B x)
          (by : B y) →
          PathP (λ i → B (eq i)) bx by
elimEq/ {B = B} Bprop {x = x} =
  J (λ y eq → ∀ bx by → PathP (λ i → B (eq i)) bx by) (λ bx by → Bprop x bx by)

elimProp : ((x : A / R ) → isProp (B x))
         → ((a : A) → B ( [ a ]))
         → (x : A / R)
         → B x
elimProp Bprop f [ x ] = f x
elimProp Bprop f (squash/ x y p q i j) =
  isOfHLevel→isOfHLevelDep 2 (λ x → isProp→isSet (Bprop x))
    (g x) (g y) (cong g p) (cong g q) (squash/ x y p q) i j
    where
    g = elimProp Bprop f
elimProp Bprop f (eq/ a b r i) = elimEq/ Bprop (eq/ a b r) (f a) (f b) i

elimProp2 : ((x y : A / R ) → isProp (C x y))
          → ((a b : A) → C [ a ] [ b ])
          → (x y : A / R)
          → C x y
elimProp2 Cprop f = elimProp (λ x → isPropΠ (λ y → Cprop x y))
                             (λ x → elimProp (λ y → Cprop [ x ] y) (f x))

elimProp3 : ((x y z : A / R ) → isProp (D x y z))
          → ((a b c : A) → D [ a ] [ b ] [ c ])
          → (x y z : A / R)
          → D x y z
elimProp3 Dprop f = elimProp (λ x → isPropΠ2 (λ y z → Dprop x y z))
                             (λ x → elimProp2 (λ y z → Dprop [ x ] y z) (f x))

-- lemma 6.10.2 in hott book
[]surjective : (x : A / R) → ∃[ a ∈ A ] [ a ] ≡ x
[]surjective = elimProp (λ x → squash) (λ a → ∣ a , refl ∣)

elim : {B : A / R → Type ℓ}
     → ((x : A / R) → isSet (B x))
     → (f : (a : A) → (B [ a ]))
     → ((a b : A) (r : R a b) → PathP (λ i → B (eq/ a b r i)) (f a) (f b))
     → (x : A / R)
     → B x
elim Bset f feq [ a ] = f a
elim Bset f feq (eq/ a b r i) = feq a b r i
elim Bset f feq (squash/ x y p q i j) =
  isOfHLevel→isOfHLevelDep 2 Bset
              (g x) (g y) (cong g p) (cong g q) (squash/ x y p q) i j
    where
      g = elim Bset f feq

rec : {B : Type ℓ}
      (Bset : isSet B)
      (f : A → B)
      (feq : (a b : A) (r : R a b) → f a ≡ f b)
    → A / R → B
rec Bset f feq [ a ] = f a
rec Bset f feq (eq/ a b r i) = feq a b r i
rec Bset f feq (squash/ x y p q i j) = Bset (g x) (g y) (cong g p) (cong g q) i j
  where
  g = rec Bset f feq

rec2 : {B : Type ℓ} (Bset : isSet B)
       (f : A → A → B) (feql : (a b c : A) (r : R a b) → f a c ≡ f b c)
                       (feqr : (a b c : A) (r : R b c) → f a b ≡ f a c)
    → A / R → A / R → B
rec2 Bset f feql feqr = rec (isSetΠ (λ _ → Bset))
                            (λ a → rec Bset (f a) (feqr a))
                            (λ a b r → funExt (elimProp (λ _ → Bset _ _)
                                              (λ c → feql a b c r)))

setQuotUniversal : {B : Type ℓ} (Bset : isSet B) →
                   (A / R → B) ≃ (Σ[ f ∈ (A → B) ] ((a b : A) → R a b → f a ≡ f b))
setQuotUniversal Bset = isoToEquiv (iso intro out outRightInv outLeftInv)
  where
  intro = λ g →  (λ a → g [ a ]) , λ a b r i → g (eq/ a b r i)
  out = λ h → elim (λ x → Bset) (fst h) (snd h)

  outRightInv : ∀ h → intro (out h) ≡ h
  outRightInv h = refl

  outLeftInv : ∀ g → out (intro g) ≡ g
  outLeftInv = λ g → funExt (λ x → PropTrunc.elim {P = λ sur → out (intro g) x ≡ g x}
    (λ sur → Bset (out (intro g) x) (g x))
    (λ sur → cong (out (intro g)) (sym (snd sur)) ∙ (cong g (snd sur))) ([]surjective x)
    )

open BinaryRelation

effective : (Rprop : isPropValued R) (Requiv : isEquivRel R) (a b : A) → [ a ] ≡ [ b ] → R a b
effective {A = A} {R = R} Rprop (equivRel R/refl R/sym R/trans) a b p = transport aa≡ab (R/refl _)
  where
    helper : A / R → hProp _
    helper =
      rec isSetHProp (λ c → (R a c , Rprop a c))
                     (λ c d cd → Σ≡Prop (λ _ → isPropIsProp)
                                        (hPropExt (Rprop a c) (Rprop a d)
                                                  (λ ac → R/trans _ _ _ ac cd) (λ ad → R/trans _ _ _ ad (R/sym _ _ cd))))

    aa≡ab : R a a ≡ R a b
    aa≡ab i = helper (p i) .fst

isEquivRel→isEffective : isPropValued R → isEquivRel R → isEffective R
isEquivRel→isEffective {R = R} Rprop Req a b = isoToIsEquiv (iso out intro out-intro intro-out)
  where
    intro : [ a ] ≡ [ b ] → R a b
    intro = effective Rprop Req a b

    out : R a b → [ a ] ≡ [ b ]
    out = eq/ a b

    intro-out : ∀ x → intro (out x) ≡ x
    intro-out ab = Rprop a b _ _

    out-intro : ∀ x → out (intro x) ≡ x
    out-intro eq = squash/ _ _ _ _

discreteSetQuotients : Discrete A → isPropValued R → isEquivRel R → (∀ a₀ a₁ → Dec (R a₀ a₁)) → Discrete (A / R)
discreteSetQuotients {A = A} {R = R} Adis Rprop Req Rdec =
  elim (λ a₀ → isSetΠ (λ a₁ → isProp→isSet (isPropDec (squash/ a₀ a₁))))
    discreteSetQuotients' discreteSetQuotients'-eq
  where
    discreteSetQuotients' : (a : A) (y : A / R) → Dec ([ a ] ≡ y)
    discreteSetQuotients' a₀ = elim (λ a₁ → isProp→isSet (isPropDec (squash/ [ a₀ ] a₁))) dis dis-eq
      where
        dis : (a₁ : A) → Dec ([ a₀ ] ≡ [ a₁ ])
        dis a₁ with Rdec a₀ a₁
        ... | (yes p) = yes (eq/ a₀ a₁ p)
        ... | (no ¬p) = no λ eq → ¬p (effective Rprop Req a₀ a₁ eq )

        dis-eq : (a b : A) (r : R a b) →
          PathP (λ i → Dec ([ a₀ ] ≡ eq/ a b r i)) (dis a) (dis b)
        dis-eq a b ab = J (λ b ab → ∀ k → PathP (λ i → Dec ([ a₀ ] ≡ ab i)) (dis a) k)
                          (λ k → isPropDec (squash/ _ _) _  _) (eq/ a b ab) (dis b)

    discreteSetQuotients'-eq : (a b : A) (r : R a b) →
      PathP (λ i → (y : A / R) → Dec (eq/ a b r i ≡ y))
            (discreteSetQuotients' a) (discreteSetQuotients' b)
    discreteSetQuotients'-eq a b ab =
      J (λ b ab → ∀ k → PathP (λ i → (y : A / R) → Dec (ab i ≡ y))
                              (discreteSetQuotients' a) k)
        (λ k → funExt (λ x → isPropDec (squash/ _ _) _ _)) (eq/ a b ab) (discreteSetQuotients' b)

max_stars_repo_name: ayberkt/cubical

max_issues_repo_name: ayberkt/cubical

max_forks_repo_name: ayberkt/cubical


text:
{-# OPTIONS --sized-types #-}

open import Common.Size

data Heap : (i j : Size) → Set where
  node : (i j : Size) → Heap (↑ i) (↑ j)

postulate
  _∪_ : Heap ∞ ∞ → Heap ∞ ∞ → Heap ∞ ∞
  mkH : ∀ i j → Heap i j

merge : (i j : Size) → Heap i j → Heap ∞ ∞
merge .(↑ i) .(↑ j) (node i j) with Set
merge .(↑ i) .(↑ j) (node i j) | _ =
  merge i (↑ j) (mkH i (↑ j)) ∪
  merge (↑ i) j (mkH (↑ i) j)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
postulate A : Set

module _ {{a : A}} (f : A → A) where

  g : {{a : A}} → A
  g {{a}} = a

  t : A
  t = g


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

module Module where

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)
open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Structures.Ring
open import Cubical.Structures.Group
open import Cubical.Structures.AbGroup

open import NumberBundles2

record IsLeftRModule {ℓ ℓᴿ : Level}
  {R : Type ℓᴿ} (   1ᴿ : R) (_+ᴿ_ _·ᴿ_ : R → R → R)
  {X  : Type ℓ} (0ᴹ    : X) (_+ᴹ_      : X → X → X) (_·ᴹ_ : R → X → X) (-ᴹ_ : X → X)
  : Type (ℓ-max ℓ ℓᴿ) where
  field
    isAbGroupᴹ  : IsAbGroup 0ᴹ    _+ᴹ_      -ᴹ_
    ·ᴹ-dist-+ᴹ  : ∀ r x y → r ·ᴹ (x +ᴹ y) ≡ (r ·ᴹ x) +ᴹ (r ·ᴹ y)
    ·ᴹ-dist-+ᴿ  : ∀ r s x → (r +ᴿ s) ·ᴹ x ≡ (r ·ᴹ x) +ᴹ (s ·ᴹ x)
    ·ᴹ-assoc-·ᴿ : ∀ r s x → (r ·ᴿ s) ·ᴹ x ≡ r ·ᴹ (s ·ᴹ x)
    ·ᴹ-identity : ∀ x → 1ᴿ ·ᴹ x ≡ x
  open IsAbGroup isAbGroupᴹ renaming
    ( _-_ to _-ᴹ_
    ; assoc       to +ᴹ-assoc
    ; identity    to +ᴹ-identity
    ; lid         to +ᴹ-lid
    ; rid         to +ᴹ-rid
    ; inverse     to +ᴹ-inv
    ; invl        to +ᴹ-linv
    ; invr        to +ᴹ-rinv
    ; comm        to +ᴹ-comm
    ; isSemigroup to +ᴹ-isSemigroup
    ; isMonoid    to +ᴹ-isMonoid
    ; isGroup     to +ᴹ-isGroup
    ) public

ApartnessRingWithAbs = Ring -- TODO define `ApartnessRingWithAbs`

record LeftRModule {ℓ ℓᴿ : Level} (ring : ApartnessRingWithAbs {ℓᴿ}) : Type (ℓ-suc (ℓ-max ℓ ℓᴿ)) where
  open Ring ring renaming
    ( Carrier       to Carrierᴿ
    ; 0r            to 0ᴿ
    ; 1r            to 1ᴿ
    ; _+_           to _+ᴿ_
    ; _·_           to _·ᴿ_
    ; -_            to -ᴿ_
    ; is-set        to is-setᴿ
    ; +-assoc       to +ᴿ-assoc
    ; +-identity    to +ᴿ-identity
    ; +-lid         to +ᴿ-lid
    ; +-rid         to +ᴿ-rid
    ; +-inv         to +ᴿ-inv
    ; +-linv        to +ᴿ-linv
    ; +-rinv        to +ᴿ-rinv
    ; +-comm        to +ᴿ-comm
    ; +-isSemigroup to +ᴿ-isSemigroup
    ; +-isMonoid    to +ᴿ-isMonoid
    ; +-isGroup     to +ᴿ-isGroup
    ; ·-assoc       to ·ᴿ-assoc
    ; ·-identity    to ·ᴿ-identity
    ; ·-lid         to ·ᴿ-lid
    ; ·-rid         to ·ᴿ-rid
    ; ·-isSemigroup to ·ᴿ-isSemigroup
    ; ·-rdist-+     to ·ᴿ-rdist-+ᴿ
    ; ·-ldist-+     to ·ᴿ-ldist-+ᴿ
    ) public

  field
    Carrier  : Type ℓ
    0ᴹ       : Carrier
    _+ᴹ_     : Carrier → Carrier → Carrier
    _·ᴹ_     : Carrierᴿ → Carrier → Carrier
    -ᴹ_      : Carrier → Carrier
    isLeftRModule : IsLeftRModule 1ᴿ _+ᴿ_ _·ᴿ_ 0ᴹ _+ᴹ_ _·ᴹ_ -ᴹ_

  open IsLeftRModule isLeftRModule public

  infix  8 -ᴹ_
  infixl 7 _·ᴹ_
  infixl 6 _+ᴹ_

record LeftKModule {ℓ ℓᴷ : Level} (ffield : CompleteApartnessFieldWithAbs {ℓᴷ}) : Type (ℓ-suc (ℓ-max ℓ ℓᴷ)) where
   open CompleteApartnessFieldWithAbs ffield renaming
     ( Carrier       to Carrierᴷ
     ; 0f            to 0ᴷ
     ; 1f            to 1ᴷ
     ; _+_           to _+ᴷ_
     ; _·_           to _·ᴷ_
     ; -_            to -ᴷ_
     ) public
   field
     Carrier  : Type ℓ
     0ᴹ       : Carrier
     _+ᴹ_     : Carrier → Carrier → Carrier
     _·ᴹ_     : Carrierᴷ → Carrier → Carrier
     -ᴹ_      : Carrier → Carrier
     isLeftRModule : IsLeftRModule 1ᴷ _+ᴷ_ _·ᴷ_ 0ᴹ _+ᴹ_ _·ᴹ_ -ᴹ_

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


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

module Data.Tuple.UniverseMonomorphic where

open import Prelude
open import Data.Fin
Tuple : ∀ n → (Fin n → Type) → Type
Tuple zero     f = ⊤
Tuple (suc n)  f = f f0 × Tuple n (f ∘ fs)

private
  variable
    n : ℕ
    U : Fin n → Type

ind : Tuple n U → (i : Fin n) → U i
ind {n = suc n} (x , xs) f0     = x
ind {n = suc n} (x , xs) (fs i) = ind xs i

tab : ((i : Fin n) → U i) → Tuple n U
tab {n = zero}  f = tt
tab {n = suc n} f = f f0 , tab (f ∘ fs)

Π→Tuple→Π : ∀ {n} {U : Fin n → Type} (xs : (i : Fin n) → U i) i → ind (tab xs) i ≡ xs i
Π→Tuple→Π {n = suc n} f f0 = refl
Π→Tuple→Π {n = suc n} f (fs i) = Π→Tuple→Π (f ∘ fs) i

Tuple→Π→Tuple : ∀ {n} {U : Fin n → Type} (xs : Tuple n U) → tab (ind xs) ≡ xs
Tuple→Π→Tuple {n = zero} tt = refl
Tuple→Π→Tuple {n = suc n} (x , xs) i .fst = x
Tuple→Π→Tuple {n = suc n} (x , xs) i .snd = Tuple→Π→Tuple xs i

Tuple⇔ΠFin :
 Tuple n U ⇔ ((i : Fin n) → U i)
Tuple⇔ΠFin .fun = ind
Tuple⇔ΠFin .inv = tab
Tuple⇔ΠFin .leftInv = Tuple→Π→Tuple
Tuple⇔ΠFin .rightInv x = funExt (Π→Tuple→Π x)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
{-
  This file contains cospans, cones, pullbacks and maps of cones in precategories.
-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Cubical.Categories.Pullback where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma
open import Cubical.Categories.Category

private
  variable
    ℓ ℓ' : Level

record Cospan (𝒞 : Precategory ℓ ℓ') : Type (ℓ-max ℓ ℓ') where
  constructor cospan
  field
    S₁ S₂ vertex : Precategory.ob 𝒞
    s₁ : hom 𝒞 S₁ vertex
    s₂ : hom 𝒞 S₂ vertex

record Cone {𝒞 : Precategory ℓ ℓ'} (cspn : Cospan 𝒞) (c : ob 𝒞) : Type (ℓ-max ℓ ℓ') where
  constructor cone
  field
    p₁ : hom 𝒞 c (Cospan.S₁ cspn)
    p₂ : hom 𝒞 c (Cospan.S₂ cspn)
    sq : seq 𝒞 p₁ (Cospan.s₁ cspn) ≡ seq 𝒞 p₂ (Cospan.s₂ cspn)

record Pullback {𝒞 : Precategory ℓ ℓ'} (cspn : Cospan 𝒞) : Type (ℓ-max ℓ ℓ') where
  constructor pullback
  field
    c : ob 𝒞
    cn : Cone cspn c
    universal : {c' : ob 𝒞} (cn' : Cone cspn c') → ∃![ f ∈ 𝒞 .hom c' c ] Σ[ q ∈ Cone.p₁ cn' ≡ 𝒞 .seq f (Cone.p₁ cn) ] (Cone.p₂ cn' ≡ 𝒞 .seq f (Cone.p₂ cn))

-- whisker the parallel morphisms g and g' with f
lPrecatWhisker : {𝒞 : Precategory ℓ ℓ'} {x y z : 𝒞 .ob} (f : 𝒞 .hom x y) (g g' : 𝒞 .hom y z) (p : g ≡ g') → 𝒞 .seq f g ≡ 𝒞 .seq f g'
lPrecatWhisker {𝒞 = 𝒞} f _ _ p = cong (𝒞 .seq f) p

-- extend a cone on c by a morphism c'→c using precomposition
coneMap : {𝒞 : Precategory ℓ ℓ'} {cspn : Cospan 𝒞} {c c' : ob 𝒞} (cn : Cone cspn c) (f : hom 𝒞 c' c) → Cone cspn c'
coneMap {𝒞 = 𝒞} {cospan _ _ _ s₁ s₂} (cone p₁ p₂ sq) f =
  cone (𝒞 .seq f p₁)  (𝒞 .seq f p₂) ((𝒞 .seq-α f p₁ s₁) ∙∙ lPrecatWhisker {𝒞 = 𝒞} f (𝒞 .seq p₁ s₁) (𝒞 .seq p₂ s₂) sq ∙∙ sym (𝒞 .seq-α f p₂ s₂))


text:
module Common.Semantics where

open import Common.Context public

-- Special products for glueing.

infix 5 _⅋_
record Glue (Syn : Set) (Sem : Set) : Set where
  constructor _⅋_
  field
    syn : Syn
    sem : Sem

open Glue public

-- Contexts as concrete worlds.

module ConcreteWorlds (U : Set) where
  record World : Set where
    constructor wrap
    field
      Γ : Cx U

  unwrap : World → Cx U
  unwrap (wrap Γ) = Γ

  data _≤_ : World → World → Set where
    wrap : ∀ {Γ Γ′} → Γ ⊆ Γ′ → wrap Γ ≤ wrap Γ′

  unwrap≤ : ∀ {Γ Γ′} → wrap Γ ≤ wrap Γ′ → Γ ⊆ Γ′
  unwrap≤ (wrap η) = η

  refl≤ : ∀ {w} → w ≤ w
  refl≤ = wrap refl⊆

  trans≤ : ∀ {w w′ w″} → w ≤ w′ → w′ ≤ w″ → w ≤ w″
  trans≤ (wrap η) (wrap η′) = wrap (trans⊆ η η′)

  weak≤ : ∀ {A w} → w ≤ wrap (unwrap w , A)
  weak≤ = wrap weak⊆

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

data D : Set

foo : ℕ → ℕ
foo n = n

data D where
  lam : (D → D) → D


text:
module SystemF.BigStep.Intrinsic where

open import Prelude hiding (⊥)

open import SystemF.BigStep.Types

open import Data.List hiding ([_])
open import Data.List.Any.Membership
open import Data.List.Any hiding (map)
open import Data.Fin.Substitution

-- intrinsically typed syntax for System F
infix 100 _[_]
data Term {n}(Γ : Ctx n) : Type n → Set where
  unit : Term Γ Unit
  ƛ : ∀ {b} (a : Type n) → Term (Γ +tm a) b → Term Γ (a ⇒ b)
  Λ : ∀ {a} → Term (Γ +ty) a → Term Γ (∀' a)
  _·_ : ∀ {a b} → Term Γ (a ⇒ b) → Term Γ a → Term Γ b
  _[_] : ∀ {a} → Term Γ (∀' a) → ∀ b → Term Γ (a / sub b)
  var : ∀ {a} → Var Γ a → Term Γ a

_tm/_ : ∀ {n m}{Γ : Ctx n}{a} → Term Γ a → (ρ : Sub Type n m) → Term (Γ ctx/ ρ) (a / ρ)
unit tm/ ρ = unit
ƛ a t tm/ ρ = ƛ (a / ρ) (t tm/ ρ)
Λ t tm/ ρ = Λ (subst (λ Γ → Term Γ _) (sym $ CtxLemmas.ctx/-wk-comm _ ρ) (t tm/ (ρ ↑)))
(f · e) tm/ ρ = (f tm/ ρ) · (e tm/ ρ)
(_[_] {a = a} t b) tm/ ρ =
  subst (λ a → Term _ a) (sym $ Lemmas.sub-commutes a) ((t tm/ ρ) [ b / ρ ])
var x tm/ ρ = var (Inverse.to map-∈↔ ⟨$⟩ (, (x , refl)))
  where
    open import Function.Equality
    open import Function.Inverse

module Semantics where

  Env : ∀ {n} → Ctx n → Set
  data Val {n} : Type n → Set where
    unit : Val {n} Unit
    clos  : ∀ {a b Γ} → Env Γ → Term (Γ +tm a) b → Val (a ⇒ b)
    tclos : ∀ {a Γ} → Env Γ → Term (Γ +ty) a → Val (∀' a)

  open import Data.List
  open import Data.List.All as All hiding (map)

  Env Γ = All Val Γ

  open import Category.Monad.Partiality
  open import Coinduction

  private
    open Workaround

    _⊢_⇓P : ∀ {n}{Γ : Ctx n}{a} → Env Γ → Term Γ a → (Val a) ⊥P
    C ⊢ unit ⇓P = now unit
    C ⊢ ƛ a t ⇓P = now (clos C t)
    C ⊢ Λ t ⇓P = now (tclos C t)
    C ⊢ t [ ty ] ⇓P =
      (C ⊢ t ⇓P >>= λ{
        -- We have to substitute a type into the body here
        -- and proof that weakening + substitution disappears on the context.
        -- The context lemma is computationally irrelevant, but the
        -- type-in-term substitution is not as trivially irrelevant
        (tclos C' b) → later (♯ (
         (subst Env (sym $ CtxLemmas.ctx/-wk-sub≡id _ ty) C') ⊢ b tm/ sub ty ⇓P
        ))
      })
    C ⊢ f · e ⇓P =
      (C ⊢ f ⇓P) >>= λ{
        (clos C' fb) → (C ⊢ e ⇓P) >>= λ v → later (♯ ((v ∷ C') ⊢ fb ⇓P))
      }
    C ⊢ var x ⇓P = now (lookup C x)

  -- definitional interpreter in the partiality monad
  _⊢_⇓ : ∀ {n}{Γ : Ctx n}{a} → Env Γ → Term Γ a → (Val a) ⊥
  C ⊢ t ⇓ = ⟦ C ⊢ t ⇓P ⟧P

module Example where

  open import Data.Fin renaming (zero to z; suc to s)
  open import Data.List hiding ([_])
  open import Data.List.Any
  open import Data.List.All
  open import Category.Monad.Partiality
  open Semantics

  id' : Term {0} [] (∀' (ν zero ⇒ ν zero))
  id' = Λ (ƛ (ν z) (var (here refl)))

  test = run ([] ⊢ ((id' [ Unit ]) · unit) ⇓) for 10 steps


text:
-- Andreas, 2019-08-18, issue #1346

-- Allow fixity in renaming directive, but not for modules.

module _ where

open import Agda.Builtin.Equality using ()
  renaming (module _≡_ to infix 4 _~_)

-- Expected warning:

-- Modules do not have fixity
-- when scope checking the declaration
--   open import Agda.Builtin.Equality
--     using ()
--     renaming (module _≡_ to infix 4 _~_)


text:
{-
  Copyright 2019 Lisandra Silva

  Licensed under the Apache License, Version 2.0 (the "License");
  you may not use this file except in compliance with the License.
  You may obtain a copy of the License at

      http://www.apache.org/licenses/LICENSE-2.0

  Unless required by applicable law or agreed to in writing, software
  distributed under the License is distributed on an "AS IS" BASIS,
  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  See the License for the specific language governing permissions and
  limitations under the License.
-}

open import Prelude

module StateMachineModel where

   -----------------------------------------------------------------------------
   -- State Machine
   -----------------------------------------------------------------------------
  record StateMachine (State : Set) (Event : Set) : Set₁ where
    field
      initial : Pred State 0ℓ
      enabled : Event → State → Set
      action  : ∀ {preState} {event} → enabled event preState → State
  open StateMachine

  data Reachable {State Event} {sm : StateMachine State Event} : State → Set where
    init : ∀ {s₀} → initial sm s₀
           → Reachable s₀
    step : ∀ {st event} → Reachable {sm = sm} st → (enEv : enabled sm event st)
           → Reachable (action sm enEv)

  Invariant : ∀ {State Event} (sm : StateMachine State Event) (P : Pred State 0ℓ) → Set
  Invariant sm P = ∀ {state} (rs : Reachable {sm = sm} state) → P state

  Stable : ∀ {State Event} (sm : StateMachine State Event) (P : Pred State 0ℓ) → Set
  Stable sm P = ∀ {st ev} (enEv : enabled sm ev st)
                → P st
                → P (action sm enEv)

  EventSet : ∀ {Event : Set} → Set₁
  EventSet {Event} = Pred Event 0ℓ

  record System State Event : Set₁ where
    field
      stateMachine : StateMachine State Event
      weakFairness : Pred (EventSet {Event}) 0ℓ
  open System

  enabledSet : ∀ {State Event} → StateMachine State Event
               → EventSet {Event} → State → Set
  enabledSet sm evSet state = ∃[ event ] (event ∈ evSet × enabled sm event state)

  module LeadsTo
    (State : Set) (Event : Set) (sys : System State Event)
    where

   -----------------------------------------------------------------------------
   -- HOARE Triple
   -----------------------------------------------------------------------------
   data [_]_[_] (P : Pred State 0ℓ) (event : Event) (Q : Pred State 0ℓ) : Set where
      hoare : (∀ {st} → P st
                      → (enEv : enabled (stateMachine sys) event st)
                      → Q (action (stateMachine sys) enEv ))
               → [ P ] event [ Q ]

   Z : Set
   Z = ℕ

   -- Auxiliary properties with syntax renaming for better compliance with paper
   -- TODO : Try to make this more generic
   ⋃₁ : ∀ {ℓ ℓ'} {A : Set ℓ'} → (A → Pred State ℓ) → Pred State (ℓ ⊔ ℓ')
   ⋃₁ {A = A} P = λ x → Σ[ i ∈ A ] P i x

   syntax ⋃₁ (λ i → P) = [∃ i ∶ P ]

   ⋃₂ : ∀ {ℓ₁ ℓ₂ ℓ'} {A : Set ℓ'} → (C : Pred A ℓ₁) → (F : A → Pred State ℓ₂) → Pred State _
   ⋃₂ {A = A} C F = λ s → Σ[ i ∈ A ] ( C i × F i s )

   syntax ⋃₂ C (λ x → P) = [∃ x ⇒ C ∶ P ]

   -----------------------------------------------------------------------------
   -- PROOF RULES for liveness
   -----------------------------------------------------------------------------
   infix 1 _l-t_

   data _l-t_ (P : Pred State 0ℓ) (Q : Pred State 0ℓ) : Set₁ where
     viaEvSet  :   (evSet : EventSet) → (weakFairness sys evSet)
                 → (∀ (e : Event) → e ∈ evSet → [ P ] e [ Q ])
                 → (∀ (e : Event) → ¬ (e ∈ evSet) → [ P ] e [ P ∪ Q ])
                 → Invariant (stateMachine sys)
                             (P ⇒ enabledSet (stateMachine sys) evSet)
               → P l-t Q

     viaInv    : Invariant (stateMachine sys) (P ⇒ Q)
                 → P l-t Q

     viaTrans  : ∀ {R} → P l-t R → R l-t Q
                 → P l-t Q

     viaTrans2 : ∀ {R} → P l-t (Q ∪ R) → R l-t Q
                 → P l-t Q

     viaDisj   : ∀ {P₁ P₂} → P ⊆ (P₁ ∪ P₂) → P₁ l-t Q → P₂ l-t Q
                 → P  l-t Q

     viaUseInv : ∀ {R} → Invariant (stateMachine sys) R → (P ∩ R) l-t (R ⇒ Q)
                 → P l-t Q

     viaWFR    : ∀ (F : Z → Pred State 0ℓ)
                 → P l-t (Q ∪ [∃ x ∶ F x ])
                 → (∀ (w : Z) → F w l-t (Q ∪ [∃ x ⇒ _< w ∶ F x ]))
                 → P l-t Q

     viaAllVal : ∀ {A : Set} → {R : A → Pred State 0ℓ}
                 → Invariant (stateMachine sys) [∃ x ∶ R x ]
                 → (∀ (a : A) → (P ∩ R a) l-t Q )
                 → P l-t Q

     viaStable : ∀ {P' Q' S} → Stable (stateMachine sys) S
                 → P l-t P' ∩ S → P' l-t Q' → Q' ∩ S l-t Q
                 → P l-t Q

   P⊆QQ→Inv[P⇒Q] : ∀ {P Q} {sm : StateMachine State Event}
                   → P ⊆ Q
                   → Invariant sm (P ⇒ Q)
   P⊆QQ→Inv[P⇒Q] p⊆q rs pS
     with p⊆q pS
   ... | qS = qS

   invR⇒P-l-t-P∧R : ∀ {P R} {sm : StateMachine State Event}
                    → Invariant (stateMachine sys) R
                    → P l-t P ∩ R
   invR⇒P-l-t-P∧R invR = viaInv (λ rs ps → ps , (invR rs))

max_stars_repo_name: lisandrasilva/agda-liveness

max_issues_repo_name: lisandrasilva/agda-liveness

max_forks_repo_name: lisandrasilva/agda-liveness


text:
------------------------------------------------------------------------------
-- FOTC version of the domain predicate of quicksort given by the
-- Bove-Capretta method
------------------------------------------------------------------------------

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

module FOT.FOTC.Program.QuickSort.DomainPredicate where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Nat.Inequalities hiding ( le ; gt )
open import FOTC.Data.Nat.List.Type
open import FOTC.Data.Nat.Type
open import FOTC.Data.List

------------------------------------------------------------------------------
-- We need to define monadic inequalities.
postulate
  le gt : D
  le-00 : le · zero · zero               ≡ false
  le-0S : ∀ d → le · zero · succ₁ d      ≡ true
  le-S0 : ∀ d → le · succ₁ d · zero      ≡ false
  le-SS : ∀ d e → le · succ₁ d · succ₁ e ≡ lt d e

postulate
  filter    : D → D → D
  filter-[] : ∀ f → filter f [] ≡ []
  filter-∷  : ∀ f d ds →
              filter f (d ∷ ds) ≡
              (if f · d then d ∷ filter f (d ∷ ds) else filter f (d ∷ ds))

postulate filter-List : ∀ f {xs} → List xs → List (filter f xs)

postulate
  qs    : D → D
  qs-[] : qs [] ≡ []
  qs-∷  : ∀ x xs → qs (x ∷ xs) ≡ qs (filter (gt · x) xs) ++
                                 x ∷ qs (filter (le · x) xs)

-- Domain predicate for quicksort.
data Dqs : {xs : D} → List xs → Set where
  dnil  : Dqs lnil
  dcons : ∀ {x xs} → (Lxs : List xs) →
                     Dqs (filter-List (gt · x) Lxs) →
                     Dqs (filter-List (le · x) Lxs) →
                     Dqs (lcons x Lxs)

-- Induction principle associated to the domain predicate of quicksort.
Dqs-ind : (P : {xs : D} → List xs → Set) →
          P lnil →
          (∀ {x xs} → (Lxs : List xs) →
                      Dqs (filter-List (gt · x) Lxs) →
                      P (filter-List (gt · x) Lxs) →
                      Dqs (filter-List (le · x) Lxs) →
                      P (filter-List (le · x) Lxs) →
                      P (lcons x Lxs)) →
          (∀ {xs} → {Lxs : List xs} → Dqs Lxs → P Lxs)
Dqs-ind P P[] ih dnil              = P[]
Dqs-ind P P[] ih (dcons Lxs h₁ h₂) =
  ih Lxs h₁ (Dqs-ind P P[] ih h₁) h₂ (Dqs-ind P P[] ih h₂)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

module Categories.2-Functor where

open import Level

open import Categories.Category.Monoidal.Instance.StrictCats using (module Product)
open import Categories.2-Category using (2-Category)
open import Categories.Enriched.Functor using (Functor)

2-Functor : ∀ {o ℓ e c d} →
            2-Category o ℓ e c → 2-Category o ℓ e d → Set (o ⊔ ℓ ⊔ e ⊔ c ⊔ d)
2-Functor C D = Functor (Product.Cats-Monoidal) C D

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:
{-# OPTIONS --cubical --safe #-}

module Cubical.Structures.Rng where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma

open import Cubical.Foundations.SIP renaming (SNS-PathP to SNS)

open import Cubical.Structures.NAryOp
open import Cubical.Structures.Semigroup hiding (⟨_⟩)
open import Cubical.Structures.AbGroup

private
  variable
    ℓ ℓ' : Level

raw-rng-structure : Type ℓ → Type ℓ
raw-rng-structure X = (X → X → X) × (X → X → X)

raw-rng-is-SNS : SNS {ℓ} raw-rng-structure _
raw-rng-is-SNS = join-SNS (nAryFunIso 2) (nAryFunSNS 2) (nAryFunIso 2) (nAryFunSNS 2)

rng-axioms : (X : Type ℓ) (s : raw-rng-structure X) → Type ℓ
rng-axioms X (_·_ , _+_) = abelian-group-axioms X _·_ ×
                           semigroup-axioms X _+_ ×
                           ((x y z : X) → x · (y + z) ≡ (x · y) + (x · z)) ×
                           ((x y z : X) → (x + y) · z ≡ (x · z) + (y · z))

rng-structure : Type ℓ → Type ℓ
rng-structure = add-to-structure raw-rng-structure rng-axioms

Rngs : Type (ℓ-suc ℓ)
Rngs {ℓ} = TypeWithStr ℓ rng-structure

rng-iso : StrIso rng-structure ℓ
rng-iso = add-to-iso (join-iso (nAryFunIso 2) (nAryFunIso 2)) rng-axioms

rng-axioms-isProp : (X : Type ℓ) (s : raw-rng-structure X) → isProp (rng-axioms X s)
rng-axioms-isProp X (_·_ , _+_) = isPropΣ (abelian-group-axioms-isProp X _·_)
                                  λ _ → isPropΣ (semigroup-axiom-isProp X _+_)
                                  λ { (isSetX , _) → isPropΣ (isPropΠ3 (λ _ _ _ → isSetX _ _))
                                  λ _ → isPropΠ3 (λ _ _ _ → isSetX _ _)}

rng-is-SNS : SNS {ℓ} rng-structure rng-iso
rng-is-SNS = add-axioms-SNS _ rng-axioms-isProp raw-rng-is-SNS

RngPath : (M N : Rngs {ℓ}) → (M ≃[ rng-iso ] N) ≃ (M ≡ N)
RngPath = SIP rng-is-SNS


text:
module Extensionality where

open import Relation.Binary.PropositionalEquality hiding (Extensionality)

postulate
  f-ext : {A : Set}{B : A → Set}{f : (x : A) → B x} {g : (x : A) → B x} →
    (∀ x → f x ≡ g x) → f ≡ g

max_stars_repo_name: kcaliban/ldlc

max_issues_repo_name: kcaliban/ldlc

max_forks_repo_name: kcaliban/ldlc


text:
_ : Set
_ : Set → Set


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Heterogeneous N-ary Functions: basic types and operations
------------------------------------------------------------------------

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

module Function.Nary.NonDependent.Base where

------------------------------------------------------------------------
-- Concrete examples can be found in README.Nary. This file's comments
-- are more focused on the implementation details and the motivations
-- behind the design decisions.
------------------------------------------------------------------------

open import Level using (Level; 0ℓ; _⊔_; Lift)
open import Data.Nat.Base using (ℕ; zero; suc)
open import Data.Product using (_×_; _,_)
open import Data.Unit.Base
open import Function using (_∘′_; _$′_; const; flip)

private
  variable
    a b c : Level
    A : Set a
    B : Set b
    C : Set c

------------------------------------------------------------------------
-- Type Definitions

-- We want to define n-ary function spaces and generic n-ary operations on
-- them such as (un)currying, zipWith, alignWith, etc.

-- We want users to be able to use these seamlessly whenever n is concrete.

-- In other words, we want Agda to infer the sets `A₁, ⋯, Aₙ` when we write
-- `uncurryₙ n f` where `f` has type `A₁ → ⋯ → Aₙ → B`. For this to happen,
-- we need the structure in which these Sets are stored to effectively
-- η-expand to `A₁, ⋯, Aₙ` when the parameter `n` is known.

-- Hence the following definitions:
------------------------------------------------------------------------

-- First, a "vector" of `n` Levels (defined by induction on n so that it
-- may be built by η-expansion and unification). Each Level will be that
-- of one of the Sets we want to take the n-ary product of.

Levels : ℕ → Set
Levels zero    = ⊤
Levels (suc n) = Level × Levels n

-- The overall Level of a `n` Sets of respective levels `l₁, ⋯, lₙ` will
-- be the least upper bound `l₁ ⊔ ⋯ ⊔ lₙ` of all of the Levels involved.
-- Hence the following definition of n-ary least upper bound:

⨆ : ∀ n → Levels n → Level
⨆ zero    _        = Level.zero
⨆ (suc n) (l , ls) = l ⊔ (⨆ n ls)

-- Second, a "vector" of `n` Sets whose respective Levels are determined
-- by the `Levels n` input.

Sets : ∀ n (ls : Levels n) → Set (Level.suc (⨆ n ls))
Sets zero    _        = Lift _ ⊤
Sets (suc n) (l , ls) = Set l × Sets n ls

-- Third, a function type whose domains are given by a "vector" of `n` Sets
-- `A₁, ⋯, Aₙ` and whose codomain is `B`. `Arrows` forms such a type of
-- shape `A₁ → ⋯ → Aₙ → B` by induction on `n`.

Arrows : ∀ n {r ls} → Sets n ls → Set r → Set (r ⊔ (⨆ n ls))
Arrows zero    _        b = b
Arrows (suc n) (a , as) b = a → Arrows n as b

-- We introduce a notation for this definition

infixr 0 _⇉_
_⇉_ : ∀ {n ls r} → Sets n ls → Set r → Set (r ⊔ (⨆ n ls))
_⇉_ = Arrows _

------------------------------------------------------------------------
-- Operations on Sets

-- Level-respecting map

_<$>_ : (∀ {l} → Set l → Set l) →
        ∀ {n ls} → Sets n ls → Sets n ls
_<$>_ f {zero}   as        = _
_<$>_ f {suc n}  (a , as)  = f a , f <$> as

-- Level-modifying generalised map

lmap : (Level → Level) → ∀ n → Levels n → Levels n
lmap f zero    ls       = _
lmap f (suc n) (l , ls) = f l , lmap f n ls

smap : ∀ f → (∀ {l} → Set l → Set (f l)) →
       ∀ n {ls} → Sets n ls → Sets n (lmap f n ls)
smap f F zero    as       = _
smap f F (suc n) (a , as) = F a , smap f F n as

------------------------------------------------------------------------
-- Operations on Functions

-- mapping under n arguments

mapₙ : ∀ n {ls} {as : Sets n ls} → (B → C) → as ⇉ B → as ⇉ C
mapₙ zero    f v = f v
mapₙ (suc n) f g = mapₙ n f ∘′ g

-- compose function at the n-th position

_%=_⊢_ : ∀ n {ls} {as : Sets n ls} → (A → B) → as ⇉ (B → C) → as ⇉ (A → C)
n %= f ⊢ g = mapₙ n (_∘′ f) g

-- partially apply function at the n-th position

_∷=_⊢_ : ∀ n {ls} {as : Sets n ls} → A → as ⇉ (A → B) → as ⇉ B
n ∷= x ⊢ g = mapₙ n (_$′ x) g

-- hole at the n-th position

holeₙ : ∀ n {ls} {as : Sets n ls} → (A → as ⇉ B) → as ⇉ (A → B)
holeₙ zero    f = f
holeₙ (suc n) f = holeₙ n ∘′ flip f

-- function constant in its n first arguments

-- Note that its type will only be inferred if it is used in a context
-- specifying what the type of the function ought to be. Just like the
-- usual const: there is no way to infer its domain from its argument.

constₙ : ∀ n {ls r} {as : Sets n ls} {b : Set r} → b → as ⇉ b
constₙ zero    v = v
constₙ (suc n) v = const (constₙ n v)