text:
{-# OPTIONS --cubical --safe #-}
module Subtyping where

open import Cubical.Core.Everything hiding (Type)
open import Cubical.Foundations.Prelude using (refl; sym; symP; cong; _∙_; transport; subst; transportRefl; transport-filler; toPathP; fromPathP; congP)
open import Cubical.Foundations.Transport using (transport⁻Transport)

open import Cubical.Data.Nat using (ℕ; zero; suc; _+_; +-comm; snotz; znots; +-suc; +-zero; injSuc; isSetℕ)
open import Cubical.Data.Nat.Order using (_≟_; lt; eq; gt; ≤-k+; ≤-+k; ≤-trans; pred-≤-pred; _≤_; _<_; ¬m+n<m; ¬-<-zero; suc-≤-suc; <-k+; <-+k; zero-≤; m≤n-isProp; <≤-trans; ≤-refl; <-weaken)
open import Cubical.Data.Fin using (Fin; toℕ; fzero; fsuc; Fin-fst-≡)
open import Cubical.Data.Sigma using (_×_; _,_; fst; snd; ΣPathP; Σ-cong-snd)
open import Cubical.Data.Sum using (_⊎_; inl; inr)
import Cubical.Data.Empty as Empty

open import Label using (Label; Record; nil; cons; _∈_; find; l∈r-isProp)

-- A term with at most `n` free variables.
data Term (n : ℕ) : Set where
  var : Fin n -> Term n
  abs : Term (suc n) -> Term n
  _·_ : Term n -> Term n -> Term n
  rec : forall {l} -> Record (Term n) l -> Term n
  _#_ : Term n -> Label -> Term n

shift : forall {m : ℕ} (n : ℕ) (i : Fin (suc m)) (e : Term m) -> Term (m + n)
shiftRecord : forall {m : ℕ} (n : ℕ) (i : Fin (suc m)) {l : Label} (r : Record (Term m) l) -> Record (Term (m + n)) l

shift {m} n i (var j)
  with toℕ i ≟ toℕ j
... | lt _ = var (toℕ j + n , ≤-+k (snd j))
... | eq _ = var (toℕ j + n , ≤-+k (snd j))
... | gt _ = var (toℕ j , ≤-trans (snd j) (n , +-comm n m))
shift n i (abs e) = abs (shift n (fsuc i) e)
shift n i (e · e₁) = shift n i e · shift n i e₁
shift n i (rec r) = rec (shiftRecord n i r)
shift n i (e # l) = shift n i e # l

shiftRecord n i nil = nil
shiftRecord n i (cons r l' x x₁) = cons (shiftRecord n i r) l' (shift n i x) x₁

subst′ : forall {m n : ℕ}
  -> (e' : Term m)
  -> (i : Fin (suc n))
  -> (e1 : Term (suc (n + m)))
  -> Term (n + m)
substRecord : forall {m n : ℕ}
  -> (e' : Term m)
  -> (i : Fin (suc n))
  -> forall {l : Label}
  -> (r1 : Record (Term (suc (n + m))) l)
  -> Record (Term (n + m)) l

subst′ {m} {n} e' i (var j) with toℕ j ≟ toℕ i
... | lt j<i = var (toℕ j , <≤-trans j<i (pred-≤-pred (≤-trans (snd i) (suc-≤-suc (m , +-comm m n)))))
... | eq _ = transport (λ i₁ → Term (+-comm m n i₁)) (shift n fzero e')
... | gt i<j with j
...             | zero , _        = Empty.rec (¬-<-zero i<j)
...             | suc fst₁ , snd₁ = var (fst₁ , pred-≤-pred snd₁)
subst′ e' i (abs e1) = abs (subst′ e' (fsuc i) e1)
subst′ e' i (e1 · e2) = subst′ e' i e1 · subst′ e' i e2
subst′ e' i (rec r) = rec (substRecord e' i r)
subst′ e' i (e # l) = subst′ e' i e # l

substRecord e' i nil = nil
substRecord e' i (cons r1 l' x x₁) = cons (substRecord e' i r1) l' (subst′ e' i x) x₁

infix 3 _▷_

data _▷_ {n : ℕ} : Term n -> Term n -> Set where
  beta/=> : forall {e1 : Term (suc n)} {e2 : Term n} -> abs e1 · e2 ▷ subst′ e2 fzero e1
  cong/app : forall {e1 e1' e2 : Term n} -> e1 ▷ e1' -> e1 · e2 ▷ e1' · e2

  beta/rec : forall {l'} {r : Record (Term n) l'} {l} {l∈r : l ∈ r} -> rec r # l ▷ find l r l∈r
  cong/# : forall {e e' : Term n} {l} -> e ▷ e' -> e # l  ▷ e' # l

data Base : Set where
  Unit : Base
  Int : Base

infixr 8 _=>_

data Type : Set where
  base : Base -> Type
  Top : Type
  _=>_ : Type -> Type -> Type
  rec : forall {l} -> Record Type l -> Type

data Context : ℕ -> Set where
  [] : Context 0
  _∷_ : forall {n} -> Type -> Context n -> Context (suc n)

data _[_]=_ : forall {n} -> Context n -> Fin n -> Type -> Set where
  here  : forall {n} A (G : Context n)         -> (A ∷ G) [ 0 , suc-≤-suc zero-≤ ]= A
  there : forall {n} {A} B {G : Context n} {i} -> G [ i ]= A -> (B ∷ G) [ fsuc i ]= A

lookup : forall {n} -> Context n -> Fin n -> Type
lookup [] (fst₁ , snd₁) = Empty.rec (¬-<-zero snd₁)
lookup (A ∷ G) (zero , snd₁) = A
lookup (A ∷ G) (suc fst₁ , snd₁) = lookup G (fst₁ , pred-≤-pred snd₁)

lookup-[]= : forall {n} (G : Context n) i -> G [ i ]= lookup G i
lookup-[]= [] (fst₁ , snd₁) = Empty.rec (¬-<-zero snd₁)
lookup-[]= (A ∷ G) (zero , snd₁) = subst (λ f -> (A ∷ G) [ f ]= A) (Fin-fst-≡ refl) (here A G)
lookup-[]= (A ∷ G) (suc fst₁ , snd₁) = subst (λ f -> (A ∷ G) [ f ]= lookup G (fst₁ , pred-≤-pred snd₁)) (Fin-fst-≡ refl) (there A (lookup-[]= G (fst₁ , pred-≤-pred snd₁)))

_++_ : forall {m n} -> Context m -> Context n -> Context (m + n)
[] ++ G2       = G2
(A ∷ G1) ++ G2 = A ∷ (G1 ++ G2)

++-[]= : forall {m n} {G : Context m} (G' : Context n) {j : Fin m} {A}
  -> G [ j ]= A
  -> (G' ++ G) [ n + toℕ j , <-k+ (snd j) ]= A
++-[]= [] l = subst (λ f → _ [ f ]= _) (Fin-fst-≡ refl) l
++-[]= {G = G} (C ∷ G') {A = A} l = subst (λ f → ((C ∷ G') ++ G) [ f ]= A) (Fin-fst-≡ refl) (there C (++-[]= G' l))

inserts : forall {m n} -> Fin (suc m) -> Context n -> Context m -> Context (m + n)
inserts {m} {n} (zero , snd₁) G' G   = subst Context (+-comm n m) (G' ++ G)
inserts (suc fst₁ , snd₁) G' []      = Empty.rec (¬-<-zero (pred-≤-pred snd₁))
inserts (suc fst₁ , snd₁) G' (A ∷ G) = A ∷ inserts (fst₁ , pred-≤-pred snd₁) G' G

inserts-[]=-unaffected : forall {m n} (G : Context m) (G' : Context n) {j : Fin m} (i : Fin (suc m)) {A}
  -> toℕ j < toℕ i
  -> G [ j ]= A
  -> inserts i G' G [ toℕ j , ≤-trans (snd j) (n , +-comm n m) ]= A
inserts-[]=-unaffected (A ∷ G) G' (zero , snd₁) j<i (here .A .G) = Empty.rec (¬-<-zero j<i)
inserts-[]=-unaffected (A ∷ G) G' (suc fst₁ , snd₁) j<i (here .A .G) = subst (λ f → inserts (suc fst₁ , snd₁) G' (A ∷ G) [ f ]= A) (Fin-fst-≡ refl) (here A (inserts (fst₁ , pred-≤-pred snd₁) G' G))
inserts-[]=-unaffected (B ∷ _) G' (zero , snd₁) j<i (there .B l) = Empty.rec (¬-<-zero j<i)
inserts-[]=-unaffected (B ∷ G) G' (suc fst₁ , snd₁) {A = A} j<i (there .B l) = subst (λ f → inserts (suc fst₁ , snd₁) G' (B ∷ G) [ f ]= A) (Fin-fst-≡ refl) (there B (inserts-[]=-unaffected G G' (fst₁ , pred-≤-pred snd₁) (pred-≤-pred j<i) l))

helper1 : forall m n (j : Fin m) -> PathP (λ i -> Fin (+-comm n m i)) (n + toℕ j , <-k+ (snd j)) (toℕ j + n , ≤-+k (snd j))
helper1 m n j = ΣPathP (+-comm n (toℕ j) , toPathP (m≤n-isProp _ _))

helper2 : forall m n (G : Context m) (G' : Context n) -> PathP (λ i → Context (+-comm n m i)) (G' ++ G) (subst Context (+-comm n m) (G' ++ G))
helper2 m n G G' = toPathP refl

inserts-[]=-shifted : forall {m n} (G : Context m) (G' : Context n) {j : Fin m} (i : Fin (suc m)) {A}
  -> toℕ i ≤ toℕ j
  -> G [ j ]= A
  -> inserts i G' G [ toℕ j + n , ≤-+k (snd j) ]= A
inserts-[]=-shifted {m} {n} G G' {j} (zero , snd₁) {A} i≤j l = transport (λ i -> helper2 m n G G' i [ helper1 m n j i ]= A) (++-[]= G' l)
inserts-[]=-shifted (B ∷ G) G' (suc fst₁ , snd₁) i≤j (here .B .G) = Empty.rec (¬-<-zero i≤j)
inserts-[]=-shifted (B ∷ G) G' {j = suc fst₂ , snd₂} (suc fst₁ , snd₁) {A = A} i≤j (there .B l) =
  subst (λ f → inserts (suc fst₁ , snd₁) G' (B ∷ G) [ f ]= A) (Fin-fst-≡ refl) (there B (inserts-[]=-shifted G G' (fst₁ , pred-≤-pred snd₁) (pred-≤-pred i≤j) l))

_+++_+++_ : forall {m n} -> Context m -> Type -> Context n -> Context (suc (m + n))
[] +++ A +++ G2       = A ∷ G2
(B ∷ G1) +++ A +++ G2 = B ∷ (G1 +++ A +++ G2)

++++++-[]=-unaffected : forall {m n} (G1 : Context m) (G2 : Context n) {A B} {j : Fin (suc (n + m))}
  -> (j<n : toℕ j < n)
  -> (G2 +++ A +++ G1) [ j ]= B
  -> (G2 ++ G1) [ toℕ j , <≤-trans j<n (m , +-comm m n) ]= B
++++++-[]=-unaffected G1 [] j<n l = Empty.rec (¬-<-zero j<n)
++++++-[]=-unaffected G1 (C ∷ G2) j<n (here .C .(G2 +++ _ +++ G1)) = subst (λ f -> (C ∷ (G2 ++ G1)) [ f ]= C) (Fin-fst-≡ refl) (here C (G2 ++ G1))
++++++-[]=-unaffected G1 (C ∷ G2) {B = B} j<n (there .C l) =
  let a = ++++++-[]=-unaffected G1 G2 (pred-≤-pred j<n) l
  in
  subst (λ f -> (C ∷ (G2 ++ G1)) [ f ]= B) (Fin-fst-≡ refl) (there C a)

-- Note that `j` stands for `suc fst₁`.
++++++-[]=-shifted : forall {m n} (G1 : Context m) (G2 : Context n) {A B} {fst₁ : ℕ} {snd₁ : suc (fst₁) < suc (n + m)}
  -> (n<j : n < suc fst₁)
  -> (G2 +++ A +++ G1) [ suc fst₁ , snd₁ ]= B
  -> (G2 ++ G1) [ fst₁ , pred-≤-pred snd₁ ]= B
++++++-[]=-shifted G1 [] n<j (there _ l) = subst (λ f → G1 [ f ]= _) (Fin-fst-≡ refl) l
++++++-[]=-shifted {m} {suc n} G1 (C ∷ G2) n<j (there .C {i = zero , snd₁} l) = Empty.rec (¬-<-zero (pred-≤-pred n<j))
++++++-[]=-shifted {m} {suc n} G1 (C ∷ G2) {B = B} n<j (there .C {i = suc fst₁ , snd₁} l) =
  let a = ++++++-[]=-shifted G1 G2 (pred-≤-pred n<j) l
  in
  subst (λ f → (C ∷ (G2 ++ G1)) [ f ]= B) (Fin-fst-≡ refl) (there C a)

++++++-[]=-hit : forall {m n} (G1 : Context m) (G2 : Context n) {A B} {j : Fin (suc (n + m))}
  -> toℕ j ≡ n
  -> (G2 +++ A +++ G1) [ j ]= B
  -> A ≡ B
++++++-[]=-hit G1 [] j≡n (here _ .G1) = refl
++++++-[]=-hit G1 [] j≡n (there _ l) = Empty.rec (snotz j≡n)
++++++-[]=-hit G1 (C ∷ G2) j≡n (here .C .(G2 +++ _ +++ G1)) = Empty.rec (znots j≡n)
++++++-[]=-hit G1 (C ∷ G2) j≡n (there .C l) = ++++++-[]=-hit G1 G2 (injSuc j≡n) l

infix 2 _<:_
infix 2 _<::_

data _<:_ : Type -> Type -> Set
data _<::_ {l1 l2 : Label} : Record Type l1 -> Record Type l2 -> Set

data _<:_ where
  S-Refl : forall {A} -> A <: A
  S-Arr : forall {A1 B1 A2 B2} -> A2 <: A1 -> B1 <: B2 -> A1 => B1 <: A2 => B2
  S-Top : forall {A} -> A <: Top
  S-Record : forall {l1 l2} {r1 : Record Type l1} {r2 : Record Type l2} -> r1 <:: r2 -> rec r1 <: rec r2

data _<::_ {l1} {l2} where
  S-nil : l2 ≤ l1 -> nil <:: nil

  S-cons1 : forall {l1'} {r1 : Record Type l1'} {r2 : Record Type l2} {A} {l1'<l1 : l1' < l1}
    -> r1 <:: r2
    -> cons r1 l1 A l1'<l1 <:: r2

  S-cons2 : forall {l1' l2'} {r1 : Record Type l1'} {r2 : Record Type l2'} {A B} {l1'<l1 : l1' < l1} .{l2'<l2 : l2' < l2}
    -> r1 <:: r2
    -> A <: B
    -> l1 ≡ l2
    -> cons r1 l1 A l1'<l1 <:: cons r2 l2 B l2'<l2

<::-implies-≥ : forall {l1 l2} {r1 : Record Type l1} {r2 : Record Type l2} -> r1 <:: r2 -> l2 ≤ l1
<::-implies-≥ (S-nil x) = x
<::-implies-≥ (S-cons1 {l1'<l1 = l1'<l1} s) = ≤-trans (<::-implies-≥ s) (<-weaken l1'<l1)
<::-implies-≥ (S-cons2 s x x₁) = 0 , sym x₁

helper/<::-∈ : forall {l1 l2} {r1 : Record Type l1} {r2 : Record Type l2}
  -> r1 <:: r2
  -> forall {l}
  -> l ∈ r2
  -> l ∈ r1
helper/<::-∈ (S-cons1 {l1'<l1 = l1'<l1} s) l∈r2 = _∈_.there {lt = l1'<l1} (helper/<::-∈ s l∈r2)
helper/<::-∈ (S-cons2 {r1 = r1} {A = A} {l1'<l1 = l1'<l1} _ x l1≡l2) (_∈_.here {lt = a} e) = transport (λ i -> (l1≡l2 ∙ sym e) i ∈ cons r1 _ A l1'<l1) (_∈_.here {lt = l1'<l1} refl)
helper/<::-∈ (S-cons2 {l1'<l1 = l1'<l1} s x l1≡l2) (_∈_.there l∈r2) = _∈_.there {lt = l1'<l1} (helper/<::-∈ s l∈r2)

infix 2 _⊢_::_
infix 2 _⊢_:::_

data _⊢_::_ {n : ℕ} (G : Context n) : Term n -> Type -> Set
data _⊢_:::_ {n : ℕ} (G : Context n) {l} : Record (Term n) l -> Record Type l -> Set

data _⊢_::_ {n} G where
  axiom : forall {i : Fin n} {A}
    -> G [ i ]= A
    -> G ⊢ var i :: A

  =>I : forall {A B : Type} {e : Term (suc n)}
    -> A ∷ G ⊢ e :: B
    -> G ⊢ abs e :: A => B

  =>E : forall {A B : Type} {e1 e2 : Term n}
    -> G ⊢ e1 :: A => B
    -> G ⊢ e2 :: A
    -> G ⊢ e1 · e2 :: B

  recI : forall {l} {r : Record (Term n) l} {rt : Record Type l}
    -> G ⊢ r ::: rt
    -> G ⊢ rec r :: rec rt

  recE : forall {l'} {r : Record Type l'} {e : Term n} {l : Label}
    -> G ⊢ e :: rec r
    -> (l∈r : l ∈ r)
    -> G ⊢ e # l :: find l r l∈r

  sub : forall {A B : Type} {e}
    -> G ⊢ e :: A
    -> A <: B
    -> G ⊢ e :: B

data _⊢_:::_ {n} G {l} where
  rec/nil : G ⊢ nil ::: nil

  rec/cons : forall {l'} {r : Record (Term n) l'} {rt : Record Type l'} {e A} .{l'<l : (l' < l)}
    -> G ⊢ r ::: rt
    -> G ⊢ e :: A
    -> G ⊢ cons r l e l'<l ::: cons rt l A l'<l

helper/∈ : forall {n} {G : Context n} {l} {r : Record (Term n) l} {rt : Record Type l}
  -> G ⊢ r ::: rt
  -> forall {l₁}
  -> l₁ ∈ r
  -> l₁ ∈ rt
helper/∈ (rec/cons D x) (_∈_.here {lt = y} e) = _∈_.here {lt = y} e
helper/∈ (rec/cons D x) (_∈_.there {lt = y} l₁∈r) = _∈_.there {lt = y} (helper/∈ D l₁∈r)

helper/∈′ : forall {n} {G : Context n} {l} {r : Record (Term n) l} {rt : Record Type l}
  -> G ⊢ r ::: rt
  -> forall {l₁}
  -> l₁ ∈ rt
  -> l₁ ∈ r
helper/∈′ (rec/cons D x) (_∈_.here {lt = y} e) = _∈_.here {lt = y} e
helper/∈′ (rec/cons D x) (_∈_.there {lt = y} l₁∈r) = _∈_.there {lt = y} (helper/∈′ D l₁∈r)

weakening : forall {m n} (i : Fin (suc m)) {G : Context m} (G' : Context n) {e : Term m} {A}
  -> G ⊢ e :: A
  -> inserts i G' G ⊢ shift n i e :: A
weakeningRecord : forall {m n} (i : Fin (suc m)) {G : Context m} (G' : Context n) {l} {r : Record (Term m) l} {rt}
  -> G ⊢ r ::: rt
  -> inserts i G' G ⊢ shiftRecord n i r ::: rt

weakening {m = m} {n = n} i {G = G} G' {e = var j} (axiom l)
  with toℕ i ≟ toℕ j
... | lt i<j = axiom (inserts-[]=-shifted G G' i (≤-trans (1 , refl) i<j) l)
... | eq i≡j = axiom (inserts-[]=-shifted G G' i (0 , i≡j) l)
... | gt j<i = axiom (inserts-[]=-unaffected G G' i j<i l)
weakening {n = n} i {G = G} G' {e = abs e} {A = A => B} (=>I D) =
  =>I (subst (λ f -> (A ∷ inserts f G' G) ⊢ shift n (fsuc i) e :: B) (Fin-fst-≡ {j = i} refl) (weakening (fsuc i) G' D))
weakening i G' (=>E D D₁) = =>E (weakening i G' D) (weakening i G' D₁)
weakening i G' (sub D s) = sub (weakening i G' D) s
weakening i G' (recI D) = recI (weakeningRecord i G' D)
weakening i G' (recE D l∈r) = recE (weakening i G' D) l∈r

weakeningRecord i G' rec/nil = rec/nil
weakeningRecord i G' (rec/cons x x₁) = rec/cons (weakeningRecord i G' x) (weakening i G' x₁)

helper3 : forall {n} -> (suc n , ≤-refl) ≡ (suc n , suc-≤-suc ≤-refl)
helper3 = Fin-fst-≡ refl

helper4 : forall m n (j : Fin (suc (n + m))) j<n
  -> (toℕ j , <≤-trans j<n (m , +-comm m n)) ≡ (toℕ j , <≤-trans j<n (pred-≤-pred (≤-trans (0 , refl) (suc-≤-suc (m , +-comm m n)))))
helper4 m n j j<n = Fin-fst-≡ refl

helper5 : forall m n (G1 : Context m) (G2 : Context n)
  -> PathP (λ i -> Context (+-comm n m (~ i))) (subst Context (+-comm n m) (G2 ++ G1)) (G2 ++ G1)
helper5 m n G1 G2 = symP {A = λ i -> Context (+-comm n m i)} (toPathP refl)

helper6 : forall m n (e : Term (m + n))
  -> PathP (λ i -> Term (+-comm m n i)) e (transport (λ i -> Term (+-comm m n i)) e)
helper6 m n e = toPathP refl

helper' : forall m n -> +-comm m n ≡ sym (+-comm n m)
helper' m n = isSetℕ (m + n) (n + m) (+-comm m n) (sym (+-comm n m))

helper7 : forall m n (e : Term (m + n))
  -> PathP (λ i -> Term (+-comm n m (~ i))) e (transport (λ i -> Term (+-comm m n i)) e)
helper7 m n e = subst (λ m+n≡n+m → PathP (λ i → Term (m+n≡n+m i)) e (transport (λ i -> Term (+-comm m n i)) e)) (helper' m n) (helper6 m n e)

substitution : forall {m n} (G1 : Context m) (G2 : Context n) (e1 : Term (suc (n + m))) {e2 : Term m} {A B}
  -> G1 ⊢ e2 :: A
  -> G2 +++ A +++ G1 ⊢ e1 :: B
  -> G2 ++ G1 ⊢ subst′ e2 (n , ≤-refl) e1 :: B
substitutionRecord : forall {m n} (G1 : Context m) (G2 : Context n) {l} (r : Record (Term (suc (n + m))) l) {e2 : Term m} {A} {rt}
  -> G1 ⊢ e2 :: A
  -> G2 +++ A +++ G1 ⊢ r ::: rt
  -> G2 ++ G1 ⊢ substRecord e2 (n , ≤-refl) r ::: rt

substitution G1 G2 e1 D' (sub D s) = sub (substitution G1 G2 e1 D' D) s
substitution {m} {n} G1 G2 (var j) {e2 = e2} {B = B} D' (axiom l) with toℕ j ≟ toℕ (n , ≤-refl)
... | lt j<n = axiom (transport (λ i -> (G2 ++ G1) [ helper4 m n j j<n i ]= B) (++++++-[]=-unaffected G1 G2 j<n l))
... | eq j≡n = let a = weakening fzero G2 D' in transport (λ i → helper5 m n G1 G2 i ⊢ helper7 m n (shift n fzero e2) i :: ++++++-[]=-hit G1 G2 j≡n l i ) a
... | gt n<j with j
...             | zero , snd₁ = Empty.rec (¬-<-zero n<j)
...             | suc fst₁ , snd₁ = axiom (++++++-[]=-shifted G1 G2 n<j l)
substitution G1 G2 (abs e1) {e2 = e2} D' (=>I {A} {B} D) = =>I (transport (λ i → (A ∷ (G2 ++ G1)) ⊢ subst′ e2 (helper3 i) e1 :: B) (substitution G1 (A ∷ G2) e1 D' D))
substitution G1 G2 (e · e') D' (=>E D D₁) = =>E (substitution G1 G2 e D' D) (substitution G1 G2 e' D' D₁)
substitution G1 G2 (rec r) D' (recI D) = recI (substitutionRecord G1 G2 r D' D)
substitution G1 G2 (e # l) D' (recE D l∈r) = recE (substitution G1 G2 e D' D) l∈r

substitutionRecord G1 G2 nil D' rec/nil = rec/nil
substitutionRecord G1 G2 (cons r l e _) D' (rec/cons D x) = rec/cons (substitutionRecord G1 G2 r D' D) (substitution G1 G2 e D' x)

S-Trans : forall {A B C}
  -> A <: B
  -> B <: C
  -> A <: C
S-TransRecord : forall {l1 l2 l3} {r1 : Record Type l1} {r2 : Record Type l2} {r3 : Record Type l3}
  -> r1 <:: r2
  -> r2 <:: r3
  -> r1 <:: r3

S-Trans S-Refl s2 = s2
S-Trans (S-Arr s1 s3) S-Refl = S-Arr s1 s3
S-Trans (S-Arr s1 s3) (S-Arr s2 s4) = S-Arr (S-Trans s2 s1) (S-Trans s3 s4)
S-Trans (S-Arr s1 s3) S-Top = S-Top
S-Trans S-Top S-Refl = S-Top
S-Trans S-Top S-Top = S-Top
S-Trans (S-Record s1) S-Refl = S-Record s1
S-Trans (S-Record s1) S-Top = S-Top
S-Trans (S-Record s1) (S-Record s2) = S-Record (S-TransRecord s1 s2)

S-TransRecord (S-nil x) (S-nil y) = S-nil (≤-trans y x)
S-TransRecord (S-cons1 {l1'<l1 = l1'<l1} x) x₁ = S-cons1 {l1'<l1 = l1'<l1} (S-TransRecord x x₁)
S-TransRecord (S-cons2 {l1'<l1 = a} x x₂ _) (S-cons1 x₁) = S-cons1 {l1'<l1 = a} (S-TransRecord x x₁)
S-TransRecord (S-cons2 {l1'<l1 = a} x x₂ l1≡l2) (S-cons2 x₁ x₃ l2≡l3) = S-cons2 {l1'<l1 = a} (S-TransRecord x x₁) (S-Trans x₂ x₃) (l1≡l2 ∙ l2≡l3)

inversion/S-Arr : forall {A1 B1 A2 B2}
  -> A1 => B1 <: A2 => B2
  -> (A2 <: A1) × (B1 <: B2)
inversion/S-Arr S-Refl = S-Refl , S-Refl
inversion/S-Arr (S-Arr s s₁) = s , s₁

helper/inversion/S-Record : forall {l1 l2} {r1 : Record Type l1} {r2 : Record Type l2}
  -> (s : r1 <:: r2)
  -> forall {l}
  -> (l∈r2 : l ∈ r2)
  -> find l r1 (helper/<::-∈ s l∈r2) <: find l r2 l∈r2
helper/inversion/S-Record (S-cons1 s) l∈r2 = helper/inversion/S-Record s l∈r2
helper/inversion/S-Record {l1} {r1 = cons r1 l1 A k} (S-cons2 {B = B} {l1'<l1 = l1'<l1} _ x l1≡l2) {l = l} (_∈_.here {lt = u} e) =
  subst (λ z -> find l (cons r1 l1 A k) z <: B) (l∈r-isProp l (cons r1 l1 A k) (_∈_.here {lt = l1'<l1} (e ∙ sym l1≡l2)) (transport (λ i → (l1≡l2 ∙ sym e) i ∈ cons r1 l1 A k) (_∈_.here refl))) x
helper/inversion/S-Record (S-cons2 s x x₁) (_∈_.there l∈r2) = helper/inversion/S-Record s l∈r2

inversion/S-Record : forall {l1 l2} {r1 : Record Type l1} {r2 : Record Type l2}
  -> rec r1 <: rec r2
  -> forall {l} (l∈r2 : l ∈ r2) -> Σ[ l∈r1 ∈ (l ∈ r1) ] (find l r1 l∈r1 <: find l r2 l∈r2)
inversion/S-Record S-Refl l∈r2 = l∈r2 , S-Refl
inversion/S-Record (S-Record s) l∈r2 = helper/<::-∈ s l∈r2 , helper/inversion/S-Record s l∈r2

inversion/=>I : forall {n} {G : Context n} {e : Term (suc n)} {A}
  -> G ⊢ abs e :: A
  -> Σ[ B ∈ Type ] Σ[ C ∈ Type ] ((B ∷ G ⊢ e :: C)  ×  (B => C <: A))
inversion/=>I (=>I D) = _ , _ , D , S-Refl
inversion/=>I (sub D s)
  with inversion/=>I D
... | B , C , D' , s' = B , C , D' , S-Trans s' s

helper/inversion/recI : forall {n} {G : Context n} {l} {r : Record (Term n) l} {rt : Record Type l}
  -> (D : G ⊢ r ::: rt)
  -> forall {l₁}
  -> (l₁∈r : l₁ ∈ r)
  -> G ⊢ find l₁ r l₁∈r :: find l₁ rt (helper/∈ D l₁∈r)
helper/inversion/recI (rec/cons D x) (_∈_.here e) = x
helper/inversion/recI (rec/cons D x) (_∈_.there l₁∈r) = helper/inversion/recI D l₁∈r

inversion/recI : forall {n} {G : Context n} {l} {r : Record (Term n) l} {A}
  -> G ⊢ rec r :: A
  -> Σ[ rt ∈ Record Type l ] Σ[ f ∈ (forall {l₁} -> l₁ ∈ r -> l₁ ∈ rt) ] Σ[ g ∈ (forall {l₁} -> l₁ ∈ rt -> l₁ ∈ r) ] ((forall {l₁} (l₁∈r : l₁ ∈ r) -> (G ⊢ find l₁ r l₁∈r :: find l₁ rt (f l₁∈r)))  ×  (rec rt <: A))
inversion/recI (recI D) = _ , helper/∈ D , helper/∈′ D , (helper/inversion/recI D) , S-Refl
inversion/recI (sub D s)
  with inversion/recI D
... | rt , f , g , x , s' = rt , f , g , x , S-Trans s' s

preservation : forall {n} {G : Context n} (e : Term n) {e' : Term n} {A}
  -> G ⊢ e :: A
  -> e ▷ e'
  -> G ⊢ e' :: A
preservation e (sub D s) st = sub (preservation e D st) s
preservation (_ · _) (=>E D D₁) (cong/app s) = =>E (preservation _ D s) D₁
preservation {G = G} (abs e1 · e2) (=>E D D₁) beta/=>
  with inversion/=>I D
... | _ , _ , D , s with inversion/S-Arr s
... | sdom , scod = substitution G [] e1 (sub D₁ sdom) (sub D scod)
preservation (e # l) (recE D l∈r) (cong/# s) = recE (preservation e D s) l∈r
preservation {G = G} (rec r # l) (recE D l∈r) (beta/rec {l∈r = l∈r′})
  with inversion/recI D
...  | rt , f , _ , x , s with inversion/S-Record s
...  | sr = let a = x l∈r′ in let l∈rt , b = sr l∈r in sub (subst (λ z -> G ⊢ find l r l∈r′ :: find l rt z) (l∈r-isProp l rt (f l∈r′) (l∈rt)) a) b

-- Path.
data P {n : ℕ} : Term n -> Set where
  var : forall {i : Fin n} -> P (var i)
  app : forall {e1 e2 : Term n} -> P e1 -> P (e1 · e2)
  proj : forall {e} {l} -> P e -> P (e # l)

data Whnf {n : ℕ} : Term n -> Set where
  `_ : forall {p : Term n} -> P p -> Whnf p
  abs : forall {e : Term (suc n)} -> Whnf (abs e)
  rec : forall {l} {r : Record (Term n) l} -> Whnf (rec r)

=>Whnf : forall {n} {G : Context n} {e : Term n} {A B : Type}
  -> G ⊢ e :: A => B
  -> Whnf e
  -> P e ⊎ (Σ[ e' ∈ Term (suc n) ] e ≡ abs e')
=>Whnf {e = var x} D (` x₁) = inl x₁
=>Whnf {e = abs e} D abs = inr (e , refl)
=>Whnf {e = e · e₁} D (` x) = inl x
=>Whnf {e = rec x} D w
  with inversion/recI D
... | ()
=>Whnf {e = e # x} D (` x₁) = inl x₁

recWhnf : forall {n} {G : Context n} {e : Term n} {l} {rt : Record Type l}
  -> G ⊢ e :: rec rt
  -> Whnf e
  -> P e ⊎ (Σ[ l' ∈ Label ] Σ[ r ∈ Record (Term n) l' ] e ≡ rec r)
recWhnf {e = var x} D (` x₁) = inl x₁
recWhnf {e = abs e} D w
  with inversion/=>I D
... | ()
recWhnf {e = e · e₁} D (` x) = inl x
recWhnf {e = rec x} D rec = inr (_ , x , refl)
recWhnf {e = e # x} D (` x₁) = inl x₁

helper/progress : forall {n} {G : Context n} {l1 l2} {r : Record _ l1} {rt : Record _ l2}
  -> G ⊢ rec r :: rec rt
  -> forall {l}
  -> l ∈ rt
  -> l ∈ r
helper/progress D l∈rt
  with inversion/recI D
... | rt0 , f , g , x , s with inversion/S-Record s l∈rt
... | l∈rt0 , s' = g l∈rt0

progress : forall {n} {G : Context n} {e : Term n} {A}
  -> G ⊢ e :: A
  -> (Σ[ e' ∈ Term n ] e ▷ e') ⊎ Whnf e
progress (axiom x) = inr (` var)
progress (=>I D) = inr abs
progress {n} {e = e1 · e2} (=>E D D₁) with progress D
... | inl (e1' , s) = inl ((e1' · e2) , cong/app s)
... | inr w with =>Whnf D w
... | inl p = inr (` app p)
... | inr (e1 , x) = inl (transport (Σ-cong-snd λ x₁ i → (x (~ i) · e2) ▷ x₁) (subst′ e2 fzero e1 , beta/=>))
progress (sub D _) = progress D
progress (recI D) = inr rec
progress {G = G} {e = e # l} (recE D l∈r) with progress D
... | inl (e' , s) = inl ((e' # l) , cong/# s)
... | inr w with recWhnf D w
... | inl p = inr (` proj p)
... | inr (l' , r , x) = inl (transport (Σ-cong-snd λ x₁ i → x (~ i) # l ▷ x₁) (find l r (helper/progress (subst (λ x₁ → G ⊢ x₁ :: _) x D) l∈r) , beta/rec))

max_stars_repo_name: elpinal/subtyping-agda

max_issues_repo_name: elpinal/subtyping-agda

max_forks_repo_name: elpinal/subtyping-agda


text:
postulate
  I : Set
  D : I → Set
  T : Set

record R : Set where
  field
    t0   : T
    {i0} : I
    t1   : T
    d0   : D i0
    {i1} : I
    d1   : D i1
    t2   : T

module M0 where
  postulate
    t0 t1 : T

module MI where
  postulate
    i1 : I
    d1 : D i1

module MD {i0 : I} where
  postulate
    d0 : D i0
    t0 : T

r : R
r = record { M0; t2 = M0.t0; MD; MI; i0 = i0 }
  module My where postulate i0 : I

r' : R
r' = record { R r; t0 = R.t1 r }
  where module Rr = R r

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Functions.Definition

module Orders.WellFounded.Definition {a b : _} {A : Set a} (_<_ : Rel {a} {b} A) where

data Accessible (x : A) : Set (lsuc a ⊔ b) where
  access : (∀ y → y < x → Accessible y) → Accessible x

WellFounded : Set (lsuc a ⊔ b)
WellFounded = ∀ x → Accessible x


text:
------------------------------------------------------------------------------
-- Quicksort using the Bove-Capretta method
------------------------------------------------------------------------------

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

module FOT.FOTC.Program.QuickSort.QuickSortBC where

open import Data.List.Base
open import Data.Nat.Base
open import Data.Nat.Properties

open import Induction
open import Induction.Nat
open import Induction.WellFounded

open import Level

open import Relation.Unary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

module InvImg =
  Induction.WellFounded.Inverse-image {A = List ℕ} {ℕ} {_<′_} length

------------------------------------------------------------------------------

-- Non-terminating quicksort.

{-# TERMINATING #-}
qsNT : List ℕ → List ℕ
qsNT []       = []
qsNT (x ∷ xs) = qsNT (filter (λ y → y ≤′? x) xs) ++
                x ∷ qsNT (filter (λ y → x ≤′? y) xs)

-- Domain predicate for quicksort.
data QSDom : List ℕ → Set where
  qsDom-[] : QSDom []
  qsDom-∷  : ∀ {x xs} →
             (QSDom (filter (λ y → y ≤′? x) xs)) →
             (QSDom (filter (λ y → x ≤′? y) xs)) →
             QSDom (x ∷ xs)

-- Induction principle associated to the domain predicate of quicksort.
-- (It was not necessary).
QSDom-ind : (P : List ℕ → Set) →
            P [] →
            (∀ {x xs} → QSDom (filter (λ y → y ≤′? x) xs) →
                        P (filter (λ y → y ≤′? x) xs) →
                        QSDom (filter (λ y → x ≤′? y) xs) →
                        P (filter (λ y → x ≤′? y) xs) →
                        P (x ∷ xs)) →
            (∀ {xs} → QSDom xs → P xs)
QSDom-ind P P[] ih qsDom-[]        = P[]
QSDom-ind P P[] ih (qsDom-∷ h₁ h₂) =
  ih h₁ (QSDom-ind P P[] ih h₁) h₂ (QSDom-ind P P[] ih h₂)

-- Well-founded relation on lists.
_⟪′_ : {A : Set} → List A → List A → Set
xs ⟪′ ys = length xs <′ length ys

wf-⟪′ : WellFounded _⟪′_
wf-⟪′ = InvImg.well-founded <′-wellFounded

-- The well-founded induction principle on _⟪′_.
-- postulate wfi-⟪′ : (P : List ℕ → Set) →
--                    (∀ xs → (∀ ys → ys ⟪′ xs → P ys) → P xs) →
--                    ∀ xs → P xs

-- The quicksort algorithm is total.

filter-length : {A : Set} {P : Pred A Level.zero} →
                (P? : Relation.Unary.Decidable P ) → ∀ xs → length (filter P? xs) ≤′ length xs
filter-length P? [] = ≤′-refl
filter-length P? (x ∷ xs) with P? x
... | yes _ = ≤⇒≤′ (s≤s (≤′⇒≤ (filter-length P? xs)))
... | no  _ = ≤′-step (filter-length P? xs)

module AllWF = Induction.WellFounded.All wf-⟪′

allQSDom : ∀ xs → QSDom xs
-- If we use wfi-⟪′ then allQSDom =  wfi-⟪′ P ih
allQSDom = build (AllWF.wfRec-builder _) P ih
  where
  P : List ℕ → Set
  P = QSDom

  -- If we use wfi-⟪′ then
  -- ih : ∀ zs → (∀ ys → ys ⟪′ zs → P ys) → P zs
  ih :  ∀ zs → WfRec _⟪′_ P zs → P zs
  ih []       h = qsDom-[]
  ih (z ∷ zs) h = qsDom-∷ prf₁ prf₂
    where
    c₁ : (y : ℕ) → Dec (y ≤′ z)
    c₁ y = y ≤′? z

    c₂ : (y : ℕ) → Dec (z ≤′ y)
    c₂ y = z ≤′? y

    f₁ : List ℕ
    f₁ = filter c₁ zs

    f₂ : List ℕ
    f₂ = filter c₂ zs

    prf₁ : QSDom (filter (λ y → y ≤′? z) zs)
    prf₁ = h f₁ (≤⇒≤′ (s≤s (≤′⇒≤ (filter-length c₁ zs))))

    prf₂ : QSDom (filter (λ y → z ≤′? y) zs)
    prf₂ = h f₂ (≤⇒≤′ (s≤s (≤′⇒≤ (filter-length c₂ zs))))

-- Quicksort algorithm by structural recursion on the domain predicate.
qsDom : ∀ xs → QSDom xs → List ℕ
qsDom .[]      qsDom-[]        = []
qsDom (x ∷ xs) (qsDom-∷ h₁ h₂) =
  qsDom (filter (λ y → y ≤′? x) xs) h₁ ++
  x ∷ qsDom (filter (λ y → x ≤′? y) xs) h₂

-- The quicksort algorithm.
qs : List ℕ → List ℕ
qs xs = qsDom xs (allQSDom xs)

-- Testing.
l₁ : List ℕ
l₁ = []
l₂ = 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ []
l₃ = 5 ∷ 4 ∷ 3 ∷ 2 ∷ 1 ∷ []
l₄ = 4 ∷ 1 ∷ 3 ∷ 5 ∷ 2 ∷ []

t₁ : qs l₁ ≡ l₁
t₁ = refl

t₂ : qs l₂ ≡ l₂
t₂ = refl

t₃ : qs l₃ ≡ l₂
t₃ = refl

t₄ : qs l₄ ≡ l₂
t₄ = refl

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------------
-- Totality properties respect to Tree
------------------------------------------------------------------------------

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

module FOTC.Program.SortList.Properties.Totality.TreeI where

open import FOTC.Base
open import FOTC.Data.Nat.List.Type
open import FOTC.Data.Nat.Type
open import FOTC.Program.SortList.SortList

------------------------------------------------------------------------------
-- See the ATP version.
postulate toTree-Tree : ∀ {item t} → N item → Tree t → Tree (toTree · item · t)

makeTree-Tree : ∀ {is} → ListN is → Tree (makeTree is)
makeTree-Tree lnnil = subst Tree (sym (lit-[] toTree nil)) tnil
makeTree-Tree (lncons {i} {is} Ni LNis) =
  subst Tree
        (sym (lit-∷ toTree i is nil))
        (toTree-Tree Ni (makeTree-Tree LNis))


text:
{-

Theory about equivalences

Definitions are in Core/Glue.agda but re-exported by this module

- isEquiv is a proposition ([isPropIsEquiv])
- Any isomorphism is an equivalence ([isoToEquiv])

There are more statements about equivalences in Equiv/Properties.agda:

- if f is an equivalence then (cong f) is an equivalence
- if f is an equivalence then precomposition with f is an equivalence
- if f is an equivalence then postcomposition with f is an equivalence

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Foundations.Equiv where

open import Cubical.Foundations.Function
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws

open import Cubical.Foundations.Equiv.Base public
open import Cubical.Data.Sigma.Base

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

equivIsEquiv : (e : A ≃ B) → isEquiv (equivFun e)
equivIsEquiv e = snd e

equivCtr : (e : A ≃ B) (y : B) → fiber (equivFun e) y
equivCtr e y = e .snd .equiv-proof y .fst

equivCtrPath : (e : A ≃ B) (y : B) →
  (v : fiber (equivFun e) y) → Path _ (equivCtr e y) v
equivCtrPath e y = e .snd .equiv-proof y .snd

-- Proof using isPropIsContr. This is slow and the direct proof below is better

isPropIsEquiv' : (f : A → B) → isProp (isEquiv f)
equiv-proof (isPropIsEquiv' f u0 u1 i) y =
  isPropIsContr (u0 .equiv-proof y) (u1 .equiv-proof y) i

-- Direct proof that computes quite ok (can be optimized further if
-- necessary, see:
-- https://github.com/mortberg/cubicaltt/blob/pi4s3_dimclosures/examples/brunerie2.ctt#L562

isPropIsEquiv : (f : A → B) → isProp (isEquiv f)
equiv-proof (isPropIsEquiv f p q i) y =
  let p2 = p .equiv-proof y .snd
      q2 = q .equiv-proof y .snd
  in p2 (q .equiv-proof y .fst) i
   , λ w j → hcomp (λ k → λ { (i = i0) → p2 w j
                            ; (i = i1) → q2 w (j ∨ ~ k)
                            ; (j = i0) → p2 (q2 w (~ k)) i
                            ; (j = i1) → w })
                   (p2 w (i ∨ j))

equivEq : {e f : A ≃ B} → (h : e .fst ≡ f .fst) → e ≡ f
equivEq {e = e} {f = f} h = λ i → (h i) , isProp→PathP (λ i → isPropIsEquiv (h i)) (e .snd) (f .snd) i

module _ {f : A → B} (equivF : isEquiv f) where
  funIsEq : A → B
  funIsEq = f

  invIsEq : B → A
  invIsEq y = equivF .equiv-proof y .fst .fst

  secIsEq : section f invIsEq
  secIsEq y = equivF .equiv-proof y .fst .snd

  retIsEq : retract f invIsEq
  retIsEq a i = equivF .equiv-proof (f a) .snd (a , refl) i .fst

  commSqIsEq : ∀ a → Square (secIsEq (f a)) refl (cong f (retIsEq a)) refl
  commSqIsEq a i = equivF .equiv-proof (f a) .snd (a , refl) i .snd

module _ (w : A ≃ B) where
  invEq : B → A
  invEq = invIsEq (snd w)

  secEq : section invEq (w .fst)
  secEq = retIsEq (snd w)

  retEq : retract invEq (w .fst)
  retEq = secIsEq (snd w)

open Iso

equivToIso : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → A ≃ B → Iso A B
fun (equivToIso e) = e .fst
inv (equivToIso e) = invEq e
rightInv (equivToIso e) = retEq e
leftInv (equivToIso e)  = secEq e

-- TODO: there should be a direct proof of this that doesn't use equivToIso
invEquiv : A ≃ B → B ≃ A
invEquiv e = isoToEquiv (invIso (equivToIso e))

invEquivIdEquiv : (A : Type ℓ) → invEquiv (idEquiv A) ≡ idEquiv A
invEquivIdEquiv _ = equivEq refl

-- TODO: there should be a direct proof of this that doesn't use equivToIso
compEquiv : A ≃ B → B ≃ C → A ≃ C
compEquiv f g = isoToEquiv (compIso (equivToIso f) (equivToIso g))

compEquivIdEquiv : (e : A ≃ B) → compEquiv (idEquiv A) e ≡ e
compEquivIdEquiv e = equivEq refl

compEquivEquivId : (e : A ≃ B) → compEquiv e (idEquiv B) ≡ e
compEquivEquivId e = equivEq refl

invEquiv-is-rinv : (e : A ≃ B) → compEquiv e (invEquiv e) ≡ idEquiv A
invEquiv-is-rinv e = equivEq (funExt (secEq e))

invEquiv-is-linv : (e : A ≃ B) → compEquiv (invEquiv e) e ≡ idEquiv B
invEquiv-is-linv e = equivEq (funExt (retEq e))

compEquiv-assoc : (f : A ≃ B) (g : B ≃ C) (h : C ≃ D)
                → compEquiv f (compEquiv g h) ≡ compEquiv (compEquiv f g) h
compEquiv-assoc f g h = equivEq refl

LiftEquiv : A ≃ Lift {i = ℓ} {j = ℓ'} A
LiftEquiv .fst a .lower = a
LiftEquiv .snd .equiv-proof = strictContrFibers lower

Lift≃Lift : (e : A ≃ B) → Lift {j = ℓ'} A ≃ Lift {j = ℓ''} B
Lift≃Lift e .fst a .lower = e .fst (a .lower)
Lift≃Lift e .snd .equiv-proof b .fst .fst .lower = invEq e (b .lower)
Lift≃Lift e .snd .equiv-proof b .fst .snd i .lower =
  e .snd .equiv-proof (b .lower) .fst .snd i
Lift≃Lift e .snd .equiv-proof b .snd (a , p) i .fst .lower =
  e .snd .equiv-proof (b .lower) .snd (a .lower , cong lower p) i .fst
Lift≃Lift e .snd .equiv-proof b .snd (a , p) i .snd j .lower =
  e .snd .equiv-proof (b .lower) .snd (a .lower , cong lower p) i .snd j

isContr→Equiv : isContr A → isContr B → A ≃ B
isContr→Equiv Actr Bctr = isoToEquiv (isContr→Iso Actr Bctr)

propBiimpl→Equiv : (Aprop : isProp A) (Bprop : isProp B) (f : A → B) (g : B → A) → A ≃ B
propBiimpl→Equiv Aprop Bprop f g = f , hf
  where
  hf : isEquiv f
  hf .equiv-proof y .fst          = (g y , Bprop (f (g y)) y)
  hf .equiv-proof y .snd h i .fst = Aprop (g y) (h .fst) i
  hf .equiv-proof y .snd h i .snd = isProp→isSet' Bprop (Bprop (f (g y)) y) (h .snd)
                                                  (cong f (Aprop (g y) (h .fst))) refl i

isEquivPropBiimpl→Equiv : isProp A → isProp B
                        → ((A → B) × (B → A)) ≃ (A ≃ B)
isEquivPropBiimpl→Equiv {A = A} {B = B} Aprop Bprop = isoToEquiv isom where
  isom : Iso (Σ (A → B) (λ _ → B → A)) (A ≃ B)
  isom .fun (f , g) = propBiimpl→Equiv Aprop Bprop f g
  isom .inv e = equivFun e , invEq e
  isom .rightInv e = equivEq refl
  isom .leftInv _ = refl

equivΠCod : ∀ {F : A → Type ℓ} {G : A → Type ℓ'}
        → ((x : A) → F x ≃ G x) → ((x : A) → F x) ≃ ((x : A) → G x)
equivΠCod k .fst f x = k x .fst (f x)
equivΠCod k .snd .equiv-proof f .fst .fst x   = equivCtr (k x) (f x) .fst
equivΠCod k .snd .equiv-proof f .fst .snd i x = equivCtr (k x) (f x) .snd i
equivΠCod k .snd .equiv-proof f .snd (g , p) i .fst x =
  equivCtrPath (k x) (f x) (g x , λ j → p j x) i .fst
equivΠCod k .snd .equiv-proof f .snd (g , p) i .snd j x =
  equivCtrPath (k x) (f x) (g x , λ k → p k x) i .snd j

equivImplicitΠCod : ∀ {F : A → Type ℓ} {G : A → Type ℓ'}
        → ({x : A} → F x ≃ G x) → ({x : A} → F x) ≃ ({x : A} → G x)
equivImplicitΠCod k .fst f {x} = k {x} .fst (f {x})
equivImplicitΠCod k .snd .equiv-proof f .fst .fst {x}   = equivCtr (k {x}) (f {x}) .fst
equivImplicitΠCod k .snd .equiv-proof f .fst .snd i {x} = equivCtr (k {x}) (f {x}) .snd i
equivImplicitΠCod k .snd .equiv-proof f .snd (g , p) i .fst {x} =
  equivCtrPath (k {x}) (f {x}) (g {x} , λ j → p j {x}) i .fst
equivImplicitΠCod k .snd .equiv-proof f .snd (g , p) i .snd j {x} =
  equivCtrPath (k {x}) (f {x}) (g {x} , λ k → p k {x}) i .snd j

equiv→Iso : (A ≃ B) → (C ≃ D) → Iso (A → C) (B → D)
equiv→Iso h k .Iso.fun f b = equivFun k (f (invEq h b))
equiv→Iso h k .Iso.inv g a = invEq k (g (equivFun h a))
equiv→Iso h k .Iso.rightInv g = funExt λ b → retEq k _ ∙ cong g (retEq h b)
equiv→Iso h k .Iso.leftInv f = funExt λ a → secEq k _ ∙ cong f (secEq h a)

equiv→ : (A ≃ B) → (C ≃ D) → (A → C) ≃ (B → D)
equiv→ h k = isoToEquiv (equiv→Iso h k)

equivCompIso : (A ≃ B) → (C ≃ D) → Iso (A ≃ C) (B ≃ D)
equivCompIso h k .Iso.fun f = compEquiv (compEquiv (invEquiv h) f) k
equivCompIso h k .Iso.inv g = compEquiv (compEquiv h g) (invEquiv k)
equivCompIso h k .Iso.rightInv g = equivEq (equiv→Iso h k .Iso.rightInv (equivFun g))
equivCompIso h k .Iso.leftInv f = equivEq (equiv→Iso h k .Iso.leftInv (equivFun f))

equivComp : (A ≃ B) → (C ≃ D) → (A ≃ C) ≃ (B ≃ D)
equivComp h k = isoToEquiv (equivCompIso h k)

-- Some helpful notation:
_≃⟨_⟩_ : (X : Type ℓ) → (X ≃ B) → (B ≃ C) → (X ≃ C)
_ ≃⟨ f ⟩ g = compEquiv f g

_■ : (X : Type ℓ) → (X ≃ X)
_■ = idEquiv

infixr  0 _≃⟨_⟩_
infix   1 _■

composesToId→Equiv : (f : A → B) (g : B → A) → f ∘ g ≡ idfun B → isEquiv f → isEquiv g
composesToId→Equiv f g id iseqf =
  isoToIsEquiv
    (iso g f
         (λ b → (λ i → equiv-proof iseqf (f b) .snd (g (f b) , cong (λ h → h (f b)) id) (~ i) .fst)
                ∙∙ cong (λ x → equiv-proof iseqf (f b) .fst .fst) id
                ∙∙ λ i → equiv-proof iseqf (f b) .snd (b , refl) i .fst)
         λ a i → id i a)

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
module Scratch where
  open import OutsideIn.Prelude
  open import OutsideIn.X
  open import OutsideIn.Instantiations.Simple as Simple
  import OutsideIn

  data DCs : ℕ → Set where
    True : DCs 0
    False : DCs 0

  data TCs : Set where
    BoolT : TCs

  open OutsideIn(Simple DCs)

  data ⊥ : Set where
  import OutsideIn.Inference.Separator as S
  open S(Simple DCs)

  ep : ∀ {v} → SConstraint v
  ep = SConstraint.ε
  _~_ : ∀ {v} → Simple.Type v → Simple.Type v → SConstraint v
  _~_ = SConstraint._∼_

  con : SConstraint  (TCs ⨁ 7)
  con = (((((SConstraint.ε ∧′
                 (Var (suc (suc zero)) SConstraint.∼ Var (suc (suc (suc (suc zero))))))
               ∧′ (Var (suc (suc (suc zero))) SConstraint.∼ Var (suc (suc (suc (suc (suc zero)))))))
              ∧′ ((((Var (suc zero) SConstraint.∼ Var (suc (suc (suc zero))))
                    ∧′ (Var (suc zero) SConstraint.∼ Var (suc (suc (suc (suc (suc (suc (suc BoolT)))))))))
                   ∧′ (Var (suc (suc (suc (suc (suc (suc (suc BoolT))))))) SConstraint.∼ Var (suc (suc zero))))
                  ∧′ ((((Var zero SConstraint.∼ Var (suc (suc (suc zero)))) ∧′ (Var zero SConstraint.∼ Var (suc (suc (suc (suc (suc (suc (suc BoolT)))))))))
                      ∧′ (Var (suc (suc (suc (suc (suc (suc (suc BoolT))))))) SConstraint.∼ Var (suc (suc zero)))) ∧′ SConstraint.ε)))
             ∧′ (Var (suc (suc (suc (suc (suc (suc zero)))))) SConstraint.∼ ((funTy · Var (suc (suc (suc (suc zero))))) · Var (suc (suc (suc (suc (suc zero)))))))))

  con-s : SConstraint (SVar TCs 7)
  con-s = Functor.map sconstraint-is-functor svar-iso₁ con

  con′ : SConstraint (TCs ⨁ 1)
  con′ = SConstraint.ε ∧′ ((Var zero) SConstraint.∼ (Var (suc BoolT)) )

  conn : SConstraint  (TCs ⨁ 2)
  conn =  (Var (suc zero)) Simple.∼ ((funTy · Var zero) · Var zero)

  v = Simple.simplifier (λ a b → true) 1 ax SConstraint.ε conn

  open import Data.List

  --

  -- zero --> suc suc zero
  -- suc zero --> zero
  -- suc suc zero --> suc zero
  -- suc suc suc zero --> suc suc zero
  -- suc suc suc suc zero --> suc suc suc zero
  -- suc suc suc suc suc zero --> suc suc suc suc zero
  -- suc suc suc suc suc suc zero --> suc suc suc suc suc zero

  e : ∀ {tv} → Expression tv TCs _
  e = λ′ case Var (N zero) of
                ( DC True  →′ Var (DC False)
                ∣ DC False →′ Var (DC True )
                ∣ esac
                )

  e2 : ∀ {tv ev} → Expression tv ev _
  e2 = λ′ Var (N zero)

  p2 : Program ⊥ TCs
  p2 = bind₂ 1 · e2 ∷ SConstraint.ε ⇒ Var zero ⟶ Var zero
     , bind₁ e2
     , end

  p : Program ⊥ TCs
  p = bind₂ 0 · e ∷ SConstraint.ε ⇒ Var BoolT ⟶ Var BoolT
    , bind₁ e
    , end

  Γ : Environment ⊥ TCs
  Γ (DC True) = DC∀ 0 · [] ⟶ BoolT
  Γ (DC False) = DC∀ 0 · [] ⟶ BoolT
  Γ (N ())
  open import Data.Fin

  test = go ax Γ (λ a b → true) p
  test2 = go ax Γ (λ a b → true) p2

max_stars_repo_name: liamoc/outside-in

max_issues_repo_name: liamoc/outside-in

max_forks_repo_name: liamoc/outside-in


text:
-- -----------------------------
-- Equality

module Homogenous.Equality where
import Homogenous.Base
import EqBase
import PolyDepPrelude

open PolyDepPrelude using ( Datoid
                   ; Bool; true; false; _&&_
                   ; Pair; pair
                   ; Either; left; right
                   ; suc; zero
                   ; _::_; nil
                   ; cmp; Unit; unit
                   )
open Homogenous.Base using (Arity; Sig; Fa; F; T; It; out)

eq_step_ar : (n : Arity){X : Set}(fs : Fa n (X -> Bool))(xs : Fa n X) -> Bool
eq_step_ar zero    unit         unit         = true
eq_step_ar (suc m) (pair f fs') (pair x xs') = f x && eq_step_ar m fs' xs'

-- We write left as This (as in "This constructor" and right as Other
-- (as in "one of the Other constructors") to help the reader

eq_step' : (fi : Sig){X : Set} -> F fi (X -> Bool) -> F fi X -> Bool
eq_step' (nil)   ()         ()  -- empty
eq_step' (n :: ns) (left fs ) (left xs ) = eq_step_ar n fs xs
eq_step' (n :: ns) (left fs ) (right y') = false
eq_step' (n :: ns) (right x') (left xs ) = false
eq_step' (n :: ns) (right x') (right y') = eq_step' ns x' y'

eq_step : (fi : Sig)(x : F fi (T fi -> Bool)) -> T fi -> Bool
eq_step fi x = \t -> eq_step' fi x (out fi t)

equal' : (fi : Sig) -> T fi -> (T fi -> Bool)
equal' fi = It fi (eq_step fi)

equal : (fi : Sig) -> T fi -> T fi -> Bool
equal fi x y = equal' fi x y

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Structure.Monoid.Laws where

open import Prelude

record MonoidLaws {a} (A : Set a) {{Mon : Monoid A}} : Set a where
  field
    idLeft  : (x : A)     → mempty <> x ≡ x
    idRight : (x : A)     → x <> mempty ≡ x
    <>assoc : (x y z : A) → x <> (y <> z) ≡ (x <> y) <> z

open MonoidLaws {{...}} public

{-# DISPLAY MonoidLaws.idLeft _ = idLeft   #-}
{-# DISPLAY MonoidLaws.idRight _ = idRight #-}
{-# DISPLAY MonoidLaws.<>assoc _ = <>assoc #-}

instance
  MonoidLawsList : ∀ {a} {A : Set a} → MonoidLaws (List A)
  idLeft  {{MonoidLawsList}} xs       = refl
  idRight {{MonoidLawsList}} []       = refl
  idRight {{MonoidLawsList}} (x ∷ xs) = x ∷_ $≡ idRight xs
  <>assoc {{MonoidLawsList}} []       ys zs = refl
  <>assoc {{MonoidLawsList}} (x ∷ xs) ys zs = x ∷_ $≡ <>assoc xs ys zs

  MonoidLawsMaybe : ∀ {a} {A : Set a} {{_ : Monoid A}} {{_ : MonoidLaws A}} → MonoidLaws (Maybe A)
  idLeft  {{MonoidLawsMaybe}} x     = refl
  idRight {{MonoidLawsMaybe}} nothing  = refl
  idRight {{MonoidLawsMaybe}} (just _) = refl
  <>assoc {{MonoidLawsMaybe}} nothing  y z = refl
  <>assoc {{MonoidLawsMaybe}} (just x) y z = refl

  -- Can't do function lifting because no extentionality.

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
module _ where

import DummyModule Set Set


text:
module Data.HVec where

open import Data.Fin using (Fin; zero; suc)
open import Data.Nat using (ℕ; zero; suc; _+_)

open import Function using (const)

open import Data.Vec as V using (Vec; []; _∷_; _[_]≔_)

open import Level as L using (Level; suc)

-- ------------------------------------------------------------------------
-- Hetrogenous Vectors

infixr 5 _∷_

data HVec { ℓ } : ( n : ℕ ) → Vec (Set ℓ) n → Set ℓ where
  [] : HVec 0 []
  _∷_ : ∀ { n } { A : Set ℓ } { As }
    → A
    → HVec n As
    -- ----------------------
    → HVec (1 + n) (A ∷ As)

-- -- ------------------------------------------------------------------------

private
  variable
    ℓ : Level
    A : Set ℓ
    n : ℕ
    As : Vec (Set ℓ) n

length : HVec n As → ℕ
length { n = n } _ = n

head : HVec (1 + n) As → (V.head As)
head (x ∷ xs) = x

tail : HVec (1 + n) As → HVec n (V.tail As)
tail (x ∷ xs) = xs

lookup : HVec n As → (i : Fin n) → (V.lookup As i)
lookup (x ∷ xs) zero = x
lookup (x ∷ xs) (suc i) = lookup xs i

insert : HVec n As → (i : Fin (1 + n)) → A → HVec (1 + n) (V.insert As i A)
insert xs zero v = v ∷ xs
insert (x ∷ xs) (suc i) v = x ∷ insert xs i v

remove : HVec (1 + n) As → (i : Fin (1 + n)) → HVec n (V.remove As i)
remove (x ∷ xs) zero = xs
remove (x₁ ∷ x₂ ∷ xs) (suc i) = x₁ ∷ remove (x₂ ∷ xs) i

updateAt : ∀ { ℓ n } { A : Set ℓ } { As : Vec (Set ℓ) n } (i : Fin n) → (V.lookup As i → A) → HVec n As → HVec n (As [ i ]≔ A)
updateAt zero f (x ∷ xs) = f x ∷ xs
updateAt (suc i) f (x ∷ xs) = x ∷ updateAt i f xs

infixl 6 _[_]$=_

_[_]$=_ : HVec n As → (i : Fin n) → (V.lookup As i → A) → HVec n (As [ i ]≔ A)
xs [ i ]$= f = updateAt i f xs

infixl 6 _[_]&=_

_[_]&=_ : HVec n As → (i : Fin n) → A → HVec n (As [ i ]≔ A)
xs [ i ]&= y = xs [ i ]$= const y

-- -- ------------------------------------------------------------------------

max_stars_repo_name: johnyob/agda-sigma

max_issues_repo_name: johnyob/agda-sigma

max_forks_repo_name: johnyob/agda-sigma


text:
open import Oscar.Prelude
open import Oscar.Data.Proposequality

module Oscar.Class.Symmetrical where

private

  module _
    {𝔞} {𝔄 : Ø 𝔞}
    {𝔟} {𝔅 : Ø 𝔟}
    where
    module Visible
      (_∼_ : 𝔄 → 𝔄 → 𝔅)
      {ℓ} (_↦_ : 𝔅 → 𝔅 → Ø ℓ)
      where
      𝓼ymmetrical = λ x y → (x ∼ y) ↦ (y ∼ x)
      𝓈ymmetrical = ∀ x y → 𝓼ymmetrical x y
      record 𝓢ymmetrical
        {𝓢 : 𝔄 → 𝔄 → Ø ℓ}
        ⦃ _ : 𝓢 ≡ 𝓼ymmetrical ⦄
        : Ø 𝔞 ∙̂ ℓ
        where
        field symmetrical : 𝓈ymmetrical -- FIXME might there be some reason to use "∀ x y → 𝓢 x y" here instead?
      Symmetrical : Ø _
      Symmetrical = 𝓢ymmetrical ⦃ ∅ ⦄
      symmetrical⟦_/_⟧ : ⦃ _ : Symmetrical ⦄ → 𝓈ymmetrical
      symmetrical⟦_/_⟧ ⦃ I ⦄ = 𝓢ymmetrical.symmetrical I
    module Hidden
      {_∼_ : 𝔄 → 𝔄 → 𝔅}
      {ℓ} {_↦_ : 𝔅 → 𝔅 → Ø ℓ}
      where
      open Visible _∼_ _↦_
      symmetrical : ⦃ _ : Symmetrical ⦄ → 𝓈ymmetrical
      symmetrical = symmetrical⟦_/_⟧

open Visible public
open Hidden public


text:
-- Andreas, 2012-06-07
-- {-# OPTIONS --show-implicit -v tc.rec:100 -v tc.meta.assign:15 #-}
module Issue387 where

import Common.Level

mutual

  record R' (A : Set) : Set where
    field f : _

  c' : {A : Set} -> A -> R' A
  c' a = record { f = a }

-- previous to fix of 387, this had an unresolved meta
-- because two metas were created for _


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

open import Categories.Category.Core using (Category)

module Categories.Diagram.Pushout {o ℓ e} (C : Category o ℓ e) where

open Category C
open HomReasoning
open Equiv

open import Categories.Morphism.Reasoning C as Square
  renaming (glue to glue-square) hiding (id-unique)

open import Level

private
  variable
    A B E X Y Z : Obj
    f g h j : A ⇒ B

record Pushout (f : X ⇒ Y) (g : X ⇒ Z) : Set (o ⊔ ℓ ⊔ e) where
  field
    {Q} : Obj
    i₁  : Y ⇒ Q
    i₂  : Z ⇒ Q

  field
    commute   : i₁ ∘ f ≈ i₂ ∘ g
    universal : {h₁ : Y ⇒ B} {h₂ : Z ⇒ B} → h₁ ∘ f ≈ h₂ ∘ g → Q ⇒ B
    unique    : {h₁ : Y ⇒ E} {h₂ : Z ⇒ E} {j : Q ⇒ E} {eq : h₁ ∘ f ≈ h₂ ∘ g} →
                  j ∘ i₁ ≈ h₁ → j ∘ i₂ ≈ h₂ →
                  j ≈ universal eq

    universal∘i₁≈h₁  : {h₁ : Y ⇒ E} {h₂ : Z ⇒ E} {eq : h₁ ∘ f ≈ h₂ ∘ g} →
                         universal eq ∘ i₁ ≈ h₁
    universal∘i₂≈h₂  : {h₁ : Y ⇒ E} {h₂ : Z ⇒ E} {eq : h₁ ∘ f ≈ h₂ ∘ g} →
                         universal eq ∘ i₂ ≈ h₂

  unique-diagram : h ∘ i₁ ≈ j ∘ i₁ →
                   h ∘ i₂ ≈ j ∘ i₂ →
                   h ≈ j
  unique-diagram {h = h} {j = j} eq₁ eq₂ = begin
    h            ≈⟨ unique eq₁ eq₂ ⟩
    universal eq ≈˘⟨ unique refl refl ⟩
    j            ∎
    where eq = extendˡ commute

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:
module Basic.Compiler.Machine where

open import Basic.AST
open import Basic.BigStep
open import Basic.Compiler.Code

open import Utils.Decidable
open import Data.Product
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Data.List hiding (unfold)
open import Data.Bool
open import Data.Nat
open import Data.Maybe

{-

This is a simple interpreter for the abstract machine code.

There's no corresponding part in the book.

A nice thing about the abstract machine is that each transition is decidable,
so we can tell at each point whether our program is stuck or may continue.

Of course, this doesn't mean that *computation sequences* are decidable! (it's pretty much
just the halting problem).

What we can do is specify how many steps we'd like to compute, and then compute that far.

The "steps" function below only computes the ending configuration, while "trace"
returns a list of all intermediate configurations.

"unfold" returns a computation sequence if the program terminates or gets stuck in
the given number of steps.

-}

step : ∀ {n} (c : Code n) e s → Dec (∃₂ λ c' e' -> ∃ λ s' → ⟨ c , e , s ⟩▷⟨ c' , e' , s' ⟩)
step [] e s = no (λ {(c' , e' , s' , ())})
step (PUSH x ∷ c) e s = yes (c , nat x ∷ e , s , PUSH x)
step (FETCH x ∷ c) e s = yes (c , nat _ ∷ e , s , FETCH x)
step (STORE x ∷ c) [] s = no (λ {(c' , e' , s' , ())})
step (STORE x ∷ c) (nat x₁ ∷ e) s = yes (c , e , _ , STORE x)
step (STORE x ∷ c) (bool x₁ ∷ e) s = no (λ {(c' , e' , s' , ())})
step (ADD ∷ c) [] s = no (λ { (c' , e' , s' , ()) })
step (ADD ∷ c) (nat x ∷ []) s = no (λ { (c' , e' , s' , ()) })
step (ADD ∷ c) (nat x ∷ nat x₁ ∷ e) s = yes (c , nat _ ∷ e , s , ADD x x₁)
step (ADD ∷ c) (nat x ∷ bool x₁ ∷ e) s = no (λ { (c' , e' , s' , ()) })
step (ADD ∷ c) (bool x ∷ e) s = no (λ { (c' , e' , s' , ()) })

step (MUL ∷ c) [] s = no (λ { (c' , e' , s' , ()) })
step (MUL ∷ c) (nat x ∷ []) s = no (λ { (c' , e' , s' , ()) })
step (MUL ∷ c) (nat x ∷ nat x₁ ∷ e) s = yes (c , nat _ ∷ e , s , MUL x x₁)
step (MUL ∷ c) (nat x ∷ bool x₁ ∷ e) s = no (λ { (c' , e' , s' , ()) })
step (MUL ∷ c) (bool x ∷ e) s = no (λ { (c' , e' , s' , ()) })

step (SUB ∷ c) [] s = no (λ { (c' , e' , s' , ()) })
step (SUB ∷ c) (nat x ∷ []) s = no (λ { (c' , e' , s' , ()) })
step (SUB ∷ c) (nat x ∷ nat x₁ ∷ e) s = yes (c , nat _ ∷ e , s , SUB x x₁)
step (SUB ∷ c) (nat x ∷ bool x₁ ∷ e) s = no (λ { (c' , e' , s' , ()) })
step (SUB ∷ c) (bool x ∷ e) s = no (λ { (c' , e' , s' , ()) })

step (TRUE ∷ c) e s = yes (c  , bool true ∷ e , s , TRUE)
step (FALSE ∷ c) e s = yes (c , bool false ∷ e , s , FALSE)

step (EQ ∷ c) [] s = no (λ { (c' , e' , s' , ()) })
step (EQ ∷ c) (nat x ∷ []) s = no (λ { (c' , e' , s' , ()) })
step (EQ ∷ c) (nat x ∷ nat x₁ ∷ e) s = yes (c , bool ⌊ x ≡⁇ x₁ ⌋ ∷ e , s , EQ x x₁)
step (EQ ∷ c) (nat x ∷ bool x₁ ∷ e) s = no (λ { (c' , e' , s' , ()) })
step (EQ ∷ c) (bool x ∷ e) s = no (λ { (c' , e' , s' , ()) })

step (LTE ∷ c) [] s = no (λ { (c' , e' , s' , ()) })
step (LTE ∷ c) (nat x ∷ []) s = no (λ { (c' , e' , s' , ()) })
step (LTE ∷ c) (nat x ∷ nat x₁ ∷ e) s = yes (c , bool ⌊ x ≤⁇ x₁ ⌋ ∷ e , s , LTE x x₁)
step (LTE ∷ c) (nat x ∷ bool x₁ ∷ e) s = no (λ { (c' , e' , s' , ()) })
step (LTE ∷ c) (bool x ∷ e) s = no (λ { (c' , e' , s' , ()) })

step (LT ∷ c) [] s = no (λ { (c' , e' , s' , ()) })
step (LT ∷ c) (nat x ∷ []) s = no (λ { (c' , e' , s' , ()) })
step (LT ∷ c) (nat x ∷ nat x₁ ∷ e) s = yes (c , bool ⌊ x <⁇ x₁ ⌋ ∷ e , s , LT x x₁)
step (LT ∷ c) (nat x ∷ bool x₁ ∷ e) s = no (λ { (c' , e' , s' , ()) })
step (LT ∷ c) (bool x ∷ e) s = no (λ { (c' , e' , s' , ()) })

step (AND ∷ c) [] s = no (λ { (c' , e' , s' , ()) })
step (AND ∷ c) (nat x ∷ e) s = no (λ { (c' , e' , s' , ()) })
step (AND ∷ c) (bool x ∷ []) s = no (λ { (c' , e' , s' , ()) })
step (AND ∷ c) (bool x ∷ nat x₁ ∷ e) s = no (λ { (c' , e' , s' , ()) })
step (AND ∷ c) (bool x ∷ bool x₁ ∷ e) s = yes (c , bool (x ∧ x₁) ∷ e , s , AND x x₁)

step (NOT ∷ c) [] s = no (λ { (c' , e' , s' , ()) })
step (NOT ∷ c) (nat x ∷ e) s = no (λ { (c' , e' , s' , ()) })
step (NOT ∷ c) (bool x ∷ e) s = yes (c , bool _ ∷ e , s , NOT x)
step (NOOP ∷ c) e s = yes (c , e , s , NOOP)

step (BRANCH x x₁ ∷ c) [] s = no (λ { (c' , e' , s' , ()) })
step (BRANCH x x₁ ∷ c) (nat x₂ ∷ e) s = no (λ { (c' , e' , s' , ()) })
step (BRANCH x x₁ ∷ c) (bool true ∷ e) s = yes (x ++ c , e , s , BRANCH)
step (BRANCH x x₁ ∷ c) (bool false ∷ e) s = yes (x₁ ++ c , e , s , BRANCH)

step (LOOP x x₁ ∷ c) e s = yes (x ++ BRANCH (x₁ ++ LOOP x x₁ ∷ []) (NOOP ∷ []) ∷ c , e , s , LOOP)

steps : ∀ {n} → Code n → Stack → State n → ℕ → (Code n × Stack × State n)
steps c e s zero = c , e , s
steps c e s (suc n) with step c e s
... | yes (c' , e' , s' , p) = steps c' e' s' n
... | no _ = c , e , s

trace : ∀ {n} → Code n → Stack → State n → ℕ → List (Code n × Stack × State n)
trace c e s zero = []
trace c e s (suc n) with step c e s
... | yes  (c' , e' , s' , p) = (c , e , s) ∷ trace c' e' s' n
... | no _ = (c , e , s) ∷ []

unfold :
  ∀ {n} c e (s : State n) → ℕ → Maybe (∃₂ λ c' e' → ∃ λ s' → ⟨ c , e , s ⟩▷*⟨ c' , e' , s' ⟩)
unfold [] e s n₁ = just ([] , e , s , done)
unfold (x ∷ c) e s zero = nothing
unfold (x ∷ c) e s (suc n) with step (x ∷ c) e s
... | no ¬p = just (x ∷ c , e , s , stuck (λ c' e' s' z → ¬p (c' , e' , s' , z)))
... | yes (c' , e' , s' , p) with unfold c' e' s' n
... | nothing = nothing
... | just (c'' , e'' , s'' , seq) = just (c'' , e'' , s'' , p ∷ seq)

max_stars_repo_name: AndrasKovacs/SemanticsWithApplications

max_issues_repo_name: AndrasKovacs/SemanticsWithApplications

max_forks_repo_name: AndrasKovacs/SemanticsWithApplications


text:
{-# OPTIONS --safe --without-K #-}
module Generics.All where

open import Generics.Prelude
open import Generics.Telescope
open import Generics.Desc
open import Generics.Mu

private
  variable
    P   : Telescope ⊤
    p   : ⟦ P ⟧tel tt
    V I : ExTele P
    ℓ c : Level
    n   : ℕ

levelAllIndArg : ConDesc P V I → Level → Level
levelAllIndArg (var _) c = c
levelAllIndArg (π {ℓ} _ _ C) c = ℓ ⊔ levelAllIndArg C c
levelAllIndArg (A ⊗ B) c = levelAllIndArg A c ⊔ levelAllIndArg B c

AllIndArg
  : {X : ⟦ P , I ⟧xtel → Set ℓ}
    (Pr : ∀ {i} → X (p , i) → Set c)
    (C : ConDesc P V I)
  → ∀ {v} → ⟦ C ⟧IndArg X (p , v) → Set (levelAllIndArg C c)
AllIndArg Pr (var _) x = Pr x
AllIndArg Pr (π (n , ai) S C) x = (s : < relevance ai > S _) → AllIndArg Pr C (app< n , ai > x s)
AllIndArg Pr (A ⊗ B) (xa , xb) = AllIndArg Pr A xa × AllIndArg Pr B xb

AllIndArgω
  : {X : ⟦ P , I ⟧xtel → Set ℓ}
    (Pr : ∀ {i} → X (p , i) → Setω)
    (C : ConDesc P V I)
  → ∀ {v} → ⟦ C ⟧IndArg X (p , v) → Setω
AllIndArgω Pr (var _) x = Pr x
AllIndArgω Pr (π (n , ai) S C) x = (s : < relevance ai > S _) → AllIndArgω Pr C (app< n , ai > x s)
AllIndArgω Pr (A ⊗ B) (xa , xb) = AllIndArgω Pr A xa ×ω AllIndArgω Pr B xb

levelAllCon : ConDesc P V I → Level → Level
levelAllCon (var _) c = lzero
levelAllCon (π {ℓ} _ _ C) c = levelAllCon C c
levelAllCon (A ⊗ B) c = levelAllIndArg A c ⊔ levelAllCon B c

AllCon
  : {X : ⟦ P , I ⟧xtel → Set ℓ}
    (Pr : ∀ {i} → X (p , i) → Set c)
    (C : ConDesc P V I)
  → ∀ {v i} → ⟦ C ⟧Con X (p , v , i) → Set (levelAllCon C c)
AllCon Pr (var _) x = ⊤
AllCon Pr (π _ _ C) (_ , x) = AllCon Pr C x
AllCon Pr (A ⊗ B) (xa , xb) = AllIndArg Pr A xa × AllCon Pr B xb

AllConω
  : {X : ⟦ P , I ⟧xtel → Set ℓ}
    (Pr : ∀ {i} → X (p , i) → Setω)
    (C : ConDesc P V I)
  → ∀ {v i} → ⟦ C ⟧Con X (p , v , i) → Setω
AllConω Pr (var f) x = ⊤ω
AllConω Pr (π ia S C) (_ , x) = AllConω Pr C x
AllConω Pr (A ⊗ B) (xa , xb) = AllIndArgω Pr A xa ×ω AllConω Pr B xb

AllData : {X  : ⟦ P , I ⟧xtel → Set ℓ}
          (Pr : ∀ {i} → X (p , i) → Set c)
          (D : DataDesc P I n)
        → ∀ {i} ((k , x) : ⟦ D ⟧Data X (p , i))
        → Set (levelAllCon (lookupCon D k) c)
AllData Pr D (k , x) = AllCon Pr (lookupCon D k) x

AllDataω : {X  : ⟦ P , I ⟧xtel → Set ℓ}
           (Pr : ∀ {i} → X (p , i) → Setω)
           (D : DataDesc P I n)
         → ∀ {i} (x : ⟦ D ⟧Data X (p , i))
         → Setω
AllDataω Pr D (k , x) = AllConω Pr (lookupCon D k) x

max_stars_repo_name: flupe/generics

max_issues_repo_name: flupe/generics

max_forks_repo_name: flupe/generics


text:
module OList.Properties {A : Set}(_≤_ : A → A → Set) where

open import Data.List
open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import List.Sorted _≤_
open import OList _≤_

lemma-olist-sorted : {b : Bound} → (xs : OList b) → Sorted (forget xs)
lemma-olist-sorted onil = nils
lemma-olist-sorted (:< {x = x} _ onil) = singls x
lemma-olist-sorted (:< b≤x (:< (lexy x≤y) ys)) = conss x≤y (lemma-olist-sorted (:< (lexy x≤y) ys))

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


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

module LeqLemmas where

open import Data.Nat
  using (ℕ; zero; suc; _+_; _*_; _<_; _≤_; _≤?_; z≤n; s≤s;
    module ≤-Reasoning)
open import Data.Nat.Properties.Simple
  using (*-comm; +-right-identity; +-comm; +-assoc)
open import Data.Nat.Properties
  using (cancel-+-left-≤; n≤m+n)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; cong; module ≡-Reasoning)
open import Relation.Binary using (Decidable)
open import Relation.Binary.Core using (Transitive; _⇒_)
open import Data.Fin
  using (Fin; zero; suc; toℕ; fromℕ; raise; inject≤)
open import Data.Fin.Properties using (bounded; to-from)

------------------------------------------------------------------------------
-- Proofs and definitions about ≤ on natural numbers

_<?_ : Decidable _<_
i <? j = suc i ≤? j

-- buried in Data.Nat

refl′ : _≡_ ⇒ _≤_
refl′ {0} refl = z≤n
refl′ {suc m} refl = s≤s (refl′ refl)

trans< : Transitive _<_
trans< (s≤s z≤n) (s≤s _) = s≤s z≤n
trans< (s≤s (s≤s i≤j)) (s≤s sj<k) = s≤s (trans< (s≤s i≤j) sj<k)

trans≤ : Transitive _≤_
trans≤ z≤n x = z≤n
trans≤ (s≤s m≤n) (s≤s n≤o) = s≤s (trans≤ m≤n n≤o)

i*1≡i : (i : ℕ) → i * 1 ≡ i
i*1≡i i = begin (i * 1
                   ≡⟨ *-comm i 1 ⟩
                 1 * i
                   ≡⟨ refl ⟩
                 i + 0
                   ≡⟨ +-right-identity i ⟩
                 i ∎)
  where open ≡-Reasoning

i≤i : (i : ℕ) → i ≤ i
i≤i 0 = z≤n
i≤i (suc i) = s≤s (i≤i i)

i≤si : (i : ℕ) → i ≤ suc i
i≤si 0       = z≤n
i≤si (suc i) = s≤s (i≤si i)

i≤j+i : ∀ {i j} → i ≤ j + i
i≤j+i {i} {0} = i≤i i
i≤j+i {i} {suc j} =
  begin (i
           ≤⟨ i≤j+i {i} {j} ⟩
         j + i
           ≤⟨ i≤si (j + i) ⟩
         suc j + i ∎)
  where open ≤-Reasoning

cong+r≤ : ∀ {i j} → i ≤ j → (k : ℕ) → i + k ≤ j + k
cong+r≤ {0}     {j}     z≤n       k = n≤m+n j k
cong+r≤ {suc i} {0}     ()        k -- absurd
cong+r≤ {suc i} {suc j} (s≤s i≤j) k = s≤s (cong+r≤ {i} {j} i≤j k)

cong+l≤ : ∀ {i j} → i ≤ j → (k : ℕ) → k + i ≤ k + j
cong+l≤ {i} {j} i≤j k =
  begin (k + i
           ≡⟨ +-comm k i ⟩
         i + k
           ≤⟨ cong+r≤ i≤j k ⟩
         j + k
           ≡⟨ +-comm j k ⟩
         k + j ∎)
  where open ≤-Reasoning

cong*r≤ : ∀ {i j} → i ≤ j → (k : ℕ) → i * k ≤ j * k
cong*r≤ {0}     {j}     z≤n       k = z≤n
cong*r≤ {suc i} {0}     ()        k -- absurd
cong*r≤ {suc i} {suc j} (s≤s i≤j) k = cong+l≤ (cong*r≤ i≤j k) k

sinj : ∀ {i j} → suc i ≡ suc j → i ≡ j
sinj = cong (λ { 0 → 0 ; (suc x) → x })

sinj≤ : ∀ {i j} → suc i ≤ suc j → i ≤ j
sinj≤ {0}     {j}     _        = z≤n
sinj≤ {suc i} {0}     (s≤s ()) -- absurd
sinj≤ {suc i} {suc j} (s≤s p)  = p

i*n+n≤sucm*n : ∀ {m n} → (i : Fin (suc m)) → toℕ i * n + n ≤ suc m * n
i*n+n≤sucm*n {0} {n} zero =
  begin (n
           ≡⟨ sym (+-right-identity n) ⟩
         n + 0
           ≤⟨ i≤i (n + 0) ⟩
         n + 0 ∎)
  where open ≤-Reasoning
i*n+n≤sucm*n {0} {n} (suc ())
i*n+n≤sucm*n {suc m} {n} i =
  begin (toℕ i * n + n
           ≡⟨ +-comm (toℕ i * n) n ⟩
         n + toℕ i * n
           ≡⟨ refl ⟩
         suc (toℕ i) * n
           ≤⟨ cong*r≤ (bounded i) n ⟩
         suc (suc m) * n ∎)
  where open ≤-Reasoning

i*n+k≤m*n : ∀ {m n} → (i : Fin m) → (k : Fin n) →
            (suc (toℕ i * n + toℕ k) ≤ m * n)
i*n+k≤m*n {0} {_} () _
i*n+k≤m*n {_} {0} _ ()
i*n+k≤m*n {suc m} {suc n} i k =
  begin (suc (toℕ i * suc n + toℕ k)
           ≡⟨  cong suc (+-comm (toℕ i * suc n) (toℕ k))  ⟩
         suc (toℕ k + toℕ i * suc n)
           ≡⟨ refl ⟩
         suc (toℕ k) + (toℕ i * suc n)
           ≤⟨ cong+r≤ (bounded k) (toℕ i * suc n) ⟩
         suc n + (toℕ i * suc n)
           ≤⟨ cong+l≤ (cong*r≤ (sinj≤ (bounded i)) (suc n)) (suc n) ⟩
         suc n + (m * suc n)
           ≡⟨ refl ⟩
         suc m * suc n ∎)
  where open ≤-Reasoning

bounded' : (m : ℕ) → (j : Fin (suc m)) → (toℕ j ≤ m)
bounded' m j with bounded j
... | s≤s pr = pr

simplify-≤ : {m n m' n' : ℕ} → (m ≤ n) → (m ≡ m') → (n ≡ n') → (m' ≤ n')
simplify-≤ leq refl refl = leq

cancel-Fin : ∀ (n y z : ℕ) → ((x : Fin (suc n)) → toℕ x + y ≤ n + z) → y ≤ z
cancel-Fin 0 y z pf = pf zero
cancel-Fin (suc n) y z pf =
  cancel-+-left-≤ n (trans≤ leq (sinj≤ (pf (fromℕ (suc n)))))
  where leq : n + y ≤ toℕ (fromℕ n) + y
        leq = begin (n + y
                       ≡⟨ cong (λ x → x + y) (sym (to-from n)) ⟩
                     toℕ (fromℕ n) + y ∎)
              where open ≤-Reasoning

≤-proof-irrelevance : {m n : ℕ} → (p q : m ≤ n) → p ≡ q
≤-proof-irrelevance z≤n z≤n = refl
≤-proof-irrelevance (s≤s p) (s≤s q) = cong s≤s (≤-proof-irrelevance p q)

raise-suc' : (n a b n+a : ℕ) (n+a≡ : n+a ≡ n + a) →
  (leq : suc a ≤ b) →
  (leq' : suc n+a ≤ n + b) →
  raise n (inject≤ (fromℕ a) leq) ≡ inject≤ (fromℕ n+a) leq'
raise-suc' 0 a b .a refl leq leq' =
  cong (inject≤ (fromℕ a)) (≤-proof-irrelevance leq leq')
raise-suc' (suc n) a b .(suc (n + a)) refl leq (s≤s leq') =
  cong suc (raise-suc' n a b (n + a) refl leq leq')

raise-suc : (m n : ℕ) (j : Fin (suc m)) (d : Fin (suc n))
  (leq : suc (toℕ j * suc n + toℕ d) ≤ suc m * suc n) →
  (leq' : suc (toℕ (suc j) * suc n + toℕ d) ≤ suc (suc m) * suc n) →
  raise (suc n) (inject≤ (fromℕ (toℕ j * suc n + toℕ d)) leq) ≡
  inject≤ (fromℕ (toℕ (suc j) * suc n + toℕ d)) leq'
raise-suc m n j d leq leq' =
  raise-suc'
    (suc n)
    (toℕ j * suc n + toℕ d)
    (suc m * suc n)
    (toℕ (suc j) * suc n + toℕ d)
    (begin (toℕ (suc j) * suc n + toℕ d
              ≡⟨ refl ⟩
            (suc n + toℕ j * suc n) + toℕ d
              ≡⟨ +-assoc (suc n) (toℕ j * suc n) (toℕ d) ⟩
            suc n + (toℕ j * suc n + toℕ d) ∎))
    leq
    leq'
  where open ≡-Reasoning

{-
-- buried in Data.Nat
refl′ : _≡_ ⇒ _≤_
refl′ {0} refl = z≤n
refl′ {suc m} refl = s≤s (refl′ refl)

trans< : Transitive _<_
trans< (s≤s z≤n) (s≤s _) = s≤s z≤n
trans< (s≤s (s≤s i≤j)) (s≤s sj<k) = s≤s (trans< (s≤s i≤j) sj<k)

trans≤ : Transitive _≤_
trans≤ z≤n x = z≤n
trans≤ (s≤s m≤n) (s≤s n≤o) = s≤s (trans≤ m≤n n≤o)

i*1≡i : (i : ℕ) → i * 1 ≡ i
i*1≡i i = begin (i * 1
                   ≡⟨ *-comm i 1 ⟩
                 1 * i
                   ≡⟨ refl ⟩
                 i + 0
                   ≡⟨ +-right-identity i ⟩
                 i ∎)
  where open ≡-Reasoning

i≤i : (i : ℕ) → i ≤ i
i≤i 0 = z≤n
i≤i (suc i) = s≤s (i≤i i)

i≤si : (i : ℕ) → i ≤ suc i
i≤si 0       = z≤n
i≤si (suc i) = s≤s (i≤si i)

i≤j+i : ∀ {i j} → i ≤ j + i
i≤j+i {i} {0} = i≤i i
i≤j+i {i} {suc j} =
  begin (i
           ≤⟨ i≤j+i {i} {j} ⟩
         j + i
           ≤⟨ i≤si (j + i) ⟩
         suc j + i ∎)
  where open ≤-Reasoning

sinj : ∀ {i j} → suc i ≡ suc j → i ≡ j
sinj = cong (λ { 0 → 0 ; (suc x) → x })

i*n+n≤sucm*n : ∀ {m n} → (i : Fin (suc m)) → toℕ i * n + n ≤ suc m * n
i*n+n≤sucm*n {0} {n} zero =
  begin (n
           ≡⟨ sym (+-right-identity n) ⟩
         n + 0
           ≤⟨ i≤i (n + 0) ⟩
         n + 0 ∎)
  where open ≤-Reasoning
i*n+n≤sucm*n {0} {n} (suc ())
i*n+n≤sucm*n {suc m} {n} i =
  begin (toℕ i * n + n
           ≡⟨ +-comm (toℕ i * n) n ⟩
         n + toℕ i * n
           ≡⟨ refl ⟩
         suc (toℕ i) * n
           ≤⟨ cong*r≤ (bounded i) n ⟩
         suc (suc m) * n ∎)
  where open ≤-Reasoning

i*n+k≤m*n : ∀ {m n} → (i : Fin m) → (k : Fin n) →
            (suc (toℕ i * n + toℕ k) ≤ m * n)
i*n+k≤m*n {0} {_} () _
i*n+k≤m*n {_} {0} _ ()
i*n+k≤m*n {suc m} {suc n} i k =
  begin (suc (toℕ i * suc n + toℕ k)
           ≡⟨  cong suc (+-comm (toℕ i * suc n) (toℕ k))  ⟩
         suc (toℕ k + toℕ i * suc n)
           ≡⟨ refl ⟩
         suc (toℕ k) + (toℕ i * suc n)
           ≤⟨ cong+r≤ (bounded k) (toℕ i * suc n) ⟩
         suc n + (toℕ i * suc n)
           ≤⟨ cong+l≤ (cong*r≤ (sinj≤ (bounded i)) (suc n)) (suc n) ⟩
         suc n + (m * suc n)
           ≡⟨ refl ⟩
         suc m * suc n ∎)
  where open ≤-Reasoning

bounded' : (m : ℕ) → (j : Fin (suc m)) → (toℕ j ≤ m)
bounded' m j with bounded j
... | s≤s pr = pr

simplify-≤ : {m n m' n' : ℕ} → (m ≤ n) → (m ≡ m') → (n ≡ n') → (m' ≤ n')
simplify-≤ leq refl refl = leq

cancel-Fin : ∀ (n y z : ℕ) → ((x : Fin (suc n)) → toℕ x + y ≤ n + z) → y ≤ z
cancel-Fin 0 y z pf = pf zero
cancel-Fin (suc n) y z pf =
  cancel-+-left-≤ n (trans≤ leq (sinj≤ (pf (fromℕ (suc n)))))
  where leq : n + y ≤ toℕ (fromℕ n) + y
        leq = begin (n + y
                       ≡⟨ cong (λ x → x + y) (sym (to-from n)) ⟩
                     toℕ (fromℕ n) + y ∎)
              where open ≤-Reasoning

≤-proof-irrelevance : {m n : ℕ} → (p q : m ≤ n) → p ≡ q
≤-proof-irrelevance z≤n z≤n = refl
≤-proof-irrelevance (s≤s p) (s≤s q) = cong s≤s (≤-proof-irrelevance p q)

raise-suc' : (n a b n+a : ℕ) (n+a≡ : n+a ≡ n + a) →
  (leq : suc a ≤ b) →
  (leq' : suc n+a ≤ n + b) →
  raise n (inject≤ (fromℕ a) leq) ≡ inject≤ (fromℕ n+a) leq'
raise-suc' 0 a b .a refl leq leq' =
  cong (inject≤ (fromℕ a)) (≤-proof-irrelevance leq leq')
raise-suc' (suc n) a b .(suc (n + a)) refl leq (s≤s leq') =
  cong suc (raise-suc' n a b (n + a) refl leq leq')

raise-suc : (m n : ℕ) (j : Fin (suc m)) (d : Fin (suc n))
  (leq : suc (toℕ j * suc n + toℕ d) ≤ suc m * suc n) →
  (leq' : suc (toℕ (suc j) * suc n + toℕ d) ≤ suc (suc m) * suc n) →
  raise (suc n) (inject≤ (fromℕ (toℕ j * suc n + toℕ d)) leq) ≡
  inject≤ (fromℕ (toℕ (suc j) * suc n + toℕ d)) leq'
raise-suc m n j d leq leq' =
  raise-suc'
    (suc n)
    (toℕ j * suc n + toℕ d)
    (suc m * suc n)
    (toℕ (suc j) * suc n + toℕ d)
    (begin (toℕ (suc j) * suc n + toℕ d
              ≡⟨ refl ⟩
            (suc n + toℕ j * suc n) + toℕ d
              ≡⟨ +-assoc (suc n) (toℕ j * suc n) (toℕ d) ⟩
            suc n + (toℕ j * suc n + toℕ d) ∎))
    leq
    leq'
  where open ≡-Reasoning
-}

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
------------------------------------------------------------------------
-- Non-dependent and dependent lenses
-- Nils Anders Danielsson
------------------------------------------------------------------------

{-# OPTIONS --cubical --safe #-}

module README where

-- Non-dependent lenses.

import Lens.Non-dependent
import Lens.Non-dependent.Traditional
import Lens.Non-dependent.Higher
import Lens.Non-dependent.Higher.Capriotti
import Lens.Non-dependent.Higher.Surjective-remainder
import Lens.Non-dependent.Equivalent-preimages
import Lens.Non-dependent.Bijection

-- Non-dependent lenses with erased proofs.

import Lens.Non-dependent.Traditional.Erased
import Lens.Non-dependent.Higher.Erased

-- Dependent lenses.

import Lens.Dependent

-- Comparisons of different kinds of lenses, focusing on the
-- definition of composable record getters and setters.

import README.Record-getters-and-setters

max_stars_repo_name: Saizan/dependent-lenses

max_issues_repo_name: Saizan/dependent-lenses

max_forks_repo_name: Saizan/dependent-lenses


text:
{-

Transferring properties of terms between equivalent structures

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Structures.Transfer where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.SIP
open import Cubical.Foundations.Transport
open import Cubical.Structures.Product

private
  variable
    ℓ ℓ₀ ℓ₁ ℓ₂ ℓ₂' : Level

transfer : {ℓ₂' ℓ₀ : Level} {S : Type ℓ → Type ℓ₁} {H : Type ℓ → Type ℓ₂}
  (P : ∀ X → S X → H X → Type ℓ₀)
  (α : EquivAction H) (τ : TransportStr α)
  (ι : StrEquiv S ℓ₂') (θ : UnivalentStr S ι)
  {X Y : Type ℓ} {s : S X} {t : S Y}
  (e : (X , s) ≃[ ι ] (Y , t))
  → (h : H Y) → P X s (invEq (α (e .fst)) h) → P Y t h
transfer P α τ ι θ {X} {Y} {s} {t} e h =
  subst (λ {(Z , u , h) → P Z u h})
    (sip
      (productUnivalentStr ι θ (EquivAction→StrEquiv α)  (TransportStr→UnivalentStr α τ))
      (X , s , invEq (α (e .fst)) h)
      (Y , t , h)
      (e .fst , e .snd , retEq (α (e .fst)) h))

transfer⁻ : {ℓ₂' ℓ₀ : Level} {S : Type ℓ → Type ℓ₁} {H : Type ℓ → Type ℓ₂}
  (P : ∀ X → S X → H X → Type ℓ₀)
  (α : EquivAction H) (τ : TransportStr α)
  (ι : StrEquiv S ℓ₂') (θ : UnivalentStr S ι)
  {X Y : Type ℓ} {s : S X} {t : S Y}
  (e : (X , s) ≃[ ι ] (Y , t))
  → (h : H X) → P Y t (equivFun (α (e .fst)) h) → P X s h
transfer⁻ P α τ ι θ {X} {Y} {s} {t} e h =
  subst⁻ (λ {(Z , u , h) → P Z u h})
    (sip
      (productUnivalentStr ι θ (EquivAction→StrEquiv α)  (TransportStr→UnivalentStr α τ))
      (X , s , h)
      (Y , t , equivFun (α (e .fst)) h)
      (e .fst , e .snd , refl))

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:
module Relations where

open import Level as Level using (zero)
open import Size
open import Function
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P
open ≡-Reasoning

RelTrans : Set → Set₁
RelTrans B = Rel B Level.zero → Rel B Level.zero

Monotone : ∀{B} → RelTrans B → Set₁
Monotone F = ∀ {R S} → R ⇒ S → F R ⇒ F S

-- | Useful example of a compatible up-to technique: equivalence closure.
data EquivCls {B : Set} (R : Rel B Level.zero) : Rel B Level.zero where
  cls-incl : {a b : B} → R a b → EquivCls R a b
  cls-refl : {b : B} → EquivCls R b b
  cls-sym  : {a b : B} → EquivCls R a b → EquivCls R b a
  cls-trans : {a b c : B} → EquivCls R a b → EquivCls R b c → EquivCls R a c

-- | The operation of taking the equivalence closure is monotone.
equivCls-monotone : ∀{B} → Monotone {B} EquivCls
equivCls-monotone R≤S (cls-incl xRy)  = cls-incl (R≤S xRy)
equivCls-monotone R≤S cls-refl        = cls-refl
equivCls-monotone R≤S (cls-sym p)     = cls-sym (equivCls-monotone R≤S p)
equivCls-monotone R≤S (cls-trans p q) =
  cls-trans (equivCls-monotone R≤S p) (equivCls-monotone R≤S q)

-- | The equivalence closure is indeed a closure operator.
equivCls-expanding : ∀{B R} → R ⇒ EquivCls {B} R
equivCls-expanding p = cls-incl p

equivCls-idempotent : ∀{B R} → EquivCls (EquivCls R) ⇒ EquivCls {B} R
equivCls-idempotent (cls-incl p)    = p
equivCls-idempotent cls-refl        = cls-refl
equivCls-idempotent (cls-sym p)     = cls-sym (equivCls-idempotent p)
equivCls-idempotent (cls-trans p q) =
  cls-trans (equivCls-idempotent p) (equivCls-idempotent q)

-- | Equivalence closure gives indeed equivalence relation
equivCls-equiv : ∀{A} → (R : Rel A _) → IsEquivalence (EquivCls R)
equivCls-equiv R = record
  { refl  = cls-refl
  ; sym   = cls-sym
  ; trans = cls-trans
  }

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


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

module Algebra.Construct.Free.Semilattice.Direct where

open import Algebra
open import Prelude
open import Path.Reasoning
infixl 6 _∪_

data 𝒦 (A : Type a) : Type a where
  η : A → 𝒦 A
  _∪_ : 𝒦 A → 𝒦 A → 𝒦 A
  ∅ : 𝒦 A
  ∪-assoc : ∀ xs ys zs → (xs ∪ ys) ∪ zs ≡ xs ∪ (ys ∪ zs)
  ∪-commutative : ∀ xs ys → xs ∪ ys ≡ ys ∪ xs
  ∪-idempotent : ∀ xs → xs ∪ xs ≡ xs
  ∪-identity : ∀ xs → xs ∪ ∅ ≡ xs
  trunc : isSet (𝒦 A)

module _ (semiLattice : Semilattice b) where
  open Semilattice semiLattice
  module _ (sIsSet : isSet 𝑆) (h : A → 𝑆) where
    μ : 𝒦 A → 𝑆
    μ (η x) = h x
    μ (xs ∪ ys) = μ xs ∙ μ ys
    μ ∅ = ε
    μ (∪-assoc xs ys zs i) = assoc (μ xs) (μ ys) (μ zs) i
    μ (∪-commutative xs ys i) = comm (μ xs) (μ ys) i
    μ (∪-idempotent xs i) = idem (μ xs) i
    μ (∪-identity xs i) = ∙ε (μ xs) i
    μ (trunc xs ys x y i j) = sIsSet (μ xs) (μ ys) (cong μ x) (cong μ y) i j

module Eliminators where
  record _⇘_ {a p} (A : Type a) (P : 𝒦 A → Type p) : Type (a ℓ⊔ p) where
    constructor elim
    field
      ⟦_⟧-set : ∀ {xs} → isSet (P xs)
      ⟦_⟧∅ : P ∅
      ⟦_⟧_∪_⟨_∪_⟩ : ∀ xs ys → P xs → P ys → P (xs ∪ ys)
      ⟦_⟧η : ∀ x → P (η x)
    private z = ⟦_⟧∅; f = ⟦_⟧_∪_⟨_∪_⟩
    field
      ⟦_⟧-assoc : ∀ xs ys zs pxs pys pzs →
        f (xs ∪ ys) zs (f xs ys pxs pys) pzs ≡[ i ≔ P (∪-assoc xs ys zs i ) ]≡
        f xs (ys ∪ zs) pxs (f ys zs pys pzs)
      ⟦_⟧-commutative : ∀ xs ys pxs pys →
        f xs ys pxs pys ≡[ i ≔ P (∪-commutative xs ys i) ]≡ f ys xs pys pxs
      ⟦_⟧-idempotent : ∀ xs pxs →
        f xs xs pxs pxs ≡[ i ≔ P (∪-idempotent xs i) ]≡ pxs
      ⟦_⟧-identity : ∀ xs pxs → f xs ∅ pxs z ≡[ i ≔ P (∪-identity xs i) ]≡ pxs
    ⟦_⟧⇓ : ∀ xs → P xs
    ⟦ η x ⟧⇓ = ⟦_⟧η x
    ⟦ xs ∪ ys ⟧⇓ = f xs ys ⟦ xs ⟧⇓ ⟦ ys ⟧⇓
    ⟦ ∅ ⟧⇓ = z
    ⟦ ∪-assoc xs ys zs i ⟧⇓ = ⟦_⟧-assoc xs ys zs ⟦ xs ⟧⇓ ⟦ ys ⟧⇓ ⟦ zs ⟧⇓ i
    ⟦ ∪-commutative xs ys i ⟧⇓ = ⟦_⟧-commutative xs ys ⟦ xs ⟧⇓ ⟦ ys ⟧⇓ i
    ⟦ ∪-idempotent xs i ⟧⇓ = ⟦_⟧-idempotent xs ⟦ xs ⟧⇓ i
    ⟦ ∪-identity xs i ⟧⇓ = ⟦_⟧-identity xs ⟦ xs ⟧⇓ i
    ⟦ trunc xs ys x y i j ⟧⇓ =
        isOfHLevel→isOfHLevelDep 2
          (λ xs → ⟦_⟧-set {xs})
          ⟦ xs ⟧⇓ ⟦ ys ⟧⇓
          (cong ⟦_⟧⇓ x) (cong ⟦_⟧⇓ y)
          (trunc xs ys x y)
          i j
  open _⇘_ public

  infixr 0 ⇘-syntax
  ⇘-syntax = _⇘_
  syntax ⇘-syntax A (λ xs → Pxs) = xs ∈𝒦 A ⇒ Pxs

  record _⇲_ {a p} (A : Type a) (P : 𝒦 A  → Type p) : Type (a ℓ⊔ p) where
    constructor elim-prop
    field
      ∥_∥-prop : ∀ {xs} → isProp (P xs)
      ∥_∥∅ : P ∅
      ∥_∥_∪_⟨_∪_⟩ : ∀ xs ys → P xs → P ys → P (xs ∪ ys)
      ∥_∥η : ∀ x → P (η x)
    private z = ∥_∥∅; f = ∥_∥_∪_⟨_∪_⟩
    ∥_∥⇑ = elim
            (λ {xs} → isProp→isSet (∥_∥-prop {xs}))
            z f ∥_∥η
            (λ xs ys zs pxs pys pzs → toPathP (∥_∥-prop (transp (λ i → P (∪-assoc xs ys zs i)) i0 (f (xs ∪ ys) zs (f xs ys pxs pys) pzs)) (f xs (ys ∪ zs) pxs (f ys zs pys pzs) )))
            (λ xs ys pxs pys → toPathP (∥_∥-prop (transp (λ i → P (∪-commutative xs ys i)) i0 (f xs ys pxs pys)) (f ys xs pys pxs) ))
            (λ xs pxs → toPathP (∥_∥-prop (transp (λ i → P (∪-idempotent xs i)) i0 (f xs xs pxs pxs)) pxs))
            (λ xs pxs → toPathP (∥_∥-prop (transp (λ i → P (∪-identity xs i)) i0 (f xs ∅ pxs z)) pxs))
    ∥_∥⇓ = ⟦ ∥_∥⇑ ⟧⇓

  open _⇲_ public
  elim-prop-syntax : ∀ {a p} → (A : Type a) → (𝒦 A → Type p) → Type (a ℓ⊔ p)
  elim-prop-syntax = _⇲_

  syntax elim-prop-syntax A (λ xs → Pxs) = xs ∈𝒦 A ⇒∥ Pxs ∥

module _ {a} {A : Type a} where
  open Semilattice
  open CommutativeMonoid
  open Monoid
  𝒦-semilattice : Semilattice a
  𝒦-semilattice .commutativeMonoid .monoid .𝑆 = 𝒦 A
  𝒦-semilattice .commutativeMonoid .monoid ._∙_ = _∪_
  𝒦-semilattice .commutativeMonoid .monoid .ε = ∅
  𝒦-semilattice .commutativeMonoid .monoid .assoc = ∪-assoc
  𝒦-semilattice .commutativeMonoid .monoid .ε∙ x = ∪-commutative ∅ x ; ∪-identity x
  𝒦-semilattice .commutativeMonoid .monoid .∙ε = ∪-identity
  𝒦-semilattice .commutativeMonoid .comm = ∪-commutative
  𝒦-semilattice .idem = ∪-idempotent

import Algebra.Construct.Free.Semilattice as Listed

Listed→Direct : Listed.𝒦 A → 𝒦 A
Listed→Direct = Listed.μ 𝒦-semilattice trunc η

Direct→Listed : 𝒦 A → Listed.𝒦 A
Direct→Listed = μ Listed.𝒦-semilattice Listed.trunc (Listed._∷ Listed.[])

Listed→Direct→Listed : (xs : Listed.𝒦 A) → Direct→Listed (Listed→Direct xs) ≡ xs
Listed→Direct→Listed = ∥ ldl ∥⇓
  where
  open Listed using (_⇲_; elim-prop-syntax)
  open _⇲_

  ldl : xs ∈𝒦 A ⇒∥ Direct→Listed (Listed→Direct xs) ≡ xs ∥
  ∥ ldl ∥-prop = Listed.trunc _ _
  ∥ ldl ∥[] = refl
  ∥ ldl ∥ x ∷ xs ⟨ Pxs ⟩ = cong (x Listed.∷_) Pxs

open Eliminators

Direct→Listed→Direct : (xs : 𝒦 A) → Listed→Direct (Direct→Listed xs) ≡ xs
Direct→Listed→Direct = ∥ dld ∥⇓
  where
  dld : xs ∈𝒦 A ⇒∥ Listed→Direct (Direct→Listed xs) ≡ xs ∥
  ∥ dld ∥-prop = trunc _ _
  ∥ dld ∥∅ = refl
  ∥ dld ∥η x = ∪-identity (η x)
  ∥ dld ∥ xs ∪ ys ⟨ Pxs ∪ Pys ⟩ =
    sym (Listed.∙-hom 𝒦-semilattice trunc η (Direct→Listed xs) (Direct→Listed ys)) ;
    cong₂ _∪_ Pxs Pys

Direct⇔Listed : 𝒦 A ⇔ Listed.𝒦 A
Direct⇔Listed .fun = Direct→Listed
Direct⇔Listed .inv = Listed→Direct
Direct⇔Listed .rightInv = Listed→Direct→Listed
Direct⇔Listed .leftInv = Direct→Listed→Direct

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
-- Andreas, 2017-08-10, issue #2667, reported by xekoukou,
-- test case by gallais

-- {-# OPTIONS -v tc.with.split:40 #-}

data Bot : Set where

data A : Set where
  s  : A → A

data P : A → Set where
  p : ∀ {a} → P (s a)

poo : ∀{b} → P b → Set
poo p with Bot
poo {b = s c} p | _ = P c

-- Error WAS (2.5.3): Panic, unbound variable c

-- Expected (as in 2.5.2):
--
-- Inaccessible (dotted) patterns from the parent clause must also be
-- inaccessible in the with clause, when checking the pattern {b = s c},
-- when checking that the clause
-- poo p with Bot
-- poo {b = s c} p | _ = P c
-- has type {b : A} → P b → Set

-- Ideally: succeed.

-- 2018-01-05, Jesper: We're one step closer to an ideal world.


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

module Container.Fixpoint where

open import Container
open import Prelude

data μ {s p} (C : Container s p) : Type (s ℓ⊔ p) where
  sup : ⟦ C ⟧ (μ C) → μ C

record ν {s p} (C : Container s p) : Type (s ℓ⊔ p) where
  coinductive
  field inf : ⟦ C ⟧ (ν C)
open ν public


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2020 Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import LibraBFT.Prelude

-- This module contains a model of a key-value store, along with its
-- functionality and various properties about it.  Most of the properties
-- are not currently used, but they are included here based on our
-- experience in other work, as we think many of them will be needed when
-- reasoning about an actual LibraBFT implementation.

-- Although we believe the assumptions here are reasonable, it is always
-- possible that we made a mistake in postulating one of the properties,
-- making it impossible to implement.  Thus, it would a useful contribution
-- to:
--
-- TODO-1: construct an actual implementation and provide and prove the
-- necessary properties to satisfy the requirements of this module
--
-- Note that this would require some work, but should be relatively
-- straightforward and requires only "local" changes.

module LibraBFT.Base.KVMap  where

 private
  variable
   Key : Set
   Val : Set

   k k' : Key
   v v' : Val

 postulate -- valid assumptions, but would be good to eliminate with a reference implementation (above)
   _≟Key_ : ∀ (k1 k2 : Key) → Dec (k1 ≡ k2)

   KVMap : Set → Set → Set

   _∈KV_          : Key → KVMap Key Val → Set
   _∈KV?_         : (k : Key) (kvm : KVMap Key Val) → Dec (k ∈KV kvm)
   ∈KV-irrelevant : (k : Key) (kvm : KVMap Key Val)
                  → (r s : k ∈KV kvm)
                  → r ≡ s

   -- functionality
   empty          : KVMap Key Val

   ∈KV-empty-⊥    : k ∈KV (empty {Val = Val}) → ⊥

   lookup         : Key → KVMap Key Val → Maybe Val
   kvm-insert     : (k : Key)(v : Val)(kvm : KVMap Key Val)
                  → lookup k kvm ≡ nothing
                  → KVMap Key Val

   -- TODO-3: update properties to reflect kvm-update, consider combining insert/update
   kvm-update     : (k : Key)(v : Val)(kvm : KVMap Key Val)
                  → lookup k kvm ≢ nothing
                  → KVMap Key Val

   kvm-size       : KVMap Key Val → ℕ
   -- TODO-1: add properties relating kvm-toList to empty, kvm-insert and kvm-update
   kvm-toList     : KVMap Key Val → List (Key × Val)
   kvm-toList-length : (kvm : KVMap Key Val)
                     → length (kvm-toList kvm) ≡ kvm-size kvm

   -- TODO-1: need properties showing that the resulting map contains (k , v) for
   --         each pair in the list, provided there is no pair (k , v') in the list
   --         after (k , v).  This is consistent with Haskell's Data.Map.fromList
   kvm-fromList   : List (Key × Val) → KVMap Key Val

   -- properties
   lookup-correct : {kvm : KVMap Key Val}
                  → (prf : lookup k kvm ≡ nothing)
                  → lookup k (kvm-insert k v kvm prf) ≡ just v

   lookup-correct-update
                  : {kvm : KVMap Key Val}
                  → (prf : lookup k kvm ≢ nothing)
                  → lookup k (kvm-update k v kvm prf) ≡ just v

   lookup-stable  : {kvm : KVMap Key Val}{k k' : Key}{v' : Val}
                  → (prf : lookup k kvm ≡ nothing)
                  → lookup k' kvm ≡ just v
                  → lookup k' (kvm-insert k v' kvm prf) ≡ just v

   insert-target  : {kvm : KVMap Key Val}
                  → (prf : lookup k kvm ≡ nothing)
                  → lookup k' kvm ≢ just v
                  → lookup k' (kvm-insert k v' kvm prf) ≡ just v
                  → k' ≡ k × v ≡ v'

   insert-target-≢ : {kvm : KVMap Key Val}{k k' : Key}
                   → (prf : lookup k kvm ≡ nothing)
                   → k' ≢ k
                   → lookup k' kvm ≡ lookup k' (kvm-insert k v kvm prf)

   update-target-≢  : {kvm : KVMap Key Val}
                  → ∀ {k1 k2 x}
                  → k2 ≢ k1
                  → lookup k1 kvm ≡ lookup k1 (kvm-update k2 v kvm x)

   kvm-empty      : lookup {Val = Val} k empty ≡ nothing

   kvm-empty-⊥    : {k : Key} {v : Val} → lookup k empty ≡ just v → ⊥

   KVM-extensionality : ∀ {kvm1 kvm2 : KVMap Key Val}
                      → (∀ (x : Key) → lookup x kvm1 ≡ lookup x kvm2)
                      → kvm1 ≡ kvm2

  -- Corollaries
 lookup-stable-1  : {kvm : KVMap Key Val}{k k' : Key}{v' : Val}
                  → (prf : lookup k kvm ≡ nothing)
                  → lookup k' kvm ≡ just v'
                  → lookup k' (kvm-insert k v kvm prf) ≡ lookup k' kvm
 lookup-stable-1 prf hyp = trans (lookup-stable prf hyp) (sym hyp)

 lookup-correct-update-2
                : {kvm : KVMap Key Val}
                → (prf : lookup k kvm ≢ nothing)
                → lookup k (kvm-update k v kvm prf) ≡ just v'
                → v ≡ v'
 lookup-correct-update-2 {kvm} prf lkup =
   just-injective
     (trans (sym (lookup-correct-update prf)) lkup)

 update-target  : {kvm : KVMap Key Val}
                → ∀ {k1 k2 x}
                → lookup k1 kvm ≢ lookup k1 (kvm-update k2 v kvm x)
                → k2 ≡ k1
 update-target {kvm = kvm}{k1 = k1}{k2 = k2}{x} vneq
    with k1 ≟Key k2
 ...| yes refl = refl
 ...| no  neq  = ⊥-elim (vneq (update-target-≢ {k1 = k1} {k2 = k2} (neq ∘ sym)))

 lookup-correct-update-3 : ∀ {kvm : KVMap Key Val}{k1 k2 v2}
                → (prf : lookup k2 kvm ≢ nothing)
                → lookup k2 kvm ≡ just v2
                → lookup k1 (kvm-update k2 v2 kvm prf) ≡ lookup k1 kvm
 lookup-correct-update-3 {kvm = kvm} {k1 = k1} {k2 = k2} {v2 = v2} prf with k1 ≟Key k2
 ...| yes refl = λ pr → trans (lookup-correct-update {v = v2} prf) (sym pr)
 ...| no  neq  = λ pr → sym (update-target-≢ {k1 = k1} {k2 = k2} {prf} λ k2≢k1 → ⊥-elim (neq (sym k2≢k1)))

 lookup-correct-update-4
                : ∀ {orig : KVMap Key Val}{k1}{v1}
                    {rdy : lookup k1 orig ≢ nothing}
                → lookup k1 orig ≡ just v1
                → kvm-update k1 v1 orig rdy ≡ orig
 lookup-correct-update-4 {orig = orig} {k1 = k1} {v1 = v1} {rdy = rdy} hyp =
    KVM-extensionality {kvm1 = kvm-update k1 v1 orig rdy} {kvm2 = orig}
                       λ x → lookup-correct-update-3 rdy hyp

 insert-target-0 : {kvm : KVMap Key Val}
                 → (prf : lookup k kvm ≡ nothing)
                 → lookup k' kvm ≢ lookup k' (kvm-insert k v kvm prf)
                 → k ≡ k'
 insert-target-0 {k = k} {k' = k'} prf lookups≢
    with k' ≟Key k
 ...| yes refl = refl
 ...| no  neq  = ⊥-elim (lookups≢ (insert-target-≢ prf neq))

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
module 747Negation where

-- Library

open import Relation.Binary.PropositionalEquality using (_≡_; refl) -- added last
open import Data.Nat using (ℕ; zero; suc)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; proj₁; proj₂)

-- Negation is defined as implying false.

¬_ : Set → Set
¬ A = A → ⊥

-- if both ¬ A and A hold, then ⊥ holds (not surprisingly).

¬-elim : ∀ {A : Set}
  → ¬ A
  → A
    ---
  → ⊥

¬-elim = {!!}

infix 3 ¬_

-- Double negation introduction.

¬¬-intro : ∀ {A : Set}
  → A
    -----
  → ¬ ¬ A

¬¬-intro = {!!}

-- Double negation cannot be eliminated in intuitionistic logic.

-- Triple negation elimination.

¬¬¬-elim : ∀ {A : Set}
  → ¬ ¬ ¬ A
    -------
  → ¬ A

¬¬¬-elim = {!!}

-- One direction of the contrapositive.

contraposition : ∀ {A B : Set}
  → (A → B)
    -----------
  → (¬ B → ¬ A)

contraposition = {!!}

-- The other direction cannot be proved in intuitionistic logic.

-- not-equal-to.

_≢_ : ∀ {A : Set} → A → A → Set
x ≢ y  =  ¬ (x ≡ y)

_ : 1 ≢ 2
_ = {!!}

-- One of the first-order Peano axioms.

peano : ∀ {m : ℕ} → zero ≢ suc m
peano = {!!}

-- Copied from 747Isomorphism.

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

-- Two proofs of ⊥ → ⊥ which look different but are the same
-- (assuming extensionality).

id : ⊥ → ⊥
id x = x

id′ : ⊥ → ⊥
id′ ()

id≡id′ : id ≡ id′
id≡id′ = extensionality (λ())

-- Assuming extensionality, any two proofs of a negation are the same

assimilation : ∀ {A : Set} (¬x ¬x′ : ¬ A) → ¬x ≡ ¬x′
assimilation ¬x ¬x′ = extensionality λ x → ⊥-elim (¬x x)

-- Strict inequality (copied from 747Relations).

infix 4 _<_

data _<_ : ℕ → ℕ → Set where

  z<s : ∀ {n : ℕ}
      ------------
    → zero < suc n

  s<s : ∀ {m n : ℕ}
    → m < n
      -------------
    → suc m < suc n

-- 747/PLFA exercise: NotFourLTThree (1 point)
-- Show ¬ (4 < 3).

¬4<3 : ¬ (4 < 3)
¬4<3 = {!!}

-- 747/PLFA exercise: LTIrrefl (1 point)
-- < is irreflexive (never reflexive).

¬n<n : ∀ (n : ℕ) → ¬ (n < n)
¬n<n n = {!!}

-- 747/PLFA exercise: LTTrich (3 points)
-- Show that strict inequality satisfies trichotomy,
-- in the sense that exactly one of the three possibilities holds.
-- Here is the expanded definition of trichotomy.

data Trichotomy (m n : ℕ) : Set where
  is-< : m < n → ¬ m ≡ n → ¬ n < m → Trichotomy m n
  is-≡ : m ≡ n → ¬ m < n → ¬ n < m → Trichotomy m n
  is-> : n < m → ¬ m ≡ n → ¬ m < n → Trichotomy m n

<-trichotomy : ∀ (m n : ℕ) → Trichotomy m n
<-trichotomy m n = {!!}

-- PLFA exercise: one of DeMorgan's Laws as isomorphism
-- ⊎-dual-× : ∀ {A B : Set} → ¬ (A ⊎ B) ≃ (¬ A) × (¬ B)
-- Expand negation as implies-false, then look in 747Relations
-- for a law of which this is a special case.

-- What about ¬ (A × B) ≃ (¬ A) ⊎ (¬ B)?
-- Answer: RHS implies LHS but converse cannot be proved in intuitionistic logic.

-- Intuitionistic vs classical logic.

-- The law of the excluded middle (LEM, or just em) cannot be
-- proved in intuitionistic logic.
-- But we can add it, and get classical logic.

-- postulate
--  em : ∀ {A : Set} → A ⊎ ¬ A

-- How do we know this does not give a contradiction?
-- The following theorem of intuitionistic logic demonstrates this.
-- (The proof is compact, but takes some thought.)

em-irrefutable : ∀ {A : Set} → ¬ ¬ (A ⊎ ¬ A)
em-irrefutable = {!!}

-- PLFA exercise: classical equivalences
-- Excluded middle cannot be proved in intuitionistic logic,
-- but adding it is consistent and gives classical logic.
-- Here are four other classical theorems with the same property.
-- You can show that each of them is logically equivalent to all the others.
-- You do not need to prove twenty implications, since implication is transitive.
-- But there is a lot of choice as to how to proceed!

-- Excluded Middle
em = ∀ {A : Set} → A ⊎ ¬ A

-- Double Negation Elimination
dne = ∀ {A : Set} → ¬ ¬ A → A

-- Peirce’s Law
peirce =  ∀ {A B : Set} → ((A → B) → A) → A

-- Implication as disjunction
iad =  ∀ {A B : Set} → (A → B) → ¬ A ⊎ B

-- De Morgan:
dem = ∀ {A B : Set} → ¬ (¬ A × ¬ B) → A ⊎ B

-- End of classical five exercise.

-- Definition: a formula is stable if double negation holds for it.

Stable : Set → Set
Stable A = ¬ ¬ A → A

-- PLFA exercise: every negated formula is stable.
-- This is triple negation elimination.

-- PLFA exercise: the conjunction of two stable formulas is stable.
-- This is the version of DeMorgan's Law that is a special case, above.

-- Where negation sits in the standard library.

import Relation.Nullary using (¬_)
import Relation.Nullary.Negation using (contraposition)

-- Unicode used in this chapter:

{-

  ¬  U+00AC  NOT SIGN (\neg)
  ≢  U+2262  NOT IDENTICAL TO (\==n)

-}

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
------------------------------------------------------------------------
-- Simple regular expression matcher
------------------------------------------------------------------------

open import Eq
open import Setoids
open import Prelude
import RegExps

module SimpleMatcher (D : Datoid) where

private
  open module D' = Datoid D
  open module S' = Setoid setoid
  open module R  = RegExps setoid

infix 4 _∈‿⟦_⟧¿

------------------------------------------------------------------------
-- A lemma

private

  lemma : forall {a x xs₂}
    -> (xs₁ : [ a ]) -> (xs₁ ++ x ∷ []) ++ xs₂ ≡ xs₁ ++ x ∷ xs₂
  lemma []       = refl
  lemma (x ∷ xs) = cong (\ys -> x ∷ ys) (lemma xs)

------------------------------------------------------------------------
-- Regular expression matcher

-- The type of _∈‿⟦_⟧¿ documents its soundness (assuming that the code
-- is terminating). To prove completeness more work is necessary.

matches-⊙¿ : forall xs₁ xs₂ re₁ re₂
             -> Maybe (xs₁ ++ xs₂ ∈‿⟦ re₁ ⊙ re₂ ⟧)

_∈‿⟦_⟧¿ : (xs : [ carrier ]) -> (re : RegExp) -> Maybe (xs ∈‿⟦ re ⟧)
[]     ∈‿⟦ ε ⟧¿         = just matches-ε
_ ∷ [] ∈‿⟦ • ⟧¿         = just matches-•
x ∷ [] ∈‿⟦ sym y ⟧¿     with x ≟ y
x ∷ [] ∈‿⟦ sym y ⟧¿     | yes eq = just (matches-sym eq)
x ∷ [] ∈‿⟦ sym y ⟧¿     | no _   = nothing
xs     ∈‿⟦ re₁ ∣ re₂ ⟧¿ with xs ∈‿⟦ re₁ ⟧¿
xs     ∈‿⟦ re₁ ∣ re₂ ⟧¿ | just m  = just (matches-∣ˡ m)
xs     ∈‿⟦ re₁ ∣ re₂ ⟧¿ | nothing with xs ∈‿⟦ re₂ ⟧¿
xs     ∈‿⟦ re₁ ∣ re₂ ⟧¿ | nothing | just m  = just (matches-∣ʳ m)
xs     ∈‿⟦ re₁ ∣ re₂ ⟧¿ | nothing | nothing = nothing
xs     ∈‿⟦ re₁ ⊙ re₂ ⟧¿ = matches-⊙¿ [] xs re₁ re₂
[]     ∈‿⟦ re ⋆ ⟧¿      = just (matches-⋆ (matches-∣ˡ matches-ε))
x ∷ xs ∈‿⟦ re ⋆ ⟧¿      with matches-⊙¿ (x ∷ []) xs re (re ⋆)
x ∷ xs ∈‿⟦ re ⋆ ⟧¿      | just m  = just (matches-⋆ (matches-∣ʳ m))
x ∷ xs ∈‿⟦ re ⋆ ⟧¿      | nothing = nothing
_      ∈‿⟦ _ ⟧¿         = nothing

matches-⊙¿ xs₁ xs₂ re₁ re₂ with xs₁ ∈‿⟦ re₁ ⟧¿ | xs₂ ∈‿⟦ re₂ ⟧¿
matches-⊙¿ xs₁ xs₂ re₁ re₂ | just m₁ | just m₂ = just (matches-⊙ m₁ m₂)
matches-⊙¿ xs₁ [] re₁ re₂ | _ | _ = nothing
matches-⊙¿ xs₁ (x ∷ xs₂) re₁ re₂ | _ | _ =
  subst (\xs -> Maybe (xs ∈‿⟦ re₁ ⊙ re₂ ⟧))
        (lemma xs₁)
        (matches-⊙¿ (xs₁ ++ x ∷ []) xs₂ re₁ re₂)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Issue353 where

data Func : Set₁ where
  K : (A : Set) → Func

-- Doesn't work.
module M where

  const : ∀ {A B : Set₁} → A → B → A
  const x = λ _ → x

  ⟦_⟧ : Func → Set → Set
  ⟦ K A ⟧ X = const A X

  data μ (F : Func) : Set where
    ⟨_⟩ : ⟦ F ⟧ (μ F) → μ F

  -- Error: μ is not strictly positive, because it occurs in the second
  -- argument to ⟦_⟧ in the type of the constructor ⟨_⟩ in the
  -- definition of μ.

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
{-

A couple of general facts about equivalences:

- if f is an equivalence then (cong f) is an equivalence ([equivCong])
- if f is an equivalence then pre- and postcomposition with f are equivalences ([preCompEquiv], [postCompEquiv])
- if f is an equivalence then (Σ[ g ] section f g) and (Σ[ g ] retract f g) are contractible ([isContr-section], [isContr-retract])

(these are not in 'Equiv.agda' because they need Univalence.agda (which imports Equiv.agda))
-}
{-# OPTIONS --cubical --safe #-}
module Cubical.Foundations.Equiv.Properties where

open import Cubical.Core.Everything

open import Cubical.Data.Sigma

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

open import Cubical.Foundations.FunExtEquiv

isEquivCong : ∀ {ℓ} {A B : Type ℓ} {x y : A} (e : A ≃ B) → isEquiv (λ (p : x ≡ y) → (cong (fst e) p))
isEquivCong e = EquivJ (λ (B' A' : Type _) (e' : A' ≃ B') →
                         (x' y' : A') → isEquiv (λ (p : x' ≡ y') → cong (fst e') p))
                       (λ _ x' y' → idIsEquiv (x' ≡ y')) _ _ e _ _

congEquiv : ∀ {ℓ} {A B : Type ℓ} {x y : A} (e : A ≃ B) → (x ≡ y) ≃ (e .fst x ≡ e .fst y)
congEquiv e = ((λ (p : _ ≡ _) → cong (fst e) p) , isEquivCong e)

isEquivPreComp : ∀ {ℓ ℓ′} {A B : Type ℓ} {C : Type ℓ′} (e : A ≃ B)
  → isEquiv (λ (φ : B → C) → φ ∘ e .fst)
isEquivPreComp {A = A} {C = C} e = EquivJ
                  (λ (B A : Type _) (e' : A ≃ B) → isEquiv (λ (φ : B → C) → φ ∘ e' .fst))
                  (λ A → idIsEquiv (A → C)) _ _ e

isEquivPostComp : ∀ {ℓ ℓ′} {A B : Type ℓ} {C : Type ℓ′} (e : A ≃ B)
  → isEquiv (λ (φ : C → A) → e .fst ∘ φ)
isEquivPostComp {A = A} {C = C} e = EquivJ
                  (λ (B A : Type _) (e' : A ≃ B) →  isEquiv (λ (φ : C → A) → e' .fst ∘ φ))
                  (λ A → idIsEquiv (C → A)) _ _ e

preCompEquiv : ∀ {ℓ ℓ′} {A B : Type ℓ} {C : Type ℓ′} (e : A ≃ B)
             → (B → C) ≃ (A → C)
preCompEquiv e = (λ φ x → φ (fst e x)) , isEquivPreComp e

postCompEquiv : ∀ {ℓ ℓ′} {A B : Type ℓ} {C : Type ℓ′} (e : A ≃ B)
             → (C → A) ≃ (C → B)
postCompEquiv e = (λ φ x → fst e (φ x)) , isEquivPostComp e

isContr-section : ∀ {ℓ} {A B : Type ℓ} (e : A ≃ B) → isContr (Σ[ g ∈ (B → A) ] section (fst e) g)
fst (isContr-section e) = invEq e , retEq e
snd (isContr-section e) (f , ε) i = (λ b → fst (p b i)) , (λ b → snd (p b i))
  where p : ∀ b → (invEq e b , retEq e b) ≡ (f b , ε b)
        p b = snd (equiv-proof (snd e) b) (f b , ε b)

-- there is a (much slower) alternate proof that also works for retract

isContr-section' : ∀ {ℓ} {A B : Type ℓ} (e : A ≃ B) → isContr (Σ[ g ∈ (B → A) ] section (fst e) g)
isContr-section' {_} {A} {B} e = transport (λ i → isContr (Σ[ g ∈ (B → A) ] eq g i))
                                           (equiv-proof (isEquivPostComp e) (idfun _))
  where eq : ∀ (g : B → A) → ((fst e) ∘ g ≡ idfun _) ≡ (section (fst e) g)
        eq g = sym (funExtPath {f = (fst e) ∘ g} {g = idfun _})

isContr-retract : ∀ {ℓ} {A B : Type ℓ} (e : A ≃ B) → isContr (Σ[ g ∈ (B → A) ] retract (fst e) g)
isContr-retract {_} {A} {B} e = transport (λ i → isContr (Σ[ g ∈ (B → A) ] eq g i))
                                           (equiv-proof (isEquivPreComp e) (idfun _))
  where eq : ∀ (g : B → A) → (g ∘ (fst e) ≡ idfun _) ≡ (retract (fst e) g)
        eq g = sym (funExtPath {f = g ∘ (fst e)} {g = idfun _})

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
module Printf where

_∘_ : {A : Set}{B : A -> Set}{C : {x : A} -> B x -> Set} ->
      (f : {x : A}(y : B x) -> C y)(g : (x : A) -> B x)(x : A) -> C (g x)
(f ∘ g) x = f (g x)

infixr 10 _::_
data List (A : Set) : Set where
  nil  : List A
  _::_ : A -> List A -> List A

{-# BUILTIN LIST    List   #-}
{-# BUILTIN NIL     nil    #-}
{-# BUILTIN CONS    _::_   #-}

[_] : {A : Set} -> A -> List A
[ x ] = x :: nil

module Primitive where

  postulate
    String : Set
    Float  : Set
    Char   : Set

  data Nat : Set where
    zero : Nat
    suc  : Nat → Nat

  data Int : Set where
    pos    : Nat → Int
    negsuc : Nat → Int

  {-# BUILTIN NATURAL Nat    #-}
  {-# BUILTIN INTEGER Int    #-}
  {-# BUILTIN INTEGERPOS pos #-}
  {-# BUILTIN INTEGERNEGSUC negsuc #-}
  {-# BUILTIN STRING  String #-}
  {-# BUILTIN FLOAT   Float  #-}
  {-# BUILTIN CHAR    Char   #-}

  private
    primitive
      primStringAppend   : String -> String -> String
      primStringToList   : String -> List Char
      primStringFromList : List Char -> String
      primShowChar       : Char -> String
      primShowInteger    : Int -> String
      primShowFloat      : Float -> String

  _++_         = primStringAppend
  showChar     = primShowChar
  showInt      = primShowInteger
  showFloat    = primShowFloat
  stringToList = primStringToList
  listToString = primStringFromList

open Primitive

data Unit : Set where
  unit : Unit

infixr 8 _×_
infixr 8 _◅_

data _×_ (A B : Set) : Set where
  _◅_ : A -> B -> A × B

data Format : Set where
  stringArg : Format
  intArg    : Format
  floatArg  : Format
  charArg   : Format
  litChar   : Char -> Format
  badFormat : Char -> Format

data BadFormat (c : Char) : Set where

format : String -> List Format
format = format' ∘ stringToList
  where
    format' : List Char -> List Format
    format' ('%' :: 's' :: fmt) = stringArg   :: format' fmt
    format' ('%' :: 'd' :: fmt) = intArg      :: format' fmt
    format' ('%' :: 'f' :: fmt) = floatArg    :: format' fmt
    format' ('%' :: 'c' :: fmt) = charArg     :: format' fmt
    format' ('%' :: '%' :: fmt) = litChar '%' :: format' fmt
    format' ('%' ::  c  :: fmt) = badFormat c :: format' fmt
    format' (c          :: fmt) = litChar c   :: format' fmt
    format'  nil                = nil

Printf' : List Format -> Set
Printf' (stringArg   :: fmt) = String  × Printf' fmt
Printf' (intArg      :: fmt) = Int     × Printf' fmt
Printf' (floatArg    :: fmt) = Float   × Printf' fmt
Printf' (charArg     :: fmt) = Char    × Printf' fmt
Printf' (badFormat c :: fmt) = BadFormat c
Printf' (litChar _   :: fmt) = Printf' fmt
Printf'  nil                 = Unit

Printf : String -> Set
Printf fmt = Printf' (format fmt)

printf : (fmt : String) -> Printf fmt -> String
printf = printf' ∘ format
  where
    printf' : (fmt : List Format) -> Printf' fmt -> String
    printf' (stringArg   :: fmt) (s ◅ args) = s                  ++ printf' fmt args
    printf' (intArg      :: fmt) (n ◅ args) = showInt n          ++ printf' fmt args
    printf' (floatArg    :: fmt) (x ◅ args) = showFloat x        ++ printf' fmt args
    printf' (charArg     :: fmt) (c ◅ args) = showChar c         ++ printf' fmt args
    printf' (litChar c   :: fmt) args       = listToString [ c ] ++ printf' fmt args
    printf' (badFormat _ :: fmt) ()
    printf'  nil                 unit       = ""