text:
-- Andreas, 2017-08-13, issue #2686
-- Overloaded constructor where only one alternative is not abstract.
-- Not ambiguous, since abstract constructors are not in scope!

-- {-# OPTIONS -v tc.check.term:40 #-}

abstract
  data A : Set where
    c : A

data D : Set where
  c : D

test = c

match : D → D
match c = c

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Prelude.Nat where

open import Prelude.Unit
open import Prelude.Empty
open import Prelude.Bool
open import Prelude.Decidable
open import Prelude.Equality
open import Prelude.Equality.Unsafe using (eraseEquality)
open import Prelude.Ord
open import Prelude.Number
open import Prelude.Semiring
open import Prelude.Function
open import Prelude.Smashed

open import Prelude.Nat.Properties
open import Prelude.Nat.Core public

--- Equality ---

private
  eqNatSound : ∀ n m → IsTrue (eqNat n m) → n ≡ m
  eqNatSound zero zero _ = refl
  eqNatSound zero (suc m) ()
  eqNatSound (suc n) zero ()
  eqNatSound (suc n) (suc m) p rewrite eqNatSound n m p = refl

  eqNatComplete : ∀ n m → IsFalse (eqNat n m) → ¬ (n ≡ m)
  eqNatComplete zero zero () eq
  eqNatComplete zero (suc m) neq ()
  eqNatComplete (suc n) zero neq ()
  eqNatComplete (suc n) (suc m) neq eq = eqNatComplete n m neq (suc-inj eq)

  decEqNat : (n m : Nat) → Dec (n ≡ m)
  decEqNat n m with eqNat n m | eqNatSound n m | eqNatComplete n m
  ... | true  | eq | _   = yes (eraseEquality (eq true))
  ... | false | _  | neq = no  (eraseNegation (neq false))
  {-# INLINE decEqNat #-}

instance
  EqNat : Eq Nat
  _==_ {{EqNat}} = decEqNat

--- Comparison ---

data LessNat n m : Set where
  diff : ∀ k (eq : m ≡ suc k +N n) → LessNat n m

{-# DISPLAY LessNat a b = a < b #-}

pattern diff! k = diff k refl

private
  lemLessNatMinus : ∀ n m → IsTrue (lessNat n m) → m ≡ suc (m - suc n) + n
  lemLessNatMinus  _       zero  ()
  lemLessNatMinus  zero   (suc m) _   = sym (suc $≡ add-zero-r m)
  lemLessNatMinus (suc n) (suc m) n<m = suc $≡ (lemLessNatMinus n m n<m ⟨≡⟩ʳ add-suc-r (m - suc n) n)

  lemNoLessEqual : ∀ n m → ¬ IsTrue (lessNat n m) → ¬ IsTrue (lessNat m n) → n ≡ m
  lemNoLessEqual zero zero _ _ = refl
  lemNoLessEqual zero (suc m) h₁ h₂ = ⊥-elim (h₁ true)
  lemNoLessEqual (suc n) zero h₁ h₂ = ⊥-elim (h₂ true)
  lemNoLessEqual (suc n) (suc m) h₁ h₂ = cong suc (lemNoLessEqual n m h₁ h₂)

  -- Using eraseEquality here lets us not worry about the performance of the
  -- proofs.
  compareNat : ∀ n m → Comparison LessNat n m
  compareNat n m with decBool (lessNat n m)
  ... | yes p = less (diff (m - suc n) (eraseEquality (lemLessNatMinus n m p)))
  ... | no np₁ with decBool (lessNat m n)
  ...             | yes p  = greater (diff (n - suc m) (eraseEquality (lemLessNatMinus m n p)))
  ...             | no np₂ = equal (eraseEquality (lemNoLessEqual n m np₁ np₂))
  {-# INLINE compareNat #-}

private
  nat-lt-to-leq : ∀ {x y} → LessNat x y → LessNat x (suc y)
  nat-lt-to-leq (diff k eq) = diff (suc k) (cong suc eq)

  nat-eq-to-leq : ∀ {x y} → x ≡ y → LessNat x (suc y)
  nat-eq-to-leq eq = diff 0 (cong suc (sym eq))

  nat-from-leq : ∀ {x y} → LessNat x (suc y) → LessEq LessNat x y
  nat-from-leq (diff zero eq)    = equal (sym (suc-inj eq))
  nat-from-leq (diff (suc k) eq) = less (diff k (suc-inj eq))

  nat-lt-antirefl : ∀ {a} → LessNat a a → ⊥
  nat-lt-antirefl {a} (diff k eq) = case add-inj₁ 0 (suc k) a eq of λ ()

  nat-lt-antisym : ∀ {a b} → LessNat a b → LessNat b a → ⊥
  nat-lt-antisym {a} (diff! k) (diff j eq) =
    case add-inj₁ 0 (suc j + suc k) a (eq ⟨≡⟩ suc $≡ add-assoc j (suc k) a) of λ ()

  nat-lt-trans : ∀ {a b c} → LessNat a b → LessNat b c → LessNat a c
  nat-lt-trans (diff k eq) (diff j eq₁) = diff (j + suc k) (eraseEquality
    (case eq of λ where refl → case eq₁ of λ where refl → add-assoc (suc j) (suc k) _))

instance
  OrdNat : Ord Nat
  Ord._<_         OrdNat = LessNat
  Ord._≤_         OrdNat a b = LessNat a (suc b)
  Ord.compare     OrdNat = compareNat
  Ord.eq-to-leq   OrdNat = nat-eq-to-leq
  Ord.lt-to-leq   OrdNat = nat-lt-to-leq
  Ord.leq-to-lteq OrdNat = nat-from-leq

  OrdNatLaws : Ord/Laws Nat
  Ord/Laws.super OrdNatLaws = it
  less-antirefl {{OrdNatLaws}} = nat-lt-antirefl
  less-trans    {{OrdNatLaws}} = nat-lt-trans

instance
  SmashedNatLess : {a b : Nat} → Smashed (a < b)
  smashed {{SmashedNatLess}} {diff! k} {diff k₁ eq} with add-inj₁ (suc k) (suc k₁) _ eq | eq
  ... | refl | refl = refl

  SmashedNatComp : {a b : Nat} → Smashed (Comparison _<_ a b)
  smashed {{SmashedNatComp}} {less _    } {less _    } = less $≡ smashed
  smashed {{SmashedNatComp}} {less lt   } {equal refl} = ⊥-elim (less-antirefl {A = Nat} lt)
  smashed {{SmashedNatComp}} {less lt   } {greater gt} = ⊥-elim (less-antisym  {A = Nat} lt gt)
  smashed {{SmashedNatComp}} {equal refl} {less lt   } = ⊥-elim (less-antirefl {A = Nat} lt)
  smashed {{SmashedNatComp}} {equal _   } {equal _   } = equal $≡ smashed
  smashed {{SmashedNatComp}} {equal refl} {greater gt} = ⊥-elim (less-antirefl {A = Nat} gt)
  smashed {{SmashedNatComp}} {greater gt} {less lt   } = ⊥-elim (less-antisym  {A = Nat} lt gt)
  smashed {{SmashedNatComp}} {greater gt} {equal refl} = ⊥-elim (less-antirefl {A = Nat} gt)
  smashed {{SmashedNatComp}} {greater _ } {greater _ } = greater $≡ smashed

suc-monotone : {a b : Nat} → a < b → Nat.suc a < suc b
suc-monotone (diff! k) = diff k (sym (add-suc-r (suc k) _))

inv-suc-monotone : ∀{t v} → suc t < suc v → t < v
inv-suc-monotone (diff! k) = diff k (add-suc-r k _)

suc-comparison : {a b : Nat} → Comparison _<_ a b → Comparison _<_ (Nat.suc a) (suc b)
suc-comparison (less lt)    = less    (suc-monotone lt)
suc-comparison (equal eq)   = equal   (suc $≡ eq)
suc-comparison (greater gt) = greater (suc-monotone gt)

ext: agda

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


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

module Oscar.Class.Congruity.Proposequality where

instance

  𝓒ongruityProposequality : ∀ {a b} → 𝓒ongruity Proposequality a b
  𝓒ongruityProposequality .𝓒ongruity.congruity _ ∅ = !

  𝓒ongruity₂Proposequality : ∀ {a b c} → 𝓒ongruity₂ Proposequality a b c
  𝓒ongruity₂Proposequality .𝓒ongruity₂.congruity₂ _ ∅ ∅ = !


text:
module Data.DynamicTree where

import      Lvl
open import Data.List
open import Data.Option
open import Functional as Fn
open import Type

private variable ℓ ℓᵢ : Lvl.Level
private variable T A B : Type{ℓ}

data Node (T : Type{ℓ}) : Type{ℓ} where
  node : T → List(Node(T)) → Node(T)

DynamicTree : Type{ℓ} → Type{ℓ}
DynamicTree(T) = Option(Node(T))

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --copatterns #-}
-- {-# OPTIONS -v tc.pos:20 -v tc.meta.eta:100 #-}
-- {-# OPTIONS -v tc.lhs:100 #-}

module LinearTemporalLogic where

import Common.Level

record Stream (A : Set) : Set where
  coinductive
  field head : A
        tail : Stream A

-- Stream properties
Proposition : Set → Set₁
Proposition A = Stream A → Set

Now : {A : Set} → (A → Set) → Proposition A
Now P s = P (Stream.head s)

-- Next time
◌ : {A : Set} → Proposition A → Proposition A
◌ P s = P (Stream.tail s)

-- Forever
record ▢ {A : Set} (P : Proposition A) (s : Stream A) : Set where
  coinductive
  field head : P s
        tail : ◌ (▢ P) s

-- Sometimes
data ◇ {A : Set} (P : Proposition A) (s : Stream A) : Set where
  now   : P s → ◇ P s
  later : ◌ (◇ P) s → ◇ P s

-- Infinitely often
▢◇ : {A : Set} → Proposition A → Proposition A
▢◇ P = ▢ (◇ P)

-- Next inf. often  implies inf. often
◌▢◇⇒▢◇ : {A : Set}{P : Proposition A}{s : Stream A} →
    ◌ (▢◇ P) s → ▢◇ P s
▢.head (◌▢◇⇒▢◇ f) = later (▢.head f)
▢.tail (◌▢◇⇒▢◇ f) = ◌▢◇⇒▢◇ (▢.tail f)

-- Forever implies inf. oft.
▢⇒▢◇ : {A : Set}{P : Proposition A}{s : Stream A} →
    ▢ P s → ▢◇ P s
▢.head (▢⇒▢◇ f) = now (▢.head f)
▢.tail (▢⇒▢◇ f) = ▢⇒▢◇ (▢.tail f)

-- Eventually
◇▢ : {A : Set} → Proposition A → Proposition A
◇▢ P = ◇ (▢ P)

-- Eventually implies inf. oft.
◇▢⇒▢◇ : {A : Set}{P : Proposition A}{s : Stream A} →
  ◇▢ P s → ▢◇ P s
◇▢⇒▢◇ (now forever) = ▢⇒▢◇ forever
◇▢⇒▢◇ (later event) = ◌▢◇⇒▢◇ (◇▢⇒▢◇ event)

-- We now prove that inf. oft. does not imply eventually
-- by exhibiting a counter example

data ⊥ : Set where
record ⊤ : Set where
  constructor tt

data Bool : Set where
  true false : Bool

True : Bool → Set
True true = ⊤
True false = ⊥

open Stream

alternate : Stream Bool
(     (head alternate)) = true
(head (tail alternate)) = false
(tail (tail alternate)) = alternate

-- alternate contains infinitely many 'true's
thm1 : ▢◇ (Now True) alternate
(        (▢.head thm1)) = now tt
(▢.head (▢.tail thm1)) = later (now tt)
(▢.tail (▢.tail thm1)) = thm1

-- alternate does not eventually contain only 'true's
mutual

  thm2 : ◇▢ (Now True) alternate → ⊥
  thm2 (now forever⊤) = ▢.head (▢.tail forever⊤)
  thm2 (later event)  = thm2′ event

  thm2′ : ◇▢ (Now True) (tail alternate) → ⊥
  thm2′ (now forever⊤) = ▢.head forever⊤
  thm2′ (later event)  = thm2 event

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module HC-Lec1 where

-- ==============================================================================
-- Lecture 1 : Programs and Proofs
-- https://www.youtube.com/watch?v=O4oczQry9Jw&t=1412s

------------------------------------------------------------------------------
-- some basic logical types

-- 13:22 -- like Haskell Void
data Zero : Set where
  -- No constructors, so no inhabitants
  -- Represents logical impossibility.

-- 16:45 -- like Haskell ()
record One : Set where
  constructor <> -- added in video Lecture 2 4:50
  -- This record has no fields.
  -- This record has exactly one inhabitant.

-- 18:42 -- like Haskell Either
data _+_ (S : Set) (T : Set) : Set where
  inl : S -> S + T -- left  constructor
  inr : T -> S + T -- right constructor

-- 24:50 -- like Haskell pair ( , )
record _*_ (S : Set) (T : Set) : Set where
  constructor _,_ -- added in video Lecture 2 4:58
  field
    fst : S
    snd : T

------------------------------------------------------------------------------
-- examples

-- 28:36
comm-* : {A : Set} {B : Set} -> A * B -> B * A
comm-* record { fst = a ; snd = b } = record { fst = b ; snd = a }

-- 43:00
assocLR-+ : {A B C : Set} -> (A + B) + C -> A + (B + C)
assocLR-+ (inl (inl a)) =      inl a
assocLR-+ (inl (inr b)) = inr (inl b)
assocLR-+      (inr c)  = inr (inr c)

-- 47:34
-- If you can arrive at a contradiction, then you can derive any conclusion.
-- Given a Zero, must produce an X for ANY X.
-- But there are no inhabitants of Zero.
-- So use 'absurd' pattern that indicates something that is IMPOSSIBLE.
naughtE : {X : Set} -> Zero -> X
naughtE ()

-- standard composition: f << g is "f after g"
_<<_ : {X Y Z : Set} -> (Y -> Z) -> (X -> Y) -> (X -> Z)
(f << g) x = f (g x)

-- diagrammatic composition: f >> g is "f then g"
_>>_ : {X Y Z : Set} -> (X -> Y) -> (Y -> Z) -> (X -> Z)
                     --       ^^^^^^^^          dominoes!
(f >> g) x = g (f x)

-- infix application
_$_ : {S : Set}{T : S -> Set}(f : (x : S) -> T x)(s : S) -> T s
f $ s = f s
infixl 2 _$_

-- ==============================================================================
-- Lecture 2 : more Programs and Proof, Introducing "with"
-- https://www.youtube.com/watch?v=qcVZxQTouDk

-- 2:25
_$*_ : {A A' B B' : Set} -> (A -> A') -> (B -> B') -> A * B -> A' * B'
(a→a' $* b→b') (a , b) = (a→a' a) , (b→b' b)

-- 6:53
_$+_ : {A A' B B' : Set} -> (A -> A') -> (B -> B') -> A + B -> A' + B'
(a→a' $+ b→b') (inl a) = inl (a→a' a)
(a→a' $+ b→b') (inr b) = inr (b→b' b)

-- 8:52 -- like Haskell const ; this is pure for applicative functor needing an E
combinatorK : {A E : Set} -> A -> E -> A
combinatorK a _ = a

-- 11:25 -- this is application
combinatorS : {S T E : Set} -> (E -> S -> T) -> (E -> S) -> E -> T
combinatorS e→s→t e→s e = e→s→t e (e→s e)

-- 14:50
idK : {X : Set} -> X -> X
idK x = combinatorK x x

-- 19:00
idSKK : {X : Set} -> X -> X
idSKK {X} = combinatorS combinatorK (combinatorK {E = X}) -- 'Zero' and 'One' also work

id : {X : Set} -> X -> X
-- id x = x -- is the easy way; let's do it a funny way to make a point
id = combinatorS combinatorK (combinatorK {_} {Zero})
--                          no choice for -^   ^^^^- could be anything

-- 30:25
-- naughtE

------------------------------------------------------------------------------
-- from logic to data

-- 32:05

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat -- recursive data type
{-# BUILTIN NATURAL Nat #-} -- enables decimal notation

-- 32:58
_+N_ : Nat -> Nat -> Nat
zero  +N y = y
suc x +N y = suc (x +N y)

four : Nat
four = 2 +N 2

------------------------------------------------------------------------------
-- and back to logic

-- 36:46
data _==_ {X : Set} : X -> X -> Set where
  refl : (x : X) -> x == x -- the relation that is "only reflexive"
{-# BUILTIN EQUALITY _==_ #-}

see4 : (2 +N 2) == 4
see4 = refl 4

-- 42:35
-- application of equalities
_=$=_ : {X Y : Set} {f f' : X -> Y} {x x' : X}
     -> f   == f'
     ->   x ==    x'
     -> f x == f' x
refl f =$= refl x = refl (f x)

------------------------------------------------------------------------------
-- computing types

-- 45:00
_>=_ : Nat -> Nat -> Set
x     >= zero  = One     -- i.e., true
zero  >= suc y = Zero    -- i.e., false
suc x >= suc y = x >= y

--a0 : 2 >= 4
--a0 = {!!}

a1 : 4 >= 2
a1 = <>

refl->= : (n : Nat) -> n >= n
refl->=  zero   = <>
refl->= (suc n) = refl->= n

trans->= : (x y z : Nat) -> x >= y -> y >= z  -> x >= z
trans->= zero     zero        z  x>=y y>=z = y>=z
trans->= (suc x)  zero    zero   x>=y y>=z = <>
trans->= (suc x) (suc y)  zero   x>=y y>=z = <>
trans->= (suc x) (suc y) (suc z) x>=y y>=z = trans->= x y z x>=y y>=z

------------------------------------------------------------------------------
-- construction by proof

-- 47:38

record Sg (S : Set) (T : S -> Set) : Set where -- Sg is short for "Sigma"
  constructor _,_
  field
    fst : S       -- a value
    snd : T fst   -- some evidence about that value

difference : (m n : Nat) -> m >= n -> Sg Nat λ d -> m == (n +N d)
difference      m   zero   m>=n = m , refl m
difference  zero   (suc n) ()
difference (suc m) (suc n) m>=n
  with difference m n m>=n
...| d , e
   = d , xxx m n d e
 where
  xxx : ∀ (m n d : Nat) -> m == (n +N d) -> suc m == suc (n +N d)
  xxx m n d p rewrite p = refl (suc (n +N d))

-- ==============================================================================
-- Lecture 3 : Proof by induction
-- https://www.youtube.com/watch?v=8xFT9FPlm18

-- 6:20
-- Nat with zero, +N and assocLR-+ form a monoid.

-- 8:48
zero-+N : (n : Nat) -> (zero +N n) == n
zero-+N n = refl n -- by definition

-- 9:36
-- version in video
-- +N-zero' : (n : Nat) -> (n +N zero) == n
-- +N-zero'  zero   = refl zero -- by definition
-- +N-zero' (suc n) = refl suc =$= +N-zero' n -- TODO : does not compile

-- HC alternate version
+N-zero : (n : Nat) -> (n +N zero) == n
+N-zero  zero   = refl zero -- by definition
+N-zero (suc n)
  with +N-zero n
...| n+N0==n
  rewrite n+N0==n
   = refl (suc n)

-- 26:00
-- version in video
-- assocLR-+N' : (x y z : Nat) -> ((x +N y) +N z) == (x +N (y +N z))
-- assocLR-+N'  zero   y z = refl (y +N z)
-- assocLR-+N' (suc x) y z = refl suc =$= assocLR-+N' x y z -- TODO : does not compile

-- 30:21
assocLR-+N : (x y z : Nat) -> ((x +N y) +N z) == (x +N (y +N z))
assocLR-+N  zero   y z = refl (y +N z)
assocLR-+N (suc x) y z
  rewrite assocLR-+N x y z
  = refl (suc (x +N (y +N z)))

------------------------------------------------------------------------------
-- computing types

-- 34:46
refl->=' : (n : Nat) -> n >= n
refl->='  zero   = <>
refl->=' (suc n) = refl->=' n

-- 41:00
trans->=' : (x y z : Nat) -> x >= y -> y >= z  -> x >= z
-- start with 'z'
trans->='      x       y   zero   x>=y y>=z = <>
trans->=' (suc x) (suc y) (suc z) x>=y y>=z = trans->=' x y z x>=y y>=z

-- ==============================================================================
-- Lecture 4 : Sigma, Difference, Vector Take
-- https://www.youtube.com/watch?v=OZeDRtRmgkw

-- 0:46 Sigma type (see above)

-- 5:10 -- make _*_ from Sg
_*'_ : (S : Set) -> (T : Set) -> Set
s *' t = Sg s λ _ -> t

-- 10:55 difference (see above)
difference' : (m n : Nat) -> m >= n -> Sg Nat λ d -> m == (n +N d)
-- 1st clause of >= matches on right, so start with 'n'
difference'      m   zero   m>=n = m , refl m
difference' (suc m) (suc n) m>=n
  with difference' m n m>=n
...| d , m==n+Nd
  rewrite m==n+Nd
  = d , refl (suc (n +N d)) -- video also uses refl suc =$= m==n+Nd

-- 27:24 -- pattern match on proof of equation ; here 'm==n+Nd'
difference'' : (m n : Nat) -> m >= n -> Sg Nat λ d -> m == (n +N d)
-- 1st clause of >= matches on right, so start with 'n'
difference''      m   zero   m>=n = m , refl m
difference'' (suc m) (suc n) m>=n
  with difference'' m n m>=n
...| d , m==n+Nd
  with m==n+Nd
... | refl .(n +N d) = d , (refl (suc (n +N d)))

tryMe     = difference 42 37
-- dontTryMe = difference 37 42 {!!}

------------------------------------------------------------------------------
-- things to remember to say

{-
-- 34:22 : = VIZ ==
=  : makes a definition (part of Agda programming language)
== : makes a type (by user built definition)

function type is both IMPLICATION and UNIVERSAL QUANTIFICATION : why call Pi?

why is Sigma called Sigma?

-- 38:50 : B or not B
must be able to return a
- inl B      for any B : not possible because nothing known about B
- inR B→Zero for any B : not possible because Zero has no elements
exMiddle : {B : Set} -> B + (B -> Zero)
exMiddle = ?

-- 40:45
-- not possible to "look inside" 'notAandB' to determine 'inl' or 'inr'
deMorgan : {A B : Set} -> ((A * B) -> Zero) -> (A -> Zero) + (B -> Zero)
deMorgan notAandB = {!!}
-}

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

-- Boilerplate for contexts and substitutions inspired by:
-- https://plfa.github.io/DeBruijn/

-- Proof technique from "How to (Re)Invent Tait's Method":
-- http://www.cs.cmu.edu/~rwh/courses/chtt/pdfs/tait.pdf

open import Data.Sum
open import Data.Product
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
open import Relation.Binary.PropositionalEquality.TrustMe using (trustMe)

infix  4 _⊢_
infix  4 _∋_

infixl 7 _·_
infix  9 `_

data Type : Set where
  unit : Type
  bool : Type
  _∧_  : Type → Type → Type
  _⊃_  : Type → Type → Type

data Ctx : Set where
  ∅   : Ctx
  _#_ : Ctx → Type → Ctx

data _∋_ : Ctx → Type → Set where
  Z  : ∀ {Γ A} → (Γ # A) ∋ A
  S_ : ∀ {Γ A B} → Γ ∋ A → (Γ # B) ∋ A

ext : ∀ {Γ Δ}
  → (∀ {A} →       Γ ∋ A →     Δ ∋ A)
    ---------------------------------
  → (∀ {A B} → Γ # B ∋ A → Δ # B ∋ A)
ext ρ Z      =  Z
ext ρ (S x)  =  S (ρ x)

data _⊢_ : Ctx → Type → Set where
  `_     : ∀ {Γ A} → Γ ∋ A → Γ ⊢ A
  ⋆      : ∀ {Γ} → Γ ⊢ unit
  yes no : ∀ {Γ} → Γ ⊢ bool
  ⟨_,_⟩  : ∀ {Γ A₁ A₂} → Γ ⊢ A₁ → Γ ⊢ A₂ → Γ ⊢ (A₁ ∧ A₂)
  fst    : ∀ {Γ A₁ A₂} → Γ ⊢ (A₁ ∧ A₂) → Γ ⊢ A₁
  snd    : ∀ {Γ A₁ A₂} → Γ ⊢ (A₁ ∧ A₂) → Γ ⊢ A₂
  ƛ      : ∀ {Γ A₁ A₂} → (Γ # A₁) ⊢ A₂ → Γ ⊢ (A₁ ⊃ A₂)
  _·_    : ∀ {Γ A₁ A₂} → Γ ⊢ (A₁ ⊃ A₂) → Γ ⊢ A₁ → Γ ⊢ A₂

rename : ∀ {Γ Δ}
  → (∀ {A} → Γ ∋ A → Δ ∋ A)
    -----------------------
  → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
rename ρ (` x)          =  ` (ρ x)
rename ρ ⋆              = ⋆
rename ρ yes            = yes
rename ρ no             = no
rename ρ ⟨ M₁ , M₂ ⟩    = ⟨ rename ρ M₁ , rename ρ M₂ ⟩
rename ρ (fst M)        = fst (rename ρ M)
rename ρ (snd M)        = snd (rename ρ M)
rename ρ (ƛ N)          = ƛ (rename (ext ρ) N)
rename ρ (L · M)        = (rename ρ L) · (rename ρ M)

Subst : (Γ Δ : Ctx) → Set
Subst Γ Δ = ∀ {A} → Γ ∋ A → Δ ⊢ A

exts : ∀ {Γ Δ} → Subst Γ Δ → ∀ {A} → Subst (Γ # A) (Δ # A)
exts σ Z      =  ` Z
exts σ (S x)  =  rename S_ (σ x)

extend : ∀ {Γ Δ A} → Δ ⊢ A → Subst Γ Δ → Subst (Γ # A) Δ
extend M γ Z     = M
extend M γ (S x) = γ x

subst : ∀ {Γ Δ} → Subst Γ Δ → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
subst σ (` x)       = σ x
subst σ ⋆           = ⋆
subst σ yes         = yes
subst σ no          = no
subst σ ⟨ M₁ , M₂ ⟩ = ⟨ subst σ M₁ , subst σ M₂ ⟩
subst σ (fst M)     = fst (subst σ M)
subst σ (snd M)     = snd (subst σ M)
subst σ (ƛ M)       = ƛ (subst (exts σ) M)
subst σ (M₁ · M₂)   = subst σ M₁ · subst σ M₂

_[_] : ∀ {Γ A B}
  → Γ # B ⊢ A
  → Γ ⊢ B
    ---------
  → Γ ⊢ A
_[_] {Γ} {A} {B} N M = subst {Γ # B} {Γ} (extend M `_) {A} N

data _final : ∀ {A} → ∅ ⊢ A → Set where
  yes  : yes final
  no   : no final
  ⋆    : ⋆ final
  pair : ∀ {A₁ A₂} → (M₁ : ∅ ⊢ A₁) → (M₂ : ∅ ⊢ A₂) → ⟨ M₁ , M₂ ⟩ final
  ƛ    : ∀ {A₁ A₂} → (M : (∅ # A₁) ⊢ A₂) → (ƛ M) final

data _↦_ : {A : Type} → ∅ ⊢ A → ∅ ⊢ A → Set where
  fst-step : ∀ {A₁ A₂} → {M M' : ∅ ⊢ A₁ ∧ A₂} → (M ↦ M') → (fst M ↦ fst M')
  snd-step : ∀ {A₁ A₂} → {M M' : ∅ ⊢ A₁ ∧ A₂} → (M ↦ M') → (snd M ↦ snd M')
  fst      : ∀ {A₁ A₂} → {M₁ : ∅ ⊢ A₁} → {M₂ : ∅ ⊢ A₂} → (fst ⟨ M₁ , M₂ ⟩ ↦ M₁)
  snd      : ∀ {A₁ A₂} → {M₁ : ∅ ⊢ A₁} → {M₂ : ∅ ⊢ A₂} → (snd ⟨ M₁ , M₂ ⟩ ↦ M₂)
  app-step : ∀ {A₁ A₂} → {M₁ M₁' : ∅ ⊢ A₁ ⊃ A₂} → {M₂ : ∅ ⊢ A₁} → (M₁ ↦ M₁') → (M₁ · M₂) ↦ (M₁' · M₂)
  app      : ∀ {A₁ A₂} → {M : ∅ # A₁ ⊢ A₂} → {M₂ : ∅ ⊢ A₁} → (ƛ M · M₂) ↦ (M [ M₂ ])

data _↦*_ : {A : Type} → ∅ ⊢ A → ∅ ⊢ A → Set where
  refl : ∀ {A} → {M : ∅ ⊢ A} → M ↦* M
  step : ∀ {A} → {M M' M'' : ∅ ⊢ A} → M ↦ M' → M' ↦* M'' → M ↦* M''

step-trans : ∀ {A} → {M M' M'' : ∅ ⊢ A} → M ↦* M' → M' ↦* M'' → M ↦* M''
step-trans refl        s₂ = s₂
step-trans (step x s₁) s₂ = step x (step-trans s₁ s₂)

compatible : ∀ {A B} → ∀ {M M' : ∅ ⊢ A} → {p : ∅ ⊢ A → ∅ ⊢ B} → (∀ {N N'} → N ↦ N' → p N ↦ p N') → M ↦* M' → p M ↦* p M'
compatible lift refl       = refl
compatible lift (step x s) = step (lift x) (compatible lift s)

ht : (A : Type) → ∅ ⊢ A → Set
ht unit      M = M ↦* ⋆
ht bool      M = (M ↦* yes) ⊎ (M ↦* no)
ht (A₁ ∧ A₂) M = ∃ λ N₁ → ∃ λ N₂ → (M ↦* ⟨ N₁ , N₂ ⟩) × (ht A₁ N₁ × ht A₂ N₂)
ht (A₂ ⊃ A)  M = ∃ λ N → (M ↦* ƛ N) × (∀ N₂ → ht A₂ N₂ → ht A (N [ N₂ ]))

HT : ∀ {Γ} → Subst Γ ∅ → Set
HT {Γ} γ = ∀ {A} → (x : Γ ∋ A) → ht A (γ x)

ht-reverse-step : ∀ {A M M'} → M ↦ M' → ht A M' → ht A M
ht-reverse-step {unit}   = step
ht-reverse-step {bool}   s = [ (inj₁ ∘ step s) , (inj₂ ∘ step s) ]
ht-reverse-step {A ∧ A₁} s (N₁ , N₂ , term , ht₁ , ht₂) = N₁ , N₂ , step s term , ht₁ , ht₂
ht-reverse-step {A ⊃ A₁} s (N , term , ht') = N , step s term , ht'

ht-reverse-steps : ∀ {A M M'} → M ↦* M' → ht A M' → ht A M
ht-reverse-steps refl       h = h
ht-reverse-steps (step x s) h = ht-reverse-step x (ht-reverse-steps s h)

-- Primary Theorem

_>>_∋_ : (Γ : Ctx) → (A : Type) → Γ ⊢ A → Set
Γ >> A ∋ M = (γ : Subst Γ ∅) → (h : HT γ) → ht A (subst γ M)

tait : ∀ {Γ A} → (M : Γ ⊢ A) → Γ >> A ∋ M
tait (` x)       γ h = h x
tait ⋆           γ h = refl
tait yes         γ h = inj₁ refl
tait no          γ h = inj₂ refl
tait ⟨ M₁ , M₂ ⟩ γ h = subst γ M₁ , subst γ M₂ , refl , tait M₁ γ h , tait M₂ γ h
tait (fst M)     γ h = let _ , _ , step-to-pair , ht-M₁ , _ = tait M γ h in
                       ht-reverse-steps (step-trans (compatible fst-step step-to-pair) (step fst refl)) ht-M₁
tait (snd M)     γ h = let _ , _ , step-to-pair , _ , ht-M₂ = tait M γ h in
                       ht-reverse-steps (step-trans (compatible snd-step step-to-pair) (step snd refl)) ht-M₂
tait (ƛ M₂)      γ h = subst (exts γ) M₂ , refl , λ M₁ ht₁ →
                         let ht₂ = tait M₂ (extend M₁ γ) λ { Z → ht₁ ; (S x) → h x } in
                         Eq.subst (ht _) trustMe ht₂  -- FIXME
tait (M₁ · M₂)   γ h = let _ , step-to-lam , ht₁ = tait M₁ γ h in
                       let ht₂ = tait M₂ γ h in
                       ht-reverse-steps (step-trans (compatible app-step step-to-lam) (step app refl)) (ht₁ (subst γ M₂) ht₂ )

-- Corollary

subst-lemma : ∀ {Γ A} → (M : Γ ⊢ A) → subst `_ M ≡ M
subst-lemma (` x)       = Eq.refl
subst-lemma ⋆           = Eq.refl
subst-lemma yes         = Eq.refl
subst-lemma no          = Eq.refl
subst-lemma ⟨ M₁ , M₂ ⟩ = Eq.cong₂ ⟨_,_⟩ (subst-lemma M₁) (subst-lemma M₂)
subst-lemma (fst M)     = Eq.cong fst (subst-lemma M)
subst-lemma (snd M)     = Eq.cong snd (subst-lemma M)
subst-lemma (ƛ M)       = trustMe  -- FIXME
subst-lemma (M₁ · M₂)   = Eq.cong₂ _·_ (subst-lemma M₁) (subst-lemma M₂)

bools-terminate : (M : ∅ ⊢ bool) → M ↦* yes ⊎ M ↦* no
bools-terminate M = Eq.subst (λ M → M ↦* yes ⊎ M ↦* no) (subst-lemma M) (tait M `_ (λ {_} ()))


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

module Algebra.Construct.Free.Semilattice.Extensionality where

open import Prelude

open import Algebra.Construct.Free.Semilattice.Definition
open import Algebra.Construct.Free.Semilattice.Eliminators
open import Algebra.Construct.Free.Semilattice.Relation.Unary
open import Algebra.Construct.Free.Semilattice.Union

open import HITs.PropositionalTruncation.Sugar
import HITs.PropositionalTruncation as PropTrunc
open import HITs.PropositionalTruncation.Properties

open import Path.Reasoning

infix 4 _↭_
_↭_ : 𝒦 A → 𝒦 A → Type _
xs ↭ ys = ∀ x → x ∈ xs ↔ x ∈ ys

in-cons : (x : A) (xs : 𝒦 A) → x ∈ xs → xs ≡ x ∷ xs
in-cons = λ x → ∥ in-cons′ x ∥⇓
  where
  in-cons′ : ∀ x → xs ∈𝒦 A ⇒∥ (x ∈ xs → xs ≡ x ∷ xs) ∥
  ∥ in-cons′ y ∥-prop {xs} p q i y∈xs = trunc xs (y ∷ xs) (p y∈xs) (q y∈xs) i
  ∥ in-cons′ y ∥[] ()
  ∥ in-cons′ y ∥ x ∷ xs ⟨ Pxs ⟩ = PropTrunc.rec (trunc _ _)
    λ { (inl x≡y) → sym (dup x xs) ; cong (_∷ x ∷ xs) x≡y
      ; (inr y∈xs) → cong (x ∷_) (Pxs y∈xs) ; com x y xs
      }

subset-ext : ∀ xs ys → (∀ (x : A) → x ∈ xs → x ∈ ys) → xs ∪ ys ≡ ys
subset-ext = ∥ subset-ext′ ∥⇓
  where
  subset-ext′ : xs ∈𝒦 A ⇒∥ (∀ ys → (∀ x → x ∈ xs → x ∈ ys) → xs ∪ ys ≡ ys) ∥
  ∥ subset-ext′ ∥-prop {xs} p q i ys perm = trunc (xs ∪ ys) ys (p ys perm) (q ys perm) i
  ∥ subset-ext′ ∥[] _ _ = refl
  ∥ subset-ext′ ∥ x ∷ xs ⟨ Pxs ⟩ ys perm =
    (x ∷ xs) ∪ ys ≡⟨ cons-distrib-∪ x xs ys ⟩
    xs ∪ (x ∷ ys) ≡⟨ Pxs (x ∷ ys) (λ y y∈xs → ∣ inr (perm y ∣ inr y∈xs ∣) ∣) ⟩
    x ∷ ys ≡˘⟨ in-cons x ys (perm x ∣ inl refl ∣) ⟩
    ys ∎

extensional : (xs ys : 𝒦 A) → (xs ↭ ys) → xs ≡ ys
extensional xs ys xs↭ys =
  xs ≡˘⟨ subset-ext ys xs (inv ∘ xs↭ys) ⟩
  ys ∪ xs ≡⟨ ∪-comm ys xs ⟩
  xs ∪ ys ≡⟨ subset-ext xs ys (fun ∘ xs↭ys) ⟩
  ys ∎

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
{-
  My first Proof in Agda
-}

-- define Natural numbers

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

-- Simply defining 1
one : ℕ
one = suc(zero)

two : ℕ
two = suc(suc(zero))

-- define addition of natural numbers

_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)

-- Define equality

data _≡_ {A : Set} (a : A) : A → Set where
  refl : a ≡ a

-- small test for equality

-- oneplusoneistwo : one + one ≡ two
-- oneplusoneistwo = refl

-- Prove n+0 = n

max_stars_repo_name: adithyaselv/Learn-Agda

max_issues_repo_name: adithyaselv/Learn-Agda

max_forks_repo_name: adithyaselv/Learn-Agda


text:
{-# OPTIONS --allow-unsolved-metas #-}

open import Agda.Primitive using (lzero; lsuc; _⊔_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; subst; setoid)
open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂; zip; map; <_,_>; swap)
import Function.Equality
-- open import Relation.Binary using (Setoid)
-- import Relation.Binary.Reasoning.Setoid as SetoidR

import Categories.Category
import Categories.Functor
import Categories.Category.Instance.Setoids
import Categories.Monad.Relative
import Categories.Category.Equivalence
import Categories.Category.Cocartesian
import Categories.Category.Construction.Functors
import Categories.Category.Product
import Categories.NaturalTransformation
import Categories.NaturalTransformation.NaturalIsomorphism

import SecondOrder.Arity
import SecondOrder.Signature
import SecondOrder.Metavariable
import SecondOrder.VRenaming
import SecondOrder.MRenaming
import SecondOrder.Term
import SecondOrder.Substitution
import SecondOrder.RelativeMonadMorphism
import SecondOrder.Instantiation
import SecondOrder.IndexedCategory
import SecondOrder.RelativeKleisli

module SecondOrder.Mslot
  {ℓ}
  {𝔸 : SecondOrder.Arity.Arity}
  (Σ : SecondOrder.Signature.Signature ℓ 𝔸)
  where

  open SecondOrder.Signature.Signature Σ
  open SecondOrder.Metavariable Σ
  open SecondOrder.Term Σ
  open SecondOrder.VRenaming Σ
  open SecondOrder.MRenaming Σ
  -- open SecondOrder.Substitution Σ
  -- open import SecondOrder.RelativeMonadMorphism
  -- open SecondOrder.Instantiation
  open Categories.Category
  open Categories.Functor using (Functor)
  open Categories.NaturalTransformation renaming (id to idNt)
  open Categories.NaturalTransformation.NaturalIsomorphism renaming (refl to reflNt; sym to symNt; trans to transNt)
  open Categories.Category.Construction.Functors
  open Categories.Category.Instance.Setoids
  open Categories.Category.Product
  open Function.Equality using () renaming (setoid to Π-setoid)
  open SecondOrder.IndexedCategory
  -- open import SecondOrder.RelativeKleisli

  MTele = MContexts
  VTele = VContexts

  -- the codomain category of the MSlots functor. It should be equivalent to the
  -- functor category [ MTele x VTele , < Setoid >ₛₒᵣₜ ]
  -- objects are functors, which are really pairs of functions, one on objects
  -- one on morphisms
  -- morphisms in this category are natural transformations

  module _ where
    open Category
    open NaturalTransformation
    open Function.Equality renaming (_∘_ to _∙_)

  Mslots : Functor MContexts (IndexedCategory VContext (IndexedCategory sort (Setoids ℓ ℓ)))
  Mslots =
    let open Categories.NaturalTransformation in
    let open NaturalTransformation in
    let open Relation.Binary.PropositionalEquality.≡-Reasoning in
      record
        { F₀ = λ Θ Γ A → setoid ([ Γ , A ]∈ Θ)
        ; F₁ = λ ι Γ A → record { _⟨$⟩_ = λ M → ι M ; cong = λ M≡N → cong ι M≡N }
        ; identity = λ {Θ} Γ A {M} {N} M≡N → cong idᵐ M≡N
        ; homomorphism = λ {Θ} {Ψ} {Ξ} {ι} {μ} Γ A M≡N → cong (μ ∘ᵐ ι) M≡N
        ; F-resp-≈ = λ {Θ} {Ψ} {ι} {μ} ι≡ᵐμ Γ A {M} {N} M≡N →
                   begin
                   ι M ≡⟨ cong ι M≡N ⟩
                   ι N ≡⟨ ι≡ᵐμ N ⟩
                   μ N
                   ∎
        }

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: cilinder/formaltt

max_forks_repo_name: cilinder/formaltt


text:
module STLC3 where

open import Data.Nat
open import Data.Nat.Properties using (≤-antisym; ≤-trans; ≰⇒>)
-- open import Data.List
open import Data.Empty using (⊥-elim)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; cong₂; subst)
open import Relation.Nullary.Decidable using (map)
open import Relation.Nullary
open import Data.Product

-- de Bruijn indexed lambda calculus
infix  5 ƛ_
infixl 7 _∙_
infix  9 var_

-- indexed by the number of binders out there
data Term : ℕ → Set where
  -- if x < n
  --  then var x is bound
  --  else var x is free
  var_ : ∀ {n} → (x : ℕ) → Term n

  ƛ_ : ∀ {n} → Term (suc n) → Term n

  _∙_ : ∀ {n} → Term n → Term n → Term n

data Var : Set where
  Bound : ∀ {n x} → (bound : n > x) → Var
  FreeIncr : ∀ {n x depth} → (free : suc x ≰ n) → (prop : depth ≡ suc x) → Var
  Free : ∀ {n x depth} →(free : suc x ≰ n) → (safe : suc x ≰ depth) → Var

sort : (n x depth : ℕ) → suc n ≥ depth → Var
sort n x depth P with n >? x
sort n x depth P | yes p = Bound p
sort n x depth P | no ¬p with depth >? x
sort n x depth P | no ¬p | yes q = FreeIncr ¬p (≤-antisym (≤-trans P (≰⇒> ¬p)) q)
sort n x depth P | no ¬p | no ¬q = Free ¬p ¬q

-- only "shift" the variable when
--  1. it's free
--  2. it will be captured after substitution
shift : ∀ {n} → (i : ℕ) → suc n ≥ i → Term n → Term (suc n)
shift {n} depth P (var x) with sort n x depth P
shift {n} depth P (var x) | Bound bound = var x
shift {n} depth P (var x) | FreeIncr free prop = var suc x
shift {n} depth P (var x) | Free free safe = var x
shift depth P (ƛ M) = ƛ shift (suc depth) (s≤s P) M
shift depth P (M ∙ N) = shift depth P M ∙ shift depth P N

infixl 10 _[_/_/_]
_[_/_/_] : ∀ {n} → Term (suc n) → Term n → (i : ℕ) → n ≥ i → Term n
(var x)   [ N / i / n≥i ] with x ≟ i
(var x)   [ N / i / n≥i ] | yes p = N
(var x)   [ N / i / n≥i ] | no ¬p = var x
(ƛ M)     [ N / i / n≥i ] = ƛ (M [ shift (suc i) (s≤s n≥i) N / suc i / s≤s n≥i ])
(L ∙ M)   [ N / i / n≥i ] = L [ N / i / n≥i ] ∙ M [ N / i / n≥i ]

-- substitution
infixl 10 _[_]
_[_] : ∀ {n} → Term (suc n) → Term n → Term n
M [ N ] = M [ N / zero / z≤n ]

-- β reduction
infix 3 _β→_
data _β→_ {n : ℕ} : Term n → Term n → Set where

  β-ƛ-∙ : ∀ {M N} → ((ƛ M) ∙ N) β→ M [ N ]

  β-ƛ : ∀ {M N} → M β→ N → ƛ M β→ ƛ N

  β-∙-l : ∀ {L M N} → M β→ N → M ∙ L β→ N ∙ L

  β-∙-r : ∀ {L M N} → M β→ N → L ∙ M β→ L ∙ N

-- the reflexive and transitive closure of _β→_
infix  2 _β→*_
infixr 4 _→*_
data _β→*_ {n : ℕ} : Term n → Term n → Set where

  ∎ : ∀ {M} → M β→* M

  _→*_ : ∀ {L M N}
    → L β→  M
    → M β→* N
    --------------
    → L β→* N

infixl  3 _<β>_
_<β>_ : ∀ {n} {M N O : Term n} → M β→* N → N β→* O → M β→* O
∎          <β> N→O = N→O
L→M →* M→N <β> N→O = L→M →* (M→N <β> N→O)

hop : ∀ {n} {M N : Term n} → M β→ N → M β→* N
hop M→N = M→N →* ∎

-- infix  2 _-↠_

infixr 2 _→⟨_⟩_
_→⟨_⟩_
  : ∀ {n} {M N : Term n}
  → ∀ L
  → L β→ M
  → M β→* N
  --------------
  → L β→* N
L →⟨ P ⟩ Q = P →* Q

infixr 2 _→*⟨_⟩_
_→*⟨_⟩_
  : ∀ {n} {M N : Term n}
  → ∀ L
  → L β→* M
  → M β→* N
  --------------
  → L β→* N
L →*⟨ P ⟩ Q = P <β> Q

infix 3 _→∎
_→∎ : ∀ {n} (M : Term n) → M β→* M
M →∎ = ∎

-- the symmetric closure of _β→*_

infix  1 _β≡_
data _β≡_ {n : ℕ} : Term n → Term n → Set where
  β-sym : ∀ {M N}
    → M β→* N
    → N β→* M
    -------
    → M β≡ N

infixr 2 _=*⟨_⟩_
_=*⟨_⟩_
  : ∀ {n} {M N : Term n}
  → ∀ L
  → L β≡ M
  → M β≡ N
  --------------
  → L β≡ N
L =*⟨ β-sym A B ⟩ β-sym C D = β-sym (A <β> C) (D <β> B)

infixr 2 _=*⟨⟩_
_=*⟨⟩_
  : ∀ {n} {N : Term n}
  → ∀ L
  → L β≡ N
  --------------
  → L β≡ N
L =*⟨⟩ β-sym C D = β-sym C D

infix 3 _=∎
_=∎ : ∀ {n} → (M : Term n) → M β≡ M
M =∎ = β-sym ∎ ∎

forward : ∀ {n} {M N : Term n} → M β≡ N → M β→* N
forward (β-sym A _) = A

backward : ∀ {n} {M N : Term n} → M β≡ N → N β→* M
backward (β-sym _ B) = B

-- data Normal : Set where

Normal : ∀ {n} → Term n → Set
Normal M = ¬ ∃ (λ N → M β→ N)

normal : ∀ {n} {M N : Term n} → Normal M → M β→* N → M ≡ N
normal P ∎            = refl
normal P (M→L →* L→N) = ⊥-elim (P (_ , M→L))

cong-ƛ : ∀ {n} {M N : Term (suc n)} → M β→* N → ƛ M β→* ƛ N
cong-ƛ ∎            = ∎
cong-ƛ (M→N →* N→O) = β-ƛ M→N →* cong-ƛ N→O

cong-∙-l : ∀ {n} {L M N : Term n} → M β→* N → M ∙ L β→* N ∙ L
cong-∙-l ∎            = ∎
cong-∙-l (M→N →* N→O) = β-∙-l M→N →* cong-∙-l N→O

cong-∙-r : ∀ {n} {L M N : Term n} → M β→* N → L ∙ M β→* L ∙ N
cong-∙-r ∎            = ∎
cong-∙-r (M→N →* N→O) = β-∙-r M→N →* cong-∙-r N→O

cong-shift! : ∀ {n i} (M : Term (suc n)) (N : Term n) → (n≥i : n ≥ i) → shift (suc i) (s≤s n≥i) ((ƛ M) ∙ N) β→ shift (suc i) (s≤s n≥i) (M [ N ])
cong-shift! (var x) N n≥i = {!   !}
cong-shift! (ƛ M) N n≥i = {!   !}
cong-shift! (M ∙ L) N n≥i = {!   !}

cong-shift : ∀ {n i} {M N : Term n} → (n≥i : n ≥ i) → M β→ N → shift (suc i) (s≤s n≥i) M β→ shift (suc i) (s≤s n≥i) N
cong-shift n≥i (β-ƛ-∙ {M} {N}) = cong-shift! M N n≥i
cong-shift n≥i (β-ƛ M→N) = β-ƛ (cong-shift (s≤s n≥i) M→N)
cong-shift n≥i (β-∙-l M→N) = β-∙-l (cong-shift n≥i M→N)
cong-shift n≥i (β-∙-r M→N) = β-∙-r (cong-shift n≥i M→N)

-- cong-shift : ∀ {n i} {M N : Term n} → n ≥ i → M β→ N → shift (suc i) M β→ shift (suc i) N
-- cong-shift {n} n≥i (β-ƛ-∙ {var x} {var y}) with suc n >? x
-- cong-shift {n} n≥i (β-ƛ-∙ {var x} {var y}) | yes p with suc y ≤? n
-- cong-shift {n} n≥i (β-ƛ-∙ {var zero} {var y}) | yes p | yes q with n >? y
-- cong-shift {n} n≥i (β-ƛ-∙ {var zero} {var y}) | yes p | yes q | yes r = β-ƛ-∙
-- cong-shift {n} n≥i (β-ƛ-∙ {var zero} {var y}) | yes p | yes q | no ¬r = ⊥-elim (¬r q)
-- cong-shift {n} n≥i (β-ƛ-∙ {var suc x} {var y}) | yes p | yes q with n >? suc x
-- cong-shift {n} n≥i (β-ƛ-∙ {var suc x} {var y}) | yes p | yes q | yes r = {!   !} -- dump
-- cong-shift {n} {i} n≥i (β-ƛ-∙ {var suc x} {var y}) | yes p | yes q | no ¬r with suc i >? suc x
-- -- ≤-antisym p
-- cong-shift {n} {i} n≥i (β-ƛ-∙ {var suc x} {var y}) | yes p | yes q | no ¬r | yes s = {! (≰⇒> ¬r)  !} -- fishy
-- cong-shift {n} {i} n≥i (β-ƛ-∙ {var suc x} {var y}) | yes p | yes q | no ¬r | no ¬s = {!   !} -- dump
-- cong-shift {n} {i} n≥i (β-ƛ-∙ {var x} {var y}) | yes p | no ¬q with suc i >? y
-- cong-shift {n} {i} n≥i (β-ƛ-∙ {var zero} {var y}) | yes p | no ¬q | yes r with n >? y
-- cong-shift {n} {i} n≥i (β-ƛ-∙ {var zero} {var y}) | yes p | no ¬q | yes r | yes s = ⊥-elim (¬q s)
-- cong-shift {n} {i} n≥i (β-ƛ-∙ {var zero} {var y}) | yes p | no ¬q | yes r | no ¬s with suc i >? y
-- cong-shift {n} {i} n≥i (β-ƛ-∙ {var zero} {var y}) | yes p | no ¬q | yes r | no ¬s | yes t = β-ƛ-∙
-- cong-shift {n} {i} n≥i (β-ƛ-∙ {var zero} {var y}) | yes p | no ¬q | yes r | no ¬s | no ¬t = ⊥-elim (¬t r)
-- cong-shift {n} {i} n≥i (β-ƛ-∙ {var suc x} {var y}) | yes p | no ¬q | yes r with n >? suc x
-- cong-shift {n} {i} n≥i (β-ƛ-∙ {var suc x} {var y}) | yes p | no ¬q | yes r | yes t = {!   !} -- dump
-- cong-shift {n} {i} n≥i (β-ƛ-∙ {var suc x} {var y}) | yes p | no ¬q | yes r | no ¬t with suc i >? suc x
-- cong-shift {n} {i} n≥i (β-ƛ-∙ {var suc x} {var y}) | yes p | no ¬q | yes r | no ¬t | yes u = {!   !} -- fishy
-- cong-shift {n} {i} n≥i (β-ƛ-∙ {var suc x} {var y}) | yes p | no ¬q | yes r | no ¬t | no ¬u = β-ƛ-∙
-- cong-shift {n} {i} n≥i (β-ƛ-∙ {var x} {var y}) | yes p | no ¬q | no ¬r = {!   !}
-- cong-shift {n} n≥i (β-ƛ-∙ {var x} {var y}) | no ¬p = {!   !}
-- cong-shift {n} n≥i (β-ƛ-∙ {var x} {ƛ N}) = {!   !}
-- cong-shift {n} n≥i (β-ƛ-∙ {var x} {N ∙ O}) = {!   !}
-- -- cong-shift {n} (β-ƛ-∙ {var x} {N}) with suc n >? x
-- -- cong-shift {n} (β-ƛ-∙ {var zero} {N}) | yes p = β-ƛ-∙
-- -- cong-shift {n} (β-ƛ-∙ {var suc x} {N}) | yes (s≤s p) with n >? suc x
-- -- cong-shift {n} (β-ƛ-∙ {var suc x} {N}) | yes (s≤s p) | yes q = {!   !}
-- -- cong-shift {n} {i} (β-ƛ-∙ {var suc x} {N}) | yes (s≤s p) | no ¬q with suc i >? suc x
-- -- cong-shift {n} {i} (β-ƛ-∙ {var suc x} {N}) | yes (s≤s p) | no ¬q | yes r = {!   !} -- fishy
-- -- cong-shift {n} {i} (β-ƛ-∙ {var suc x} {N}) | yes (s≤s p) | no ¬q | no ¬r = {!   !}
-- -- cong-shift {n} (β-ƛ-∙ {var zero} {var x}) | no ¬p = {!   !}
-- -- cong-shift {n} (β-ƛ-∙ {var zero} {ƛ N}) | no ¬p = {!   !}
-- -- cong-shift {n} (β-ƛ-∙ {var zero} {N ∙ O}) | no ¬p = {!   !}
-- -- cong-shift {n} (β-ƛ-∙ {var suc x} {N}) | no ¬p = {!   !}
-- cong-shift n≥i (β-ƛ-∙ {ƛ M} {N}) = {!   !}
-- cong-shift n≥i (β-ƛ-∙ {L ∙ var x} {N}) = {!   !}
-- cong-shift n≥i (β-ƛ-∙ {L ∙ (ƛ M)} {N}) = {!   !}
-- cong-shift n≥i (β-ƛ-∙ {L ∙ (M ∙ K)} {N}) = {!   !}
-- cong-shift n≥i (β-ƛ M→N) = β-ƛ (cong-shift _ M→N)
-- cong-shift n≥i (β-∙-l M→N) = β-∙-l (cong-shift _ M→N)
-- cong-shift n≥i (β-∙-r M→N) = β-∙-r (cong-shift _ M→N)

-- -- cong-[] : ∀ {n i} {M N : Term n} → (L : Term (suc n)) → M β→ N → L [ M / i ] β→* L [ N / i ]
-- -- cong-[] {i = i} (var x) M→N with x ≟ i
-- -- cong-[] {i = i} (var x) M→N | yes p = hop M→N
-- -- cong-[] {i = i} (var x) M→N | no ¬p = ∎
-- -- cong-[] {n} {i} (ƛ L) M→N = {!   !}
-- --   -- cong-ƛ (cong-[] L (cong-shift M→N))
-- -- cong-[] {i = i} {M} {N} (L ∙ K) M→N =
-- --     L [ M / i ] ∙ K [ M / i ]
-- --   →*⟨ cong-∙-l (cong-[] L M→N) ⟩
-- --     L [ N / i ] ∙ K [ M / i ]
-- --   →*⟨ cong-∙-r (cong-[] K M→N) ⟩
-- --     L [ N / i ] ∙ K [ N / i ]
-- --   →∎

-- cong-[]2 : ∀ {n i} {M N : Term n} → (L : Term (suc n)) → n ≥ i → M β→ N → L [ M / i ] β→* L [ N / i ]
-- cong-[]2 {n} {i} (var x) n≥i M→N with x ≟ i
-- cong-[]2 {n} {i} (var x) n≥i M→N | yes p = hop M→N
-- cong-[]2 {n} {i} (var x) n≥i M→N | no ¬p = ∎
-- cong-[]2 {n} {i} (ƛ M)   n≥i M→N = cong-ƛ (cong-[]2 M (s≤s n≥i) {! cong-shift  !})
-- cong-[]2 {n} {i} {M} {N} (L ∙ K) n≥i M→N =
--     L [ M / i ] ∙ K [ M / i ]
--   →*⟨ cong-∙-l (cong-[]2 L _ M→N) ⟩
--     L [ N / i ] ∙ K [ M / i ]
--   →*⟨ cong-∙-r (cong-[]2 K _ M→N) ⟩
--     L [ N / i ] ∙ K [ N / i ]
--   →∎

-- β→confluent :  ∀ {n} (M N O : Term n) → (M β→ N) → (M β→ O) → ∃ (λ P → (N β→* P) × (O β→* P))
-- β→confluent .((ƛ M) ∙ N) _ _ (β-ƛ-∙ {M} {N}) β-ƛ-∙ = (M [ N ]) , (∎ , ∎)
-- β→confluent .((ƛ M) ∙ N) _ .(O ∙ N) (β-ƛ-∙ {M} {N}) (β-∙-l {N = O} M→O) = (O ∙ N) , ({!   !} , ∎)
-- β→confluent .((ƛ M) ∙ N) _ .((ƛ M) ∙ O) (β-ƛ-∙ {M} {N}) (β-∙-r {N = O} N→O) = (M [ O ]) , (cong-[]2 M z≤n N→O , (hop β-ƛ-∙))
-- β→confluent .(ƛ M) .(ƛ N) .(ƛ O) (β-ƛ {M} {N} M→N) (β-ƛ {N = O} M→O) with β→confluent M N O M→N M→O
-- β→confluent .(ƛ M) .(ƛ N) .(ƛ O) (β-ƛ {M} {N} M→N) (β-ƛ {N = O} M→O) | P , N→P , O→P = (ƛ P) , ((cong-ƛ N→P) , (cong-ƛ O→P))
-- β→confluent .((ƛ M) ∙ L) .(N ∙ L) _ (β-∙-l {L} {N = N} M→N) (β-ƛ-∙ {M}) = (N ∙ L) , (∎ , {!   !})
-- β→confluent .(M ∙ L) .(N ∙ L) .(K ∙ L) (β-∙-l {L} {M} {N} M→N) (β-∙-l {N = K} M→O) with β→confluent M N K M→N M→O
-- β→confluent .(M ∙ L) .(N ∙ L) .(K ∙ L) (β-∙-l {L} {M} {N} M→N) (β-∙-l {N = K} M→O) | P , N→P , K→P = P ∙ L , ((cong-∙-l N→P) , cong-∙-l K→P)
-- β→confluent .(M ∙ L) .(N ∙ L) .(M ∙ K) (β-∙-l {L} {M} {N} M→N) (β-∙-r {N = K} M→O) = N ∙ K , hop (β-∙-r M→O) , hop (β-∙-l M→N)
-- β→confluent .((ƛ L) ∙ M) .((ƛ L) ∙ N) _ (β-∙-r {M = M} {N} M→N) (β-ƛ-∙ {L}) = (L [ N ]) , (hop β-ƛ-∙ , cong-[]2 L _ M→N)
-- β→confluent .(K ∙ M) .(K ∙ N) .(L ∙ M) (β-∙-r {K} {M} {N} M→N) (β-∙-l {N = L} K→L) = (L ∙ N) , ((hop (β-∙-l K→L)) , hop (β-∙-r M→N))
-- β→confluent .(_ ∙ M) .(_ ∙ N) .(_ ∙ O) (β-∙-r {M = M} {N} M→N) (β-∙-r {N = O} M→O) with β→confluent M N O M→N M→O
-- β→confluent .(L ∙ M) .(L ∙ N) .(L ∙ O) (β-∙-r {L} {M} {N} M→N) (β-∙-r {N = O} M→O) | P , N→P , O→P = (L ∙ P) , (cong-∙-r N→P , cong-∙-r O→P)

-- β→*-confluent :  ∀ {n} {M N O : Term n} → (M β→* N) → (M β→* O) → ∃ (λ P → (N β→* P) × (O β→* P))
-- β→*-confluent {n} {M} {.M} {O} ∎            M→O          = O , M→O , ∎
-- β→*-confluent {n} {M} {N} {.M} (M→L →* L→N) ∎            = N , ∎   , (M→L →* L→N)
-- β→*-confluent {n} {M} {N} {O}  (M→L →* L→N) (M→K →* K→O) = {!   !}

-- normal-unique : ∀ {n} {M N O : Term n} → Normal N → Normal O → M β→* N → M β→* O → N ≡ O
-- normal-unique P Q M→N M→O = let X = β→*-confluent M→N M→O in trans (normal P (proj₁ (proj₂ X))) (sym (normal Q (proj₂ (proj₂ X))))

max_stars_repo_name: banacorn/bidirectional

max_issues_repo_name: banacorn/bidirectional

max_forks_repo_name: banacorn/bidirectional


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Vector equality over propositional equality
------------------------------------------------------------------------

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

open import Relation.Binary

module Data.Vec.Relation.Binary.Equality.Propositional {a} {A : Set a} where

open import Data.Nat.Base using (ℕ; zero; suc; _+_)
open import Data.Vec
open import Data.Vec.Relation.Binary.Pointwise.Inductive
  using (Pointwise-≡⇒≡; ≡⇒Pointwise-≡)
import Data.Vec.Relation.Binary.Equality.Setoid as SEq
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- Publically re-export everything from setoid equality

open SEq (setoid A) public

------------------------------------------------------------------------
-- ≋ is propositional

≋⇒≡ : ∀ {n} {xs ys : Vec A n} → xs ≋ ys → xs ≡ ys
≋⇒≡ = Pointwise-≡⇒≡

≡⇒≋ : ∀ {n} {xs ys : Vec A n} → xs ≡ ys → xs ≋ ys
≡⇒≋ = ≡⇒Pointwise-≡

-- See also Data.Vec.Relation.Binary.Equality.Propositional.WithK.≋⇒≅.


text:
module Issue589 where

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

_+_ : N -> N -> N
zero + y = y
suc x + y = suc ?


text:
module neq where

open import eq
open import negation

----------------------------------------------------------------------
-- syntax
----------------------------------------------------------------------

infix 4 _≢_

----------------------------------------------------------------------
-- defined types
----------------------------------------------------------------------

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

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
{-# OPTIONS --without-K --safe #-}
module Cats.Functor.Const where

open import Function using (const)

open import Cats.Category
open import Cats.Functor using (Functor)

module _ {lo la l≈ lo′ la′ l≈′}
  (C : Category lo la l≈) {D : Category lo′ la′ l≈′}
  where

  open Category D

  Const : Obj → Functor C D
  Const d = record
    { fobj = const d
    ; fmap = const id
    ; fmap-resp = const ≈.refl
    ; fmap-id = ≈.refl
    ; fmap-∘ = id-l
    }

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


text:
module Epic where

data Nat : Set where
  Z : Nat
  S : Nat -> Nat

_+_ : Nat -> Nat -> Nat
Z + m = m
S n + m = S (n + m)

_*_ : Nat -> Nat -> Nat
Z * m = Z
S n * m = m + (n * m)

{-# BUILTIN NATURAL Nat #-}
{-# BUILTIN NATPLUS _+_ #-}
{-# BUILTIN NATTIMES _*_ #-}

data Unit : Set where
  unit : Unit

postulate
  IO         : Set -> Set
  printNat   : Nat -> IO Unit

{-# COMPILED_EPIC printNat (a : BigInt, u : Unit) -> Unit = putStrLn (bigIntToStr(a)) #-}

main : IO Unit
main = printNat (7 * 191)

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some properties about signs
------------------------------------------------------------------------

module Data.Sign.Properties where

open import Data.Empty
open import Function
open import Data.Sign
open import Relation.Binary.PropositionalEquality

-- The opposite of a sign is not equal to the sign.

opposite-not-equal : ∀ s → s ≢ opposite s
opposite-not-equal - ()
opposite-not-equal + ()

-- Sign multiplication is right cancellative.

cancel-*-right : ∀ s₁ s₂ {s} → s₁ * s ≡ s₂ * s → s₁ ≡ s₂
cancel-*-right - - _  = refl
cancel-*-right - + eq = ⊥-elim (opposite-not-equal _ $ sym eq)
cancel-*-right + - eq = ⊥-elim (opposite-not-equal _ eq)
cancel-*-right + + _  = refl


text:
module Cats.Category.Constructions.Mono where

open import Level

open import Cats.Category.Base

module Build {lo la l≈} (Cat : Category lo la l≈) where

  private open module Cat = Category Cat
  open Cat.≈-Reasoning

  IsMono : ∀ {A B} → A ⇒ B → Set (lo ⊔ la ⊔ l≈)
  IsMono {A} f = ∀ {C} {g h : C ⇒ A} → f ∘ g ≈ f ∘ h → g ≈ h

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Functor where

open import Level
open import Relation.Binary using (IsEquivalence)
open import Relation.Binary.PropositionalEquality
  using ()
  renaming (_≡_ to _≣_)
open import Relation.Nullary using (¬_)
open import Data.Product using (Σ; _×_; ∃; proj₁)
open import Categories.Category
open import Categories.Functor.Core public
import Categories.Morphisms as Morphisms

infix  4 _≡_

_≡_ : ∀ {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} → (F G : Functor C D) → Set (e′ ⊔ ℓ′ ⊔ ℓ ⊔ o)
_≡_ {C = C} {D} F G = ∀ {A B} → (f : C [ A , B ]) → Functor.F₁ F f ∼ Functor.F₁ G f
  where open Heterogeneous D

≡⇒≣ : ∀ {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′}
  → (F G : Functor C D)
  → F ≡ G
  → (∀ x → Functor.F₀ F x ≣ Functor.F₀ G x)
≡⇒≣ {C = C} {D} F G F≡G x = domain-≣ (F≡G (Category.id C {x}))
  where
    open Heterogeneous D

.assoc : ∀ {o₀ ℓ₀ e₀ o₁ ℓ₁ e₁ o₂ ℓ₂ e₂ o₃ ℓ₃ e₃}
           {C₀ : Category o₀ ℓ₀ e₀} {C₁ : Category o₁ ℓ₁ e₁} {C₂ : Category o₂ ℓ₂ e₂} {C₃ : Category o₃ ℓ₃ e₃}
           {F : Functor C₀ C₁} {G : Functor C₁ C₂} {H : Functor C₂ C₃}
       → (H ∘ G) ∘ F ≡ H ∘ (G ∘ F)
assoc {C₃ = C₃} f = refl
  where open Heterogeneous C₃

.identityˡ : ∀ {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {F : Functor C D} → id ∘ F ≡ F
identityˡ {C = C} {D} {F} f = refl
  where open Heterogeneous D

.identityʳ : ∀ {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {F : Functor C D} → F ∘ id ≡ F
identityʳ {C = C} {D} {F} f = refl
  where open Heterogeneous D

.equiv : ∀ {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} → IsEquivalence (_≡_ {C = C} {D = D})
equiv {C = C} {D} = record
  { refl = λ f → refl
  ; sym = λ F∼G f → sym (F∼G f)
  ; trans = λ F∼G G∼H f → trans (F∼G f) (G∼H f)
  }
  where open Heterogeneous D

.∘-resp-≡  : ∀ {o₀ ℓ₀ e₀ o₁ ℓ₁ e₁ o₂ ℓ₂ e₂}
               {A : Category o₀ ℓ₀ e₀} {B : Category o₁ ℓ₁ e₁} {C : Category o₂ ℓ₂ e₂}
               {F H : Functor B C} {G I : Functor A B}
           → F ≡ H → G ≡ I → F ∘ G ≡ H ∘ I
∘-resp-≡ {B = B} {C} {F} {I = I} F≡H G≡I q = helper (G≡I q) (F≡H (Functor.F₁ I q))
  where
  open Heterogeneous C
  module C = Category C
  helper : ∀ {a b c d} {z w} {f : B [ a , b ]} {h : B [ c , d ]} {i : C [ z , w ]}
         → B [ f ∼ h ] → C [ Functor.F₁ F h ∼ i ] → C [ Functor.F₁ F f ∼ i ]
  helper (≡⇒∼ f≡h) (≡⇒∼ g≡i) = ≡⇒∼ (C.Equiv.trans (Functor.F-resp-≡ F f≡h) g≡i)

Faithful : ∀ {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} → Functor C D → Set (o ⊔ ℓ ⊔ e ⊔ e′)
Faithful {C = C} {D} F = ∀ {X Y} → (f g : C [ X , Y ]) → D [ F₁ f ≡ F₁ g ] → C [ f ≡ g ]
  where
  module C = Category C
  module D = Category D
  open Functor F

-- Is this convoluted double-negated definition really necessary? A naive constructive definition of surjectivity
-- requires a right inverse, which would probably restrict the things we can provide proofs for
Full : ∀ {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} → Functor C D → Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′)
Full {C = C} {D} F = ∀ {X Y} → ¬ Σ (D [ F₀ X , F₀ Y ]) (λ f → ¬ Σ (C [ X , Y ]) (λ g → D [ F₁ g ≡ f ]))
  where
  module C = Category C
  module D = Category D
  open Functor F

FullyFaithful : ∀ {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} → Functor C D → Set (o ⊔ ℓ ⊔ e ⊔ ℓ′ ⊔ e′)
FullyFaithful F = Full F × Faithful F

{-
[02:22:21 AM] <ddarius> copumpkin: So I think the normal statement is fine.  You should be requiring F_1 to be a setoid function, i.e. forall x ~ x'. f(x) ~ f(x').  The function that would be required by the forall y.exists x. ... is not a setoid function and thus doesn't necessarily produce an inverse.  That is, you'll have a function g such that f(g(y)) ~ y but not necessarily f(g(y)) = y and it is not necessary that for y ~ y' that
[02:22:22 AM] <ddarius> g(y) ~ g(y'), they could be different w.r.t. the domain setoid as long as f still maps them to equivalent elements in the codomain.
[02:27:53 AM] <ddarius> For example, let f : 2/= -> 2/~ (where True ~ False).  Then, we need g(True) and g(False) and we could use g = not, even though True /= False and f(g(y)) /= y (assuming say f is id on the carrier), because it is still the case that f(g(y)) ~ y.
[02:28:55 AM] <ddarius> So g isn't an inverse on the carrier sets, and g isn't a setoid function inverse because it's not even a setoid function.
-}

EssentiallySurjective : ∀ {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} → Functor C D → Set _
EssentiallySurjective {D = D} F = ∀ d → ∃ (λ c → F₀ c ≅ d)
  where
  open Functor F
  open Morphisms D

max_stars_repo_name: p-pavel/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


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

module Path where

open import Cubical.Foundations.Everything
  using ( _≡_
        ; sym
        ; refl
        ; subst
        ; transport
        ; Path
        ; PathP
        ; I
        ; i0
        ; i1
        ; funExt
        ; cong
        ; toPathP
        ; cong₂
        ; ~_
        ; _∧_
        ; _∨_
        ; hcomp
        ; transp
        ; J
        )
  renaming (_∙_ to _;_; subst2 to subst₂)
  public

open import Data.Empty using (¬_)
open import Level

infix 4 _≢_
_≢_ : {A : Type a} → A → A → Type a
x ≢ y = ¬ (x ≡ y)

infix 4 PathP-syntax
PathP-syntax = PathP
{-# DISPLAY PathP-syntax = PathP #-}

syntax PathP-syntax (λ i → Ty) lhs rhs = lhs ≡[ i ≔ Ty ]≡ rhs

import Agda.Builtin.Equality as MLTT

builtin-eq-to-path : {A : Type a} {x y : A} → x MLTT.≡ y → x ≡ y
builtin-eq-to-path {x = x} MLTT.refl i = x

path-to-builtin-eq : {A : Type a} {x y : A} → x ≡ y → x MLTT.≡ y
path-to-builtin-eq {x = x} x≡y = subst (x MLTT.≡_) x≡y MLTT.refl

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Fin Literals
------------------------------------------------------------------------

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

module Data.Fin.Literals where

open import Agda.Builtin.FromNat
open import Data.Nat using (suc; _≤?_)
open import Data.Fin using (Fin ; #_)
open import Relation.Nullary.Decidable using (True)

number : ∀ n → Number (Fin n)
number n = record
  { Constraint = λ m → True (suc m ≤? n)
  ; fromNat    = λ m {{pr}} → (# m) {n} {pr}
  }


text:
------------------------------------------------------------------------
-- A theorem related to pointwise equality
------------------------------------------------------------------------

-- To simplify the development, let's work with actual natural numbers
-- as variables and constants (see
-- Atom.one-can-restrict-attention-to-χ-ℕ-atoms).

open import Atom

open import Chi            χ-ℕ-atoms
open import Coding         χ-ℕ-atoms
open import Free-variables χ-ℕ-atoms

import Coding.Instances.Nat

-- The results are stated and proved under the assumption that a
-- correct self-interpreter can be implemented.

module Pointwise-equality
  (eval : Exp)
  (cl-eval : Closed eval)
  (eval-correct₁ : ∀ p v → Closed p → p ⇓ v → apply eval ⌜ p ⌝ ⇓ ⌜ v ⌝)
  where

open import Equality.Propositional
open import Prelude hiding (const; Decidable)

open import Bag-equivalence equality-with-J
open import Equality.Decision-procedures equality-with-J
open import H-level.Closure equality-with-J

open import Computability χ-ℕ-atoms
open import Constants     χ-ℕ-atoms
open import Reasoning     χ-ℕ-atoms
open import Values        χ-ℕ-atoms

open Computable-function
open χ-atoms χ-ℕ-atoms

open import Combinators hiding (id; if_then_else_)

-- Pointwise equality of computable functions to Bool.

Pointwise-equal :
  ∀ {a} (A : Type a) ⦃ rA : Rep A Consts ⦄ →
  let F = Computable-function A Bool Bool-set in
  (F × F) →Bool
Pointwise-equal _ =
  as-function-to-Bool₁
    (λ { (f , g) → ∀ x → function f x ≡ function g x })

-- Pointwise equality of computable functions from Bool to Bool is
-- decidable.

pointwise-equal-Bool : Decidable (Pointwise-equal Bool)
pointwise-equal-Bool =
  total→almost-computable→computable
    id
    id
    (proj₁ (Pointwise-equal Bool))
    total
    ( pointwise-equal
    , closed
    , correct
    )
  where
  F = Computable-function Bool Bool Bool-set

  pointwise-equal′ : F × F → Bool
  pointwise-equal′ (f , g) =
    (if function f true  Bool.≟ function g true  then true else false)
      ∧
    (if function f false Bool.≟ function g false then true else false)

  total : Total id (proj₁ (Pointwise-equal Bool))
  total p@(f , g) = result , true-lemma , false-lemma
    where
    result = pointwise-equal′ p

    true-lemma : (∀ b → function f b ≡ function g b) → result ≡ true
    true-lemma hyp
      with function f true Bool.≟ function g true | hyp true
    ... | no  f≢g | f≡g = ⊥-elim (f≢g f≡g)
    ... | yes _   | _
      with function f false Bool.≟ function g false | hyp false
    ... | no  f≢g | f≡g = ⊥-elim (f≢g f≡g)
    ... | yes _   | _   = refl

    false-lemma : ¬ (∀ b → function f b ≡ function g b) → result ≡ false
    false-lemma hyp
      with function f true  Bool.≟ function g true
         | function f false Bool.≟ function g false
    ... | yes ft≡gt | yes ff≡gf = ⊥-elim $ hyp Prelude.[ (λ _ → ft≡gt)
                                                       , (λ _ → ff≡gf)
                                                       ]
    ... | yes _     | no  _     = refl
    ... | no  _     | yes _     = refl
    ... | no  _     | no  _     = refl

  infix 10 _at_

  _at_ : Exp → Bool → Exp
  f at b =
    decode-Bool
      (apply eval (const c-apply (f ∷ ⌜ ⌜ b ⌝ ⦂ Exp ⌝ ∷ [])))

  test : Bool → Exp
  test b = equal-Bool (var v-f at b) (var v-g at b)

  pointwise-equal : Exp
  pointwise-equal =
    lambda v-p (case (var v-p) (
      branch c-pair (v-f ∷ v-g ∷ [])
        (and (test true) (test false)) ∷ []))

  -- This proof could have been simplified if eval had been a concrete
  -- implementation, rather than a variable.

  closed : Closed pointwise-equal
  closed =
    Closed′-closed-under-lambda $
    Closed′-closed-under-case
      (Closed′-closed-under-var (inj₁ refl))
      (λ where
        (inj₁ refl) → and-closed (test-closed true) (test-closed false)
        (inj₂ ()))
    where
    variables = v-f ∷ v-g ∷ v-p ∷ []

    at-closed : ∀ f b → f ∈ variables → Closed′ variables (var f at b)
    at-closed f b f∈ =
      decode-Bool-closed $
      Closed′-closed-under-apply
        (Closed→Closed′ cl-eval)
        (Closed′-closed-under-const λ where
           _ (inj₁ refl)        → Closed′-closed-under-var f∈
           _ (inj₂ (inj₁ refl)) → Closed→Closed′ $
                                  rep-closed (⌜ b ⌝ ⦂ Exp)
           _ (inj₂ (inj₂ ())))

    test-closed : ∀ b → Closed′ variables (test b)
    test-closed b =
      equal-Bool-closed
        (at-closed v-f b (from-⊎ (V.member v-f variables)))
        (at-closed v-g b (from-⊎ (V.member v-g variables)))

  at-correct :
    ∀ (f : F) b → ⌜ f ⌝ at b ⇓ ⌜ function f b ⌝
  at-correct f b = decode-Bool-correct (function f b) (
    apply eval ⌜ apply (proj₁ (computable f)) ⌜ b ⌝ ⦂ Exp ⌝  ⇓⟨ eval-correct₁
                                                                  (apply (proj₁ $ computable f) ⌜ b ⌝)
                                                                  ⌜ function f b ⌝
                                                                  (Closed′-closed-under-apply
                                                                     (proj₁ $ proj₂ $ computable f)
                                                                     (rep-closed b))
                                                                  (proj₁ (proj₂ $ proj₂ $ computable f)
                                                                     b
                                                                     (function f b)
                                                                     (lift refl)) ⟩■
    ⌜ ⌜ function f b ⌝ ⦂ Exp ⌝)

  test-correct :
    ∀ b (f g : F) →
    test b [ v-g ← ⌜ g ⌝ ] [ v-f ← ⌜ f ⌝ ] ⇓
    ⌜ if function f b Bool.≟ function g b then true else false ⌝
  test-correct b f g =
    equal-Bool-correct (function f b) (function g b)

      (var v-f at b [ v-g ← ⌜ g ⌝ ] [ v-f ← ⌜ f ⌝ ]  ≡⟨ lemma ⌜ f ⌝ ⟩⟶
       ⌜ f ⌝ at b                                    ⇓⟨ at-correct f b ⟩■
       ⌜ function f b ⌝)

      (var v-g at b [ v-g ← ⌜ g ⌝ ] [ v-f ← ⌜ f ⌝ ]  ≡⟨ lemma (⌜ g ⌝ [ v-f ← ⌜ f ⌝ ]) ⟩⟶
       (⌜ g ⌝ [ v-f ← ⌜ f ⌝ ]) at b                  ≡⟨ cong (_at b) (subst-rep g) ⟩⟶
       ⌜ g ⌝ at b                                    ⇓⟨ at-correct g b ⟩■
       ⌜ function g b ⌝)
    where
    ss = (v-f , ⌜ f ⌝) ∷ (v-g , ⌜ g ⌝) ∷ []

    lemma : ∀ _ → _
    lemma = λ e →
      cong₂ (λ e₁ e₂ → decode-Bool (apply e₁ (const _ (e ∷ e₂ ∷ []))))
        (substs-closed eval cl-eval ss)
        (substs-rep (⌜ b ⌝ ⦂ Exp) ss)

  correct :
    ∀ p b →
    proj₁ (Pointwise-equal Bool) [ p ]= b →
    apply pointwise-equal ⌜ p ⌝ ⇓ ⌜ b ⌝
  correct p@(f , g) b [p]=b =
    apply pointwise-equal ⌜ p ⌝                               ⟶⟨ apply lambda (rep⇓rep p) ⟩

    case ⌜ p ⌝ (
      branch c-pair (v-f ∷ v-g ∷ [])
        (and (test true) (test false) [ v-p ← ⌜ p ⌝ ]) ∷ [])  ≡⟨ cong₂ (λ e₁ e₂ → case ⌜ p ⌝ (branch c-pair (v-f ∷ v-g ∷ []) (and e₁ e₂) ∷ []))
                                                                   (test-lemma true)
                                                                   (test-lemma false) ⟩⟶
    case ⌜ p ⌝ (
      branch c-pair (v-f ∷ v-g ∷ [])
        (and (test true) (test false)) ∷ [])                  ⟶⟨ case (rep⇓rep p) here (∷ ∷ []) ⟩

    and (test true  [ v-g ← ⌜ g ⌝ ] [ v-f ← ⌜ f ⌝ ])
        (test false [ v-g ← ⌜ g ⌝ ] [ v-f ← ⌜ f ⌝ ])          ⇓⟨ and-correct (if function f true  Bool.≟ function g true  then true else false)
                                                                             (if function f false Bool.≟ function g false then true else false)
                                                                             (test-correct true f g) (test-correct false f g) ⟩

    ⌜ pointwise-equal′ p ⌝                                    ≡⟨ cong ⌜_⌝ (_⇀_.deterministic (proj₁ (Pointwise-equal Bool)) {a = p}
                                                                                (proj₂ (total p)) [p]=b) ⟩⟶
    ⌜ b ⌝                                                     ■⟨ rep-value b ⟩

    where

    at-lemma :
      ∀ b f → v-p ≢ f → var f at b [ v-p ← ⌜ p ⌝ ] ≡ var f at b
    at-lemma b f p≢f =
      var f at b [ v-p ← ⌜ p ⌝ ]                                          ≡⟨⟩

      decode-Bool (apply (eval [ v-p ← ⌜ p ⌝ ]) (const c-apply
        (var f [ v-p ← ⌜ p ⌝ ] ∷ ⌜ ⌜ b ⌝ ⦂ Exp ⌝ [ v-p ← ⌜ p ⌝ ] ∷ [])))  ≡⟨ cong (λ e → decode-Bool (apply e (const _
                                                                                (var f [ v-p ← ⌜ p ⌝ ] ∷
                                                                                ⌜ ⌜ b ⌝ ⦂ Exp ⌝ [ v-p ← ⌜ p ⌝ ] ∷ []))))
                                                                               (subst-closed v-p ⌜ p ⌝ cl-eval) ⟩
      decode-Bool (apply eval (const c-apply
        (var f [ v-p ← ⌜ p ⌝ ] ∷ ⌜ ⌜ b ⌝ ⦂ Exp ⌝ [ v-p ← ⌜ p ⌝ ] ∷ [])))  ≡⟨ cong (λ e → decode-Bool (apply _ (const _ (e ∷ _))))
                                                                               (subst-∉ v-p (var f) λ { (var p≡f) → p≢f p≡f }) ⟩
      decode-Bool (apply eval (const c-apply
        (var f ∷ ⌜ ⌜ b ⌝ ⦂ Exp ⌝ [ v-p ← ⌜ p ⌝ ] ∷ [])))                  ≡⟨ cong (λ e → decode-Bool (apply _ (const _ (_ ∷ e ∷ _))))
                                                                               (subst-rep (⌜ b ⌝ ⦂ Exp)) ⟩
      decode-Bool (apply eval (const c-apply
        (var f ∷ ⌜ ⌜ b ⌝ ⦂ Exp ⌝ ∷ [])))                                  ≡⟨⟩

      var f at b                                                          ∎

    test-lemma : ∀ b → test b [ v-p ← ⌜ p ⌝ ] ≡ test b
    test-lemma b =
      cong₂ equal-Bool (at-lemma b v-f (λ ())) (at-lemma b v-g (λ ()))

max_stars_repo_name: nad/chi

max_issues_repo_name: nad/chi

max_forks_repo_name: nad/chi


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Machine words
------------------------------------------------------------------------

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

module Data.Word where

------------------------------------------------------------------------
-- Re-export built-ins publically

open import Agda.Builtin.Word public
  using (Word64)
  renaming
  ( primWord64ToNat   to toℕ
  ; primWord64FromNat to fromℕ
  )


text:
module examplesPaperJFP.SpaceShipCell where

open import SizedIO.Base
open import StateSizedIO.GUI.BaseStateDependent

open import Data.Bool.Base
open import Data.List.Base
open import Data.Integer

open import Data.Product hiding (map)
open import SizedIO.Object
open import SizedIO.IOObject

open import NativeIO
open import Sized.SimpleCell hiding (main; program)

open import StateSizedIO.GUI.WxBindingsFFI
open import StateSizedIO.GUI.VariableList

open import StateSizedIO.GUI.WxGraphicsLib

open import StateSized.GUI.BitMaps

VarType  = Object (cellJ ℤ)

cellℤC : (z : ℤ ) → VarType
objectMethod (cellℤC z) get       = (  z     ,  cellℤC z   )
objectMethod (cellℤC z) (put z′)  = (  unit  ,  cellℤC z′  )

varInit : VarType
varInit = cellℤC (+ 150)

onPaint  : ∀{i} → VarType   → DC → Rect → IO GuiLev1Interface i VarType

onPaint c dc rect =
  let (z , c₁) = objectMethod c get                in
  exec  (drawBitmap dc ship (z , (+ 150)) true)  λ _ →
  return c₁

moveSpaceShip : ∀{i} → Frame → VarType
                     → IO GuiLev1Interface i VarType

moveSpaceShip fra c =
  let  (z  ,  c₁)  =  objectMethod c   get
       (_  ,  c₂)  =  objectMethod c₁  (put (z + (+ 20)))
  in   return c₂

callRepaint  : ∀{i} → Frame → VarType → IO GuiLev1Interface i VarType

callRepaint fra c = exec (repaint fra) λ _ →  return c

program : ∀{i} → IOˢ GuiLev2Interface i (λ _ → Unit) []
program =  execˢ (level1C makeFrame)           λ fra →
           execˢ (level1C (makeButton fra))    λ bt →
           execˢ (level1C (addButton fra bt))  λ _ →
           execˢ (createVar varInit)  λ _ →
           execˢ (setButtonHandler bt (moveSpaceShip fra
                                     ∷ [ callRepaint fra ])) λ _ →
           execˢ (setOnPaint       fra [ onPaint  ])
           returnˢ

main : NativeIO Unit
main = start (translateLev2 program)

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of interleaving using setoid equality
------------------------------------------------------------------------

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

open import Relation.Binary using (Setoid)

module Data.List.Relation.Ternary.Interleaving.Setoid.Properties
  {c ℓ} (S : Setoid c ℓ) where

open import Data.List.Base using (List; []; _∷_; filter; _++_)
open import Relation.Unary using (Decidable)
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Negation using (¬?)
open import Function

open import Data.List.Relation.Binary.Equality.Setoid S using (≋-refl)
open import Data.List.Relation.Ternary.Interleaving.Setoid S
open Setoid S renaming (Carrier to A)

------------------------------------------------------------------------
-- Re-exporting existing properties

open import Data.List.Relation.Ternary.Interleaving.Properties public

------------------------------------------------------------------------
-- _++_

++-linear : (xs ys : List A) → Interleaving xs ys (xs ++ ys)
++-linear xs ys = ++-disjoint (left ≋-refl) (right ≋-refl)

------------------------------------------------------------------------
-- filter

module _ {p} {P : A → Set p} (P? : Decidable P) where

  filter⁺ : ∀ xs → Interleaving (filter P? xs) (filter (¬? ∘ P?) xs) xs
  filter⁺ []       = []
  filter⁺ (x ∷ xs) with P? x
  ... | yes px = refl ∷ˡ filter⁺ xs
  ... | no ¬px = refl ∷ʳ filter⁺ xs


text: module Algebra.Linear.Category.Vect where

max_stars_repo_name: felko/linear-algebra

max_issues_repo_name: felko/linear-algebra

max_forks_repo_name: felko/linear-algebra


text:
module Issue309a where

data D : Set where
  d : D → D

syntax d x x = e x

g : D → D
g (d x) = e x

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --rewriting #-}

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

{-# BUILTIN REWRITE _≡_ #-}

postulate
  admit : ∀ {ℓ} {A : Set ℓ} → A
  X : Set

postulate
  Wrap : Set → Set

  wrap : {A : Set} → A → Wrap A

  rec : (A : Set) (P : Set) → (A → P) → Wrap A → P

  Rec : (A : Set) (P : Set₁) → (A → P) → Wrap A → P

  Rec-β : {A : Set} (P : Set₁) → ∀ f → (a : A) → Rec A P f (wrap a) ≡ f a

  {-# REWRITE Rec-β #-} -- bug disappears without this

record Σ {ℓ} (A : Set ℓ) (B : A → Set) : Set ℓ where
  constructor _,_
  field
    fst : A
    snd : B fst

open Σ public

-- bug disappears if Comp or isFib is not wrapped in a record

record Comp (A : X → Set) : Set where
  field
    comp : ∀ s → A s

open Comp public

record isFib {Γ : Set} (A : Γ → Set) : Set where
  field
    lift : (p : X → Γ) → Comp (λ x → A (p x))

open isFib public

compSys : (ψ : X → Set)
  (A : Σ X (λ x → Wrap (ψ x)) → Set)
  (u : ∀ s → Wrap (ψ s)) (s : X)
  → A (s , u s)
compSys ψ A u s =
  rec (∀ i → ψ i) (A (s , u s))
    (λ v →
      subst (λ s → wrap (v s)) (λ s → u s) admit
      .lift (λ s → s) .comp s)
    admit
  where
  subst : (w w' : ∀ i → Wrap (ψ i)) → isFib (λ s → A (s , w s)) → isFib (λ s → A (s , w' s))
  subst = admit

-- bug disappears if ×id is inlined
×id : {A A' : Set} {B : A' → Set} (f : A → A') → Σ A (λ x → B (f x)) → Σ A' B
×id f (a , b) = (f a , b)

fib : (ψ : X → Set) (A : Σ X (λ x → Wrap (ψ x)) → Set) → isFib A
fib ψ A .lift p .comp =
  compSys (λ x → ψ (p x .fst)) (λ xu → A (×id (λ x → p x .fst) xu)) (λ x → p x .snd)

-- bug seems to disappear if the underscore in (Σ Set _) is filled in
template : (ψ : X → Set) → X → Σ (Σ X (λ x → Wrap (ψ x)) → Set) isFib
template ψ n =
  (_ , fib ψ (λ b → Rec (ψ (b .fst)) (Σ Set _) (λ _ → admit) (b .snd) .fst))

eq : {B : Set₁} (f : X → B) {x y : X} → f x ≡ f y
eq = admit

templateEq : (ψ : X → Set) (n₀ : X) → template ψ n₀ ≡ template ψ n₀
templateEq ψ n₀ = eq (template ψ)


text:
module Builtin.Size where

open import Agda.Builtin.Size public

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
{-# OPTIONS --without-K #-}
open import HoTT.Base
open import HoTT.Equivalence

module HoTT.Identity.Boolean where

private
  variable
    x y : 𝟐

_=𝟐_ : 𝟐 → 𝟐 → 𝒰₀
0₂ =𝟐 0₂ = 𝟏
0₂ =𝟐 1₂ = 𝟎
1₂ =𝟐 0₂ = 𝟎
1₂ =𝟐 1₂ = 𝟏

=𝟐-equiv : x == y ≃ x =𝟐 y
=𝟐-equiv = f , qinv→isequiv (g , η , ε)
  where
  f : x == y → x =𝟐 y
  f {0₂} p = transport (0₂ =𝟐_) p ★
  f {1₂} p = transport (1₂ =𝟐_) p ★
  g : x =𝟐 y → x == y
  g {0₂} {0₂} _ = refl
  g {0₂} {1₂} ()
  g {1₂} {0₂} ()
  g {1₂} {1₂} _ = refl
  η : g ∘ f {x} {y} ~ id
  η {0₂} refl = refl
  η {1₂} refl = refl
  ε : f ∘ g {x} {y} ~ id
  ε {0₂} {0₂} ★ = refl
  ε {0₂} {1₂} ()
  ε {1₂} {0₂} ()
  ε {1₂} {1₂} ★ = refl

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


text:
open import Categories.Category
open import Categories.Category.CartesianClosed

open import Theory

module Categories.Category.Construction.Models
  {ℓ₁ ℓ₂ ℓ₃}
  (Th : Theory.Theory ℓ₁ ℓ₂ ℓ₃)
  {o ℓ e}
  (𝒞 : Category o ℓ e)
  (cartesianClosed : CartesianClosed 𝒞)
  where

  open import Categories.Category.Cartesian 𝒞
  open import Categories.Category.BinaryProducts 𝒞
  open import Categories.Object.Terminal 𝒞
  import Categories.Object.Product 𝒞 as P
  open import Categories.Morphism 𝒞
  open import Categories.Functor.Construction.Product using (Product)
  open import Categories.Functor.Construction.Exponential using (Exp)
  open import Categories.Functor.Properties using ([_]-resp-≅)

  open Category 𝒞
  open CartesianClosed cartesianClosed
  open Cartesian cartesian
  open BinaryProducts products
  module T = Terminal terminal
  open HomReasoning
  open import Categories.Morphism.Reasoning 𝒞

  open import Syntax
  open Theory.Theory Th
  open import Semantics 𝒞 cartesianClosed Sg
  open Signature Sg

  open import Data.Product using (Σ; Σ-syntax; proj₁; proj₂; _,_)

  open import Relation.Binary using (Rel; IsEquivalence)

  open import Level using (_⊔_)

  ⁂-id : forall {A B} -> id {A = A} ⁂ id {A = B} ≈ id
  ⁂-id = Equiv.trans (⟨⟩-cong₂ identityˡ identityˡ) η

  module Homomorphism {M N : Model 𝒞 cartesianClosed Th}
    (h : (g : Gr) -> ⟦ g ⟧G (proj₁ M) ≅ ⟦ g ⟧G (proj₁ N))
    where
    open _≅_
    open Iso

    H : (A : Type) -> ⟦ A ⟧T (proj₁ M) ≅ ⟦ A ⟧T (proj₁ N)
    H ⌊ g ⌋ = h g
    H Unit = up-to-iso terminal terminal
    H (A * A₁) = [ Product 𝒞 cartesian ]-resp-≅
      (record
        { from = from (H A) , from (H A₁)
        ; to = to (H A) , to (H A₁)
        ; iso = record { isoˡ = isoˡ (iso (H A)) , isoˡ (iso (H A₁)) ; isoʳ = isoʳ (iso (H A)) , isoʳ (iso (H A₁)) }
        })
    H (A => A₁) = [ Exp 𝒞 cartesianClosed ]-resp-≅
      (record
        { from = from (H A₁) , to (H A)
        ; to = to (H A₁) , from (H A)
        ; iso = record { isoˡ = isoˡ (iso (H A₁)) , isoˡ (iso (H A)) ; isoʳ = isoʳ (iso (H A₁)) , isoʳ (iso (H A)) }
        })

  record homomorphism (M N : Model 𝒞 cartesianClosed Th) : Set (ℓ₁ ⊔ ℓ₂ ⊔ ℓ ⊔ e) where
    field
      h : (g : Gr) -> ⟦ g ⟧G (proj₁ M) ≅ ⟦ g ⟧G (proj₁ N)

    open Homomorphism {M} {N} h public

    field
      comm : (f : Func) -> _≅_.from (H (cod f)) ∘ ⟦ f ⟧F (proj₁ M) ≈ ⟦ f ⟧F (proj₁ N) ∘ _≅_.from (H (dom f))

  module _ {M N : Model 𝒞 cartesianClosed Th} where
    _≗_ : Rel (homomorphism M N) (ℓ₁ ⊔ e)
    _≗_ x y = (g : Gr) -> _≅_.from (homomorphism.h x g) ≈ _≅_.from (homomorphism.h y g)

  module Id {M : Model 𝒞 cartesianClosed Th} where
    open Homomorphism {M} {M} (λ _ → IsEquivalence.refl ≅-isEquivalence)
    open Structure (proj₁ M)

    -- The components of the homomorphism generated by identity morphisms are also identities.
    H-id : forall A -> _≅_.from (H A) ≈ Category.id 𝒞
    H-id˘ : forall A -> _≅_.to (H A) ≈ Category.id 𝒞

    H-id ⌊ x ⌋ = Equiv.refl
    H-id Unit = T.!-unique (Category.id 𝒞)
    H-id (A * A₁) =
      begin
        _≅_.from (H A) ⁂ _≅_.from (H A₁)
      ≈⟨ ⁂-cong₂ (H-id A) (H-id A₁) ⟩
        Category.id 𝒞 ⁂ Category.id 𝒞
      ≈⟨ ⟨⟩-cong₂ identityˡ identityˡ ⟩
        ⟨ π₁ , π₂ ⟩
      ≈⟨ η ⟩
        Category.id 𝒞
      ∎
    H-id (A => A₁) =
      begin
        λg (_≅_.from (H A₁) ∘ eval′ ∘ (id ⁂ _≅_.to (H A)))
      ≈⟨ λ-cong (∘-resp-≈ˡ (H-id A₁)) ⟩
        λg (id ∘ eval′ ∘ (id ⁂ _≅_.to (H A)))
      ≈⟨ λ-cong (pullˡ identityˡ) ⟩
        λg (eval′ ∘ (id ⁂ _≅_.to (H A)))
      ≈⟨ λ-cong (∘-resp-≈ʳ (⁂-cong₂ Equiv.refl (H-id˘ A))) ⟩
        λg (eval′ ∘ (id ⁂ id))
      ≈⟨ λ-cong (elimʳ ⁂-id) ⟩
        λg eval′
      ≈⟨ η-id′ ⟩
        id
      ∎

    H-id˘ ⌊ x ⌋ = Equiv.refl
    H-id˘ Unit = T.!-unique id
    H-id˘ (A * A₁) =
      begin
        _≅_.to (H A) ⁂ _≅_.to (H A₁)
      ≈⟨ ⁂-cong₂ (H-id˘ A) (H-id˘ A₁) ⟩
        id ⁂ id
      ≈⟨ ⁂-id ⟩
        id
      ∎
    H-id˘ (A => A₁) =
      begin
        λg (_≅_.to (H A₁) ∘ eval′ ∘ (id ⁂ _≅_.from (H A)))
      ≈⟨ λ-cong (elimˡ (H-id˘ A₁)) ⟩
        λg (eval′ ∘ (id ⁂ _≅_.from (H A)))
      ≈⟨ λ-cong (∘-resp-≈ʳ (⁂-cong₂ Equiv.refl (H-id A))) ⟩
        λg (eval′ ∘ (id ⁂ id))
      ≈⟨ λ-cong (elimʳ ⁂-id) ⟩
        λg eval′
      ≈⟨ η-id′ ⟩
        id
      ∎

    comm : (f : Func) -> _≅_.from (H (cod f)) ∘ ⟦ f ⟧F ≈ ⟦ f ⟧F ∘ _≅_.from (H (dom f))
    comm f =
      begin
        _≅_.from (H (cod f)) ∘ ⟦ f ⟧F
      ≈⟨ elimˡ (H-id (cod f)) ⟩
        ⟦ f ⟧F
      ≈˘⟨ elimʳ (H-id (dom f)) ⟩
        ⟦ f ⟧F ∘ _≅_.from (H (dom f))
      ∎

    id′ : homomorphism M M
    id′ = record { h = λ _ → IsEquivalence.refl ≅-isEquivalence ; comm = comm }

  module Compose {M N O : Model 𝒞 cartesianClosed Th} where
    open _≅_

    compose : homomorphism N O -> homomorphism M N -> homomorphism M O
    compose x y = record
      { h = h
      ; comm = λ f →
          begin
            from (MO.H (cod f)) ∘ ⟦ f ⟧F (proj₁ M)
          ≈⟨ pushˡ (H-compose (cod f)) ⟩
            from (NO.H (cod f)) ∘ from (MN.H (cod f)) ∘ ⟦ f ⟧F (proj₁ M)
          ≈⟨ ∘-resp-≈ʳ (MN.comm f) ⟩
            from (NO.H (cod f)) ∘ ⟦ f ⟧F (proj₁ N) ∘ from (MN.H (dom f))
          ≈⟨ pullˡ (NO.comm f) ⟩
            (⟦ f ⟧F (proj₁ O) ∘ from (NO.H (dom f))) ∘ from (MN.H (dom f))
          ≈˘⟨ pushʳ (H-compose (dom f)) ⟩
            ⟦ f ⟧F (proj₁ O) ∘ from (MO.H (dom f))
          ∎
      }
      where
        h = λ g → IsEquivalence.trans ≅-isEquivalence (homomorphism.h y g) (homomorphism.h x g)
        module MO = Homomorphism h
        module MN = homomorphism y
        module NO = homomorphism x

        H-compose : forall A -> from (MO.H A) ≈ from (NO.H A) ∘ from (MN.H A)
        H-compose˘ : forall A -> to (MO.H A) ≈ to (MN.H A) ∘ to (NO.H A)

        H-compose ⌊ x ⌋ = Equiv.refl
        H-compose Unit = T.!-unique₂
        H-compose (A * A₁) = Equiv.trans (⁂-cong₂ (H-compose A) (H-compose A₁)) (Equiv.sym ⁂∘⁂)
        H-compose (A => A₁) =
          begin
            λg (from (MO.H A₁) ∘ eval′ ∘ (id ⁂ to (MO.H A)))
          ≈⟨ λ-cong (∘-resp-≈ˡ (H-compose A₁)) ⟩
            λg ((from (NO.H A₁) ∘ from (MN.H A₁)) ∘ eval′ ∘ (id ⁂ to (MO.H A)))
          ≈⟨ λ-cong assoc ⟩
            λg (from (NO.H A₁) ∘ from (MN.H A₁) ∘ eval′ ∘ (id ⁂ to (MO.H A)))
          ≈⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ʳ (∘-resp-≈ʳ (⁂-cong₂ Equiv.refl (H-compose˘ A))))) ⟩
            λg (from (NO.H A₁) ∘ from (MN.H A₁) ∘ eval′ ∘ (id ⁂ to (MN.H A) ∘ to (NO.H A)))
          ≈˘⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ʳ (∘-resp-≈ʳ second∘second))) ⟩
            λg (from (NO.H A₁) ∘ from (MN.H A₁) ∘ eval′ ∘ (id ⁂ to (MN.H A)) ∘ (id ⁂ to (NO.H A)))
          ≈˘⟨ λ-cong (∘-resp-≈ʳ assoc²') ⟩
            λg (from (NO.H A₁) ∘ (from (MN.H A₁) ∘ eval′ ∘ (id ⁂ to (MN.H A))) ∘ (id ⁂ to (NO.H A)))
          ≈˘⟨ λ-cong (∘-resp-≈ʳ (pullˡ β′)) ⟩
            λg (from (NO.H A₁) ∘ eval′ ∘ (λg (from (MN.H A₁) ∘ eval′ ∘ (id ⁂ to (MN.H A))) ⁂ id) ∘ (id ⁂ to (NO.H A)))
          ≈⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ʳ ⁂∘⁂)) ⟩
            λg (from (NO.H A₁) ∘ eval′ ∘ (λg (from (MN.H A₁) ∘ eval′ ∘ (id ⁂ to (MN.H A))) ∘ id ⁂ id ∘ to (NO.H A)))
          ≈⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ʳ (⁂-cong₂ identityʳ identityˡ))) ⟩
            λg (from (NO.H A₁) ∘ eval′ ∘ (λg (from (MN.H A₁) ∘ eval′ ∘ (id ⁂ to (MN.H A))) ⁂ to (NO.H A)))
          ≈˘⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ʳ (⁂-cong₂ identityˡ identityʳ))) ⟩
            λg (from (NO.H A₁) ∘ eval′ ∘ (id ∘ λg (from (MN.H A₁) ∘ eval′ ∘ (id ⁂ to (MN.H A))) ⁂ to (NO.H A) ∘ id))
          ≈˘⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ʳ ⁂∘⁂)) ⟩
            λg (from (NO.H A₁) ∘ eval′ ∘ (id ⁂ to (NO.H A)) ∘ (λg (from (MN.H A₁) ∘ eval′ ∘ (id ⁂ to (MN.H A))) ⁂ id))
          ≈˘⟨ λ-cong assoc²' ⟩
            λg ((from (NO.H A₁) ∘ eval′ ∘ (id ⁂ to (NO.H A))) ∘ (λg (from (MN.H A₁) ∘ eval′ ∘ (id ⁂ to (MN.H A))) ⁂ id))
          ≈˘⟨ CartesianClosed.exp.subst cartesianClosed product product ⟩
            λg (from (NO.H A₁) ∘ eval′ ∘ (id ⁂ to (NO.H A))) ∘ λg (from (MN.H A₁) ∘ eval′ ∘ (id ⁂ to (MN.H A)))
          ≈⟨ Equiv.refl ⟩
            from (NO.H (A => A₁)) ∘ from (MN.H (A => A₁))
          ∎

        H-compose˘ ⌊ x ⌋ = Equiv.refl
        H-compose˘ Unit = T.!-unique₂
        H-compose˘ (A * A₁) = Equiv.trans (⁂-cong₂ (H-compose˘ A) (H-compose˘ A₁)) (Equiv.sym ⁂∘⁂)
        H-compose˘ (A => A₁) =
          begin
            λg (to (MO.H A₁) ∘ eval′ ∘ (id ⁂ from (MO.H A)))
          ≈⟨ λ-cong (∘-resp-≈ˡ (H-compose˘ A₁)) ⟩
            λg ((to (MN.H A₁) ∘ to (NO.H A₁)) ∘ eval′ ∘ (id ⁂ from (MO.H A)))
          ≈⟨ λ-cong assoc ⟩
            λg (to (MN.H A₁) ∘ to (NO.H A₁) ∘ eval′ ∘ (id ⁂ from (MO.H A)))
          ≈⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ʳ (∘-resp-≈ʳ (⁂-cong₂ Equiv.refl (H-compose A))))) ⟩
            λg (to (MN.H A₁) ∘ to (NO.H A₁) ∘ eval′ ∘ (id ⁂ from (NO.H A) ∘ from (MN.H A)))
          ≈˘⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ʳ (∘-resp-≈ʳ second∘second))) ⟩
            λg (to (MN.H A₁) ∘ to (NO.H A₁) ∘ eval′ ∘ (id ⁂ from (NO.H A)) ∘ (id ⁂ from (MN.H A)))
          ≈˘⟨ λ-cong (∘-resp-≈ʳ assoc²') ⟩
            λg (to (MN.H A₁) ∘ (to (NO.H A₁) ∘ eval′ ∘ (id ⁂ from (NO.H A))) ∘ (id ⁂ from (MN.H A)))
          ≈˘⟨ λ-cong (∘-resp-≈ʳ (pullˡ β′)) ⟩
            λg (to (MN.H A₁) ∘ eval′ ∘ (λg (to (NO.H A₁) ∘ eval′ ∘ (id ⁂ from (NO.H A))) ⁂ id) ∘ (id ⁂ from (MN.H A)))
          ≈⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ʳ ⁂∘⁂)) ⟩
            λg (to (MN.H A₁) ∘ eval′ ∘ (λg (to (NO.H A₁) ∘ eval′ ∘ (id ⁂ from (NO.H A))) ∘ id ⁂ id ∘ from (MN.H A)))
          ≈⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ʳ (⁂-cong₂ identityʳ identityˡ))) ⟩
            λg (to (MN.H A₁) ∘ eval′ ∘ (λg (to (NO.H A₁) ∘ eval′ ∘ (id ⁂ from (NO.H A))) ⁂ from (MN.H A)))
          ≈˘⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ʳ (⁂-cong₂ identityˡ identityʳ))) ⟩
            λg (to (MN.H A₁) ∘ eval′ ∘ (id ∘ λg (to (NO.H A₁) ∘ eval′ ∘ (id ⁂ from (NO.H A))) ⁂ from (MN.H A) ∘ id))
          ≈˘⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ʳ ⁂∘⁂)) ⟩
            λg (to (MN.H A₁) ∘ eval′ ∘ (id ⁂ from (MN.H A)) ∘ (λg (to (NO.H A₁) ∘ eval′ ∘ (id ⁂ from (NO.H A))) ⁂ id))
          ≈˘⟨ λ-cong assoc²' ⟩
            λg ((to (MN.H A₁) ∘ eval′ ∘ (id ⁂ from (MN.H A))) ∘ (λg (to (NO.H A₁) ∘ eval′ ∘ (id ⁂ from (NO.H A))) ⁂ id))
          ≈˘⟨ CartesianClosed.exp.subst cartesianClosed product product ⟩
            λg (to (MN.H A₁) ∘ eval′ ∘ (id ⁂ from (MN.H A))) ∘ λg (to (NO.H A₁) ∘ eval′ ∘ (id ⁂ from (NO.H A)))
          ≈⟨ Equiv.refl ⟩
            to (MN.H (A => A₁)) ∘ to (NO.H (A => A₁))
          ∎

  Models : Category (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ o ⊔ ℓ ⊔ e) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ ⊔ e) (ℓ₁ ⊔ e)
  Models = record
             { Obj = Model 𝒞 cartesianClosed Th
             ; _⇒_ = homomorphism
             ; _≈_ = _≗_
             ; id = Id.id′
             ; _∘_ = Compose.compose
             ; assoc = λ _ → assoc
             ; sym-assoc = λ _ → sym-assoc
             ; identityˡ = λ _ → identityˡ
             ; identityʳ = λ _ → identityʳ
             ; identity² = λ _ → identity²
             ; equiv = record { refl = λ _ → IsEquivalence.refl equiv ; sym = λ x g → IsEquivalence.sym equiv (x g) ; trans = λ x x₁ g → IsEquivalence.trans equiv (x g) (x₁ g) }
             ; ∘-resp-≈ = λ x x₁ g → ∘-resp-≈ (x g) (x₁ g)
             }

max_stars_repo_name: elpinal/exsub-ccc

max_issues_repo_name: elpinal/exsub-ccc

max_forks_repo_name: elpinal/exsub-ccc


text:
-- It is recommended to use Cubical.Algebra.CommRing.Instances.Int
-- instead of this file.

{-# OPTIONS --safe #-}
module Cubical.Algebra.CommRing.Instances.BiInvInt where

open import Cubical.Foundations.Prelude

open import Cubical.Algebra.CommRing
open import Cubical.Data.Int.MoreInts.BiInvInt
  renaming (
    _+_ to _+ℤ_;
    -_ to _-ℤ_;
    +-assoc to +ℤ-assoc;
    +-comm to +ℤ-comm
  )

BiInvℤAsCommRing : CommRing ℓ-zero
BiInvℤAsCommRing =
  makeCommRing
    zero (suc zero) _+ℤ_ _·_ _-ℤ_
    isSetBiInvℤ
    +ℤ-assoc +-zero +-invʳ +ℤ-comm
    ·-assoc ·-identityʳ
    (λ x y z → sym (·-distribˡ x y z))
    ·-comm

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
-- Example usage of solver

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

open import Categories.Category
open import Categories.Category.Cartesian

module Experiment.Categories.Solver.Category.Cartesian.Example
  {o ℓ e} {𝒞 : Category o ℓ e} (cartesian : Cartesian 𝒞) where

open import Experiment.Categories.Solver.Category.Cartesian cartesian

open Category 𝒞
open Cartesian cartesian
open HomReasoning

private
  variable
    A B C D E F : Obj

module _ {f : D ⇒ E} {g : C ⇒ D} {h : B ⇒ C} {i : A ⇒ B} where
  _ : (f ∘ g) ∘ id ∘ h ∘ i ≈ f ∘ (g ∘ h) ∘ i
  _ = solve ((∥-∥ :∘ ∥-∥) :∘ :id :∘ ∥-∥ :∘ ∥-∥) (∥-∥ :∘ (∥-∥ :∘ ∥-∥) :∘ ∥-∥) refl

swap∘swap≈id :
  ∀ {A B} → swap {A}{B} ∘ swap {B}{A} ≈ id
swap∘swap≈id {A} {B} =
  solve (:swap {∥ A ∥} {∥ B ∥} :∘ :swap)
        :id
        refl

assocʳ∘assocˡ≈id : ∀ {A B C} → assocʳ {A}{B}{C} ∘ assocˡ {A}{B}{C} ≈ id
assocʳ∘assocˡ≈id = solve (:assocʳ {∥ _ ∥} {∥ _ ∥} {∥ _ ∥} :∘ :assocˡ) :id refl

module _ {f : B ⇒ C} (f′ : A ⇒ B) {g : E ⇒ F} {g′ : D ⇒ E} where
  ⁂-∘ : (f ⁂ g) ∘ (f′ ⁂ g′) ≈ (f ∘ f′) ⁂ (g ∘ g′)
  ⁂-∘ = solve lhs rhs refl where
    lhs = (∥ f ∥ :⁂ ∥ g ∥) :∘ (∥ f′ ∥ :⁂ ∥ g′ ∥)
    rhs = (∥ f ∥ :∘ ∥ f′ ∥) :⁂ (∥ g ∥ :∘ ∥ g′ ∥)

module _ {A B C D} where
  pentagon′ : (id ⁂ assocˡ) ∘ assocˡ ∘ (assocˡ ⁂ id) ≈
              assocˡ ∘ assocˡ {A × B} {C} {D}
  pentagon′ = solve lhs rhs refl where
    lhs = (:id :⁂ :assocˡ) :∘ :assocˡ :∘ (:assocˡ :⁂ :id)
    rhs = :assocˡ :∘ :assocˡ {∥ A ∥ :× ∥ B ∥} {∥ C ∥} {∥ D ∥}

module _ {A B C} where
  hexagon₁′ : (id ⁂ swap) ∘ assocˡ ∘ (swap ⁂ id) ≈
              assocˡ ∘ swap ∘ assocˡ {A}{B}{C}
  hexagon₁′ = solve lhs rhs refl where
    lhs = (:id :⁂ :swap) :∘ :assocˡ :∘ (:swap :⁂ :id)
    rhs = :assocˡ :∘ :swap :∘ :assocˡ {∥ A ∥}{∥ B ∥}{∥ C ∥}

module _ {f : A ⇒ B} where
  commute : ⟨ ! , id ⟩ ∘ f ≈ ⟨ id ∘ π₁ , f ∘ π₂ ⟩ ∘ ⟨ ! , id ⟩
  commute = solve (:⟨ :! , :id ⟩ :∘ ∥ f ∥)
                  (:⟨ :id :∘ :π₁ , ∥ f ∥ :∘ :π₂ ⟩ :∘ :⟨ :! , :id ⟩)
                  refl

_ : id {⊤} ≈ !
_ = solve (∥ id !∥) :! refl

_ : π₁ {⊤} {⊤} ≈ π₂
_ = solve (:π₁ {:⊤} {:⊤}) :π₂ refl

module _ {f : A ⇒ B} {g : C ⇒ D} where
  first↔second′ : first f ∘ second g ≈ second g ∘ first f
  first↔second′ = solve (:first ∥ f ∥ :∘ :second ∥ g ∥)
                        (:second ∥ g ∥ :∘ :first ∥ f ∥)
                        refl


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

open import Cubical.HITs.KleinBottle.Base public
open import Cubical.HITs.KleinBottle.Properties public

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:
data Unit : Set where
  unit : Unit

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just : A → Maybe A

data Test : Set where
  map : (Unit → Maybe Test) → Test

-- Accepted:
foo : Test → Unit
foo-aux : Maybe Test → Unit
foo (map f) = foo-aux (f unit)
foo-aux nothing = unit
foo-aux (just x) = foo x

test : Test → Unit
test (map f) with f unit
test (map f) | nothing = unit
test (map f) | just x = test x

-- WAS: Termination checker complains
-- SHOULD: succeed

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module nats where

open import Data.Nat

ten : ℕ
ten = 10


text:
open import Agda.Builtin.Nat

postulate P : Nat → Set

record R : Set where
  field
    f : P zero

foo : R → Set
foo (record { f = f0 }) with zero
foo r | x = Nat


text:
module Proof where

-- stdlib import
open import Data.Nat

main : ℕ
main = suc zero

max_stars_repo_name: sourcedennis/docker-agda-mini

max_issues_repo_name: sourcedennis/docker-agda-mini

max_forks_repo_name: sourcedennis/docker-agda-mini


text:
{-# OPTIONS --cubical #-}
module _ where

open import Agda.Builtin.Nat
open import Agda.Builtin.Cubical.Path

postulate
  admit : ∀ {A : Set} → A

data Z : Set where
  pos      : Nat → Z
  neg      : Nat → Z
  sameZero : pos 0 ≡ neg 0

_+Z_ : Z → Z → Z
pos x +Z pos x₁ = admit
pos x +Z neg x₁ = admit
pos x +Z sameZero x₁ = admit
neg x +Z z' = admit
sameZero x +Z z' = admit

max_stars_repo_name: phadej/agda

max_issues_repo_name: phadej/agda

max_forks_repo_name: phadej/agda


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

open import HoTT renaming (pt to ⊙pt)
open import homotopy.Bouquet
open import homotopy.FinWedge
open import homotopy.SphereEndomorphism
open import homotopy.DisjointlyPointedSet
open import groups.SphereEndomorphism
open import groups.SumOfSubIndicator
open import groups.DisjointlyPointedSet
open import cw.CW
open import cw.DegreeByProjection
open import cw.FinBoundary
open import cw.FinCW
open import cw.WedgeOfCells
open import cohomology.Theory

module cw.cohomology.cochainequiv.FirstCoboundary (OT : OrdinaryTheory lzero)
  (⊙fin-skel : ⊙FinSkeleton 1) where

open OrdinaryTheory OT
open import cohomology.RephraseSubFinCoboundary OT
open import cohomology.SubFinBouquet OT

private
  ⊙skel = ⊙FinSkeleton-realize ⊙fin-skel
  fin-skel = ⊙FinSkeleton.skel ⊙fin-skel
  I = AttachedFinSkeleton.numCells fin-skel
  skel = ⊙Skeleton.skel ⊙skel
  dec = FinSkeleton-has-cells-with-dec-eq fin-skel
  ac = FinSkeleton-has-cells-with-choice 0 fin-skel lzero

  fin-skel₋₁ = fcw-init fin-skel
  ac₋₁ = FinSkeleton-has-cells-with-choice 0 fin-skel₋₁ lzero
  endpoint = attaching-last skel
  I₋₁ = AttachedFinSkeleton.skel fin-skel
  ⊙head = ⊙cw-head ⊙skel
  pt = ⊙pt ⊙head

open DegreeAtOne skel dec
open import cw.cohomology.WedgeOfCells OT ⊙skel
open import cw.cohomology.reconstructed.TipAndAugment OT (⊙cw-init ⊙skel)
open import cw.cohomology.reconstructed.TipCoboundary OT ⊙skel
open import cw.cohomology.cochainequiv.FirstCoboundaryAbstractDefs OT ⊙fin-skel

abstract
  rephrase-cw-co∂-head'-in-degree : ∀ g
    → GroupIso.f (CXₙ/Xₙ₋₁-diag-β ac) (GroupHom.f cw-co∂-head' (GroupIso.g (CX₀-diag-β ac₋₁) g))
    ∼ λ <I → Group.subsum-r (C2 0) ⊙head-separate
        (λ b → Group.exp (C2 0) (g b) (degree <I (fst b)))
  rephrase-cw-co∂-head'-in-degree g <I =
    GroupIso.f (C-FinBouquet-diag 1 I)
      (CEl-fmap 1 (⊙–> (Bouquet-⊙equiv-Xₙ/Xₙ₋₁ skel))
        (CEl-fmap 1 ⊙cw-∂-head'-before-Susp
          (<– (CEl-Susp 0 ⊙head)
            (CEl-fmap 0 (⊙<– (Bouquet-⊙equiv-X ⊙head-is-separable))
              (GroupIso.g (C-SubFinBouquet-diag 0 MinusPoint-⊙head-has-choice ⊙head-separate)
                g))))) <I
      =⟨ ap
          (λ g →
            GroupIso.f (C-FinBouquet-diag 1 I)
              (CEl-fmap 1 (⊙–> (Bouquet-⊙equiv-Xₙ/Xₙ₋₁ skel))
                (CEl-fmap 1 ⊙cw-∂-head'-before-Susp g)) <I) $
          C-Susp-fmap' 0 (⊙<– (Bouquet-⊙equiv-X (Fin-has-dec-eq pt))) □$ᴳ
            (GroupIso.g (C-SubFinBouquet-diag 0 MinusPoint-⊙head-has-choice ⊙head-separate)
              g) ⟩
    GroupIso.f (C-FinBouquet-diag 1 I)
      (CEl-fmap 1 (⊙–> (Bouquet-⊙equiv-Xₙ/Xₙ₋₁ skel))
        (CEl-fmap 1 ⊙cw-∂-head'-before-Susp
          (CEl-fmap 1 (⊙Susp-fmap (⊙<– (Bouquet-⊙equiv-X ⊙head-is-separable)))
            (<– (CEl-Susp 0 (⊙Bouquet (MinusPoint ⊙head) 0))
              (GroupIso.g (C-SubFinBouquet-diag 0 MinusPoint-⊙head-has-choice ⊙head-separate)
                g))))) <I
      =⟨ ap (λ g → GroupIso.f (C-FinBouquet-diag 1 I) g <I) $
            ∘-CEl-fmap 1 (⊙–> (Bouquet-⊙equiv-Xₙ/Xₙ₋₁ skel)) ⊙cw-∂-head'-before-Susp
              (CEl-fmap 1 (⊙Susp-fmap (⊙<– (Bouquet-⊙equiv-X ⊙head-is-separable)))
                (<– (CEl-Susp 0 (⊙Bouquet (MinusPoint ⊙head) 0))
                  (GroupIso.g (C-SubFinBouquet-diag 0 MinusPoint-⊙head-has-choice ⊙head-separate)
                    g)))
          ∙ ∘-CEl-fmap 1
              (⊙cw-∂-head'-before-Susp ⊙∘ ⊙–> (Bouquet-⊙equiv-Xₙ/Xₙ₋₁ skel))
              (⊙Susp-fmap (⊙<– (Bouquet-⊙equiv-X ⊙head-is-separable)))
              (<– (CEl-Susp 0 (⊙Bouquet (MinusPoint ⊙head) 0))
                (GroupIso.g (C-SubFinBouquet-diag 0 MinusPoint-⊙head-has-choice ⊙head-separate)
                  g))
          ∙ ap (λ f → CEl-fmap 1 f
              (<– (CEl-Susp 0 (⊙Bouquet (MinusPoint ⊙head) 0))
                (GroupIso.g (C-SubFinBouquet-diag 0 MinusPoint-⊙head-has-choice ⊙head-separate)
                  g)))
              (! ⊙function₀'-β) ⟩
    GroupIso.f (C-FinBouquet-diag 1 I)
      (CEl-fmap 1 ⊙function₀'
        (<– (CEl-Susp 0 (⊙Bouquet (MinusPoint ⊙head) 0))
          (GroupIso.g (C-SubFinBouquet-diag 0 MinusPoint-⊙head-has-choice ⊙head-separate)
            g))) <I
      =⟨ rephrase-in-degree 0 {I = I} MinusPoint-⊙head-has-choice
          MinusPoint-⊙head-has-dec-eq ⊙head-separate-equiv ⊙function₀' g <I ⟩
    Group.subsum-r (C2 0) ⊙head-separate
      (λ b → Group.exp (C2 0) (g b)
        (⊙SphereS-endo-degree 0
          (⊙Susp-fmap (⊙bwproj MinusPoint-⊙head-has-dec-eq b) ⊙∘ ⊙function₀' ⊙∘ ⊙fwin <I)))
      =⟨ ap (Group.subsum-r (C2 0) ⊙head-separate)
          (λ= λ b → ap (Group.exp (C2 0) (g b)) $
            ⊙SphereS-endo-degree-base-indep 0
              {f = (  ⊙Susp-fmap (⊙bwproj MinusPoint-⊙head-has-dec-eq b)
                   ⊙∘ ⊙function₀'
                   ⊙∘ ⊙fwin <I)}
              {g = (Susp-fmap (function₁' <I b) , idp)}
              (mega-reduction <I b)) ⟩
    Group.subsum-r (C2 0) ⊙head-separate
      (λ b → Group.exp (C2 0) (g b)
        (⊙SphereS-endo-degree 0
          (Susp-fmap (function₁' <I b) , idp)))
      =⟨ ap (Group.subsum-r (C2 0) ⊙head-separate)
          (λ= λ b → ap (Group.exp (C2 0) (g b)) $
            degree-matches <I b) ⟩
    Group.subsum-r (C2 0) ⊙head-separate
      (λ b → Group.exp (C2 0) (g b)
        (degree <I (fst b)))
      =∎

abstract
  private
    degree-true-≠ : ∀ {<I <I₋₁} → (<I₋₁ ≠ endpoint <I true) → degree-true <I <I₋₁ == 0
    degree-true-≠ {<I} {<I₋₁} neq with Fin-has-dec-eq <I₋₁ (endpoint <I true)
    ... | inl eq = ⊥-rec (neq eq)
    ... | inr _ = idp

    degree-true-diag : ∀ <I → degree-true <I (endpoint <I true) == -1
    degree-true-diag <I with Fin-has-dec-eq (endpoint <I true) (endpoint <I true)
    ... | inl _ = idp
    ... | inr neq = ⊥-rec (neq idp)

    sum-degree-true : ∀ <I g → Group.sum (C2 0) (λ <I₋₁ → Group.exp (C2 0) g (degree-true <I <I₋₁)) == Group.inv (C2 0) g
    sum-degree-true <I g =
        sum-subindicator (C2 0) (λ <I₋₁ → Group.exp (C2 0) g (degree-true <I <I₋₁))
          (endpoint <I true) (λ neq → ap (Group.exp (C2 0) g) (degree-true-≠ neq))
      ∙ ap (Group.exp (C2 0) g) (degree-true-diag <I)

    degree-false-≠ : ∀ {<I <I₋₁} → (<I₋₁ ≠ endpoint <I false) → degree-false <I <I₋₁ == 0
    degree-false-≠ {<I} {<I₋₁} neq with Fin-has-dec-eq <I₋₁ (endpoint <I false)
    ... | inl eq = ⊥-rec (neq eq)
    ... | inr _ = idp

    degree-false-diag : ∀ <I → degree-false <I (endpoint <I false) == 1
    degree-false-diag <I with Fin-has-dec-eq (endpoint <I false) (endpoint <I false)
    ... | inl _ = idp
    ... | inr neq = ⊥-rec (neq idp)

    sum-degree-false : ∀ <I g → Group.sum (C2 0) (λ <I₋₁ → Group.exp (C2 0) g (degree-false <I <I₋₁)) == g
    sum-degree-false <I g =
        sum-subindicator (C2 0) (λ <I₋₁ → Group.exp (C2 0) g (degree-false <I <I₋₁))
          (endpoint <I false) (λ neq → ap (Group.exp (C2 0) g) (degree-false-≠ neq))
      ∙ ap (Group.exp (C2 0) g) (degree-false-diag <I)

    sum-degree : ∀ <I g → Group.sum (C2 0) (λ <I₋₁ → Group.exp (C2 0) g (degree <I <I₋₁)) == Group.ident (C2 0)
    sum-degree <I g =
        ap (Group.sum (C2 0)) (λ= λ <I₋₁ → Group.exp-+ (C2 0) g (degree-true <I <I₋₁) (degree-false <I <I₋₁))
      ∙ AbGroup.sum-comp (C2-abgroup 0)
          (λ <I₋₁ → Group.exp (C2 0) g (degree-true <I <I₋₁))
          (λ <I₋₁ → Group.exp (C2 0) g (degree-false <I <I₋₁))
      ∙ ap2 (Group.comp (C2 0))
          (sum-degree-true <I g)
          (sum-degree-false <I g)
      ∙ Group.inv-l (C2 0) g

    merge-branches : ∀ (g : Fin I₋₁ → Group.El (C2 0)) (g-pt : g pt == Group.ident (C2 0)) x
      →  Coprod-rec (λ _ → Group.ident (C2 0)) (λ b → g (fst b)) (⊙head-separate x)
      == g x
    merge-branches g g-pt x with Fin-has-dec-eq pt x
    merge-branches g g-pt x | inl idp = ! g-pt
    merge-branches g g-pt x | inr _ = idp

  rephrase-cw-co∂-head-in-degree : ∀ g
    → GroupIso.f (CXₙ/Xₙ₋₁-diag-β ac) (GroupHom.f cw-co∂-head (GroupIso.g (C2×CX₀-diag-β ac₋₁) g))
    ∼ λ <I → Group.sum (C2 0) (λ <I₋₁ → Group.exp (C2 0) (g <I₋₁) (degree <I <I₋₁))
  rephrase-cw-co∂-head-in-degree g <I =
    GroupIso.f (CXₙ/Xₙ₋₁-diag-β ac) (GroupHom.f cw-co∂-head' (GroupIso.g (CX₀-diag-β ac₋₁) (snd (diff-and-separate (C2 0) g)))) <I
      =⟨ rephrase-cw-co∂-head'-in-degree (snd (diff-and-separate (C2 0) g)) <I ⟩
    Group.subsum-r (C2 0) ⊙head-separate
      (λ b → Group.exp (C2 0) (Group.diff (C2 0) (g (fst b)) (g pt))
        (degree <I (fst b)))
      =⟨ ap (Group.sum (C2 0)) (λ= λ <I₋₁ →
          merge-branches
            (λ <I₋₁ → Group.exp (C2 0) (Group.diff (C2 0) (g <I₋₁) (g pt)) (degree <I <I₋₁))
            ( ap (λ g → Group.exp (C2 0) g (degree <I pt)) (Group.inv-r (C2 0) (g pt))
            ∙ Group.exp-ident (C2 0) (degree <I pt))
            <I₋₁
          ∙ AbGroup.exp-comp (C2-abgroup 0) (g <I₋₁) (Group.inv (C2 0) (g pt)) (degree <I <I₋₁)) ⟩
    Group.sum (C2 0) (λ <I₋₁ →
      Group.comp (C2 0)
        (Group.exp (C2 0) (g <I₋₁) (degree <I <I₋₁))
        (Group.exp (C2 0) (Group.inv (C2 0) (g pt)) (degree <I <I₋₁)))
      =⟨ AbGroup.sum-comp (C2-abgroup 0)
          (λ <I₋₁ → Group.exp (C2 0) (g <I₋₁) (degree <I <I₋₁))
          (λ <I₋₁ → Group.exp (C2 0) (Group.inv (C2 0) (g pt)) (degree <I <I₋₁)) ⟩
    Group.comp (C2 0)
      (Group.sum (C2 0) (λ <I₋₁ → Group.exp (C2 0) (g <I₋₁) (degree <I <I₋₁)))
      (Group.sum (C2 0) (λ <I₋₁ → Group.exp (C2 0) (Group.inv (C2 0) (g pt)) (degree <I <I₋₁)))
      =⟨ ap (Group.comp (C2 0) (Group.sum (C2 0) (λ <I₋₁ → Group.exp (C2 0) (g <I₋₁) (degree <I <I₋₁))))
          (sum-degree <I (Group.inv (C2 0) (g pt)))
        ∙ Group.unit-r (C2 0) _ ⟩
    Group.sum (C2 0) (λ <I₋₁ → Group.exp (C2 0) (g <I₋₁) (degree <I <I₋₁))
      =∎

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
-- FNF, 2017-06-13, issue # 2592 reported by Manuel Bärenz

-- The .in file loads Issue2592/B.agda and Issue2592/C.agda that both
-- imports Issue2592/A.agda.


text:
data ⊥ : Set where

module M₁ where

  postulate
    ∥_∥ : Set → Set

  {-# POLARITY ∥_∥ ++ #-}

  data D : Set where
    c : ∥ D ∥ → D

module M₂ where

  postulate
    _⇒_    : Set → Set → Set
    lambda : {A B : Set} → (A → B) → A ⇒ B
    apply  : {A B : Set} → A ⇒ B → A → B

  {-# POLARITY _⇒_ ++ #-}

  data D : Set where
    c : D ⇒ ⊥ → D

  not-inhabited : D → ⊥
  not-inhabited (c f) = apply f (c f)

  d : D
  d = c (lambda not-inhabited)

  bad : ⊥
  bad = not-inhabited d

postulate
  F₁ : Set → Set → Set₁ → Set₁ → Set₁ → Set

{-# POLARITY F₁ _ ++ + - * #-}

data D₁ : Set where
  c : F₁ (D₁ → ⊥) D₁ Set Set Set → D₁

postulate
  F₂ : ∀ {a} → Set a → Set a → Set a

{-# POLARITY F₂ * * ++ #-}

data D₂ (A : Set) : Set where
  c : F₂ A (D₂ A) → D₂ A

module _ (A : Set₁) where

  postulate
    F₃ : Set → Set

  {-# POLARITY F₃ ++ #-}

data D₃ : Set where
  c : F₃ Set D₃ → D₃

postulate
  F₄ : ∀ {a} → Set a → Set a → Set a

{-# POLARITY F₄ * ++ #-}

data D₄ (A : Set) : Set where
  c : F₄ (D₄ A) A → D₄ A

postulate
  F₅ : ⦃ _ : Set ⦄ → Set

{-# POLARITY F₅ ++ #-}

data D₅ : Set where
  c : F₅ ⦃ D₅ ⦄ → D₅


text:
module Tuples where

open import Data.Product

_² : ∀ {a} (A : Set a) → Set a
A ² = A × A

_³ : ∀ {a} (A : Set a) → Set a
A ³ = A × A ²

_⁴ : ∀ {a} (A : Set a) → Set a
A ⁴ = A × A ³

_⁵ : ∀ {a} (A : Set a) → Set a
A ⁵ = A × A ⁴

_⁶ : ∀ {a} (A : Set a) → Set a
A ⁶ = A × A ⁵

_⁷ : ∀ {a} (A : Set a) → Set a
A ⁷ = A × A ⁶


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

open import function.extensionality.core public
open import function.extensionality.proof public
open import function.extensionality.strong public
  using (strong-funext; strong-funext-iso)
open import function.extensionality.computation public

open import equality.core
open import function.isomorphism
open import function.overloading

-- extensionality for functions of implicit arguments
impl-funext : ∀ {i j}{X : Set i}{Y : X → Set j}
          → {f g : {x : X} → Y x}
          → ((x : X) → f {x} ≡ g {x})
          → (λ {x} → f {x}) ≡ g
impl-funext h = ap (apply impl-iso) (funext h)

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types